Logs on 2023-12-11 (liberachat/#haskell)
| 00:01:57 | × | alp_ quits (~alp@2001:861:e3d6:8f80:7092:9744:337:b98c) (Ping timeout: 256 seconds) |
| 00:22:48 | × | Volt_ quits (~Volt_@c-73-47-181-152.hsd1.ma.comcast.net) (Quit: ) |
| 00:36:30 | → | juri_ joins (~juri@79.140.117.38) |
| 00:37:39 | × | tri quits (~tri@ool-18bc2e74.dyn.optonline.net) (Ping timeout: 256 seconds) |
| 00:39:41 | × | juri____ quits (~juri@79.140.117.56) (Ping timeout: 268 seconds) |
| 00:59:06 | → | skyres_ joins (~skyres@176.254.244.83) |
| 01:01:42 | <hexology> | hc: i believe the classic exponential time example is recursive fibonacci without memoization |
| 01:01:47 | × | skyres quits (~skyres@176.254.244.83) (Ping timeout: 264 seconds) |
| 01:03:45 | × | pretty_dumm_guy quits (trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655) (Quit: WeeChat 3.5) |
| 01:06:21 | → | tri joins (~tri@ool-18bc2e74.dyn.optonline.net) |
| 01:08:18 | × | sawilagar quits (~sawilagar@user/sawilagar) (Ping timeout: 256 seconds) |
| 01:10:08 | → | [_] joins (~itchyjunk@user/itchyjunk/x-7353470) |
| 01:13:54 | × | [itchyjunk] quits (~itchyjunk@user/itchyjunk/x-7353470) (Ping timeout: 268 seconds) |
| 01:20:31 | → | Feuermagier joins (~Feuermagi@user/feuermagier) |
| 01:21:32 | → | emmanuelux joins (~emmanuelu@user/emmanuelux) |
| 01:21:54 | × | waleee quits (~waleee@176.10.144.38) (Ping timeout: 256 seconds) |
| 01:22:49 | × | emmanuelux_ quits (~emmanuelu@user/emmanuelux) (Ping timeout: 276 seconds) |
| 01:26:20 | <Axman6> | tri: `const a <$> b` is `(const a) <$> b` (or, `(<$>) (const a) b` if you like to move infix functions to prefix) |
| 01:27:01 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:d128:ce35:54e1:65e2) (Remote host closed the connection) |
| 01:27:33 | <ski> | @type (<$) |
| 01:27:34 | <lambdabot> | Functor f => a -> f b -> f a |
| 01:28:05 | <ski> | `const a <$> fb' is `a <$ fb' |
| 01:28:36 | <ski> | tri,dibblego,geekosaur : i don't particularly like the term "higher-kinded type" at all, i think it's unnecessary and confusing. `chr :: Int -> Char' is a first-order function, `interact :: (String -> String) -> IO ()' is a second-order (therefore higher-order) function, because it takes a (first-order) function as input |
| 01:28:49 | <ski> | `Either :: * -> * -> *' and `ReadS :: * -> *' (the former being a type constructor, while the latter being a type synonym of arity `1') are (first-order) type functions, while `MaybeT :: (* -> *) -> * -> *' is a second-order (therefore higher-order) type function (type constructor), and `Alternative :: (* -> *) -> Constraint' is a second-order type function (type class) |
| 01:29:07 | × | tri quits (~tri@ool-18bc2e74.dyn.optonline.net) (Ping timeout: 255 seconds) |
| 01:39:45 | <hexology> | HLS style suggestions are really useful. i'm learning about a lot of nice utility functions i might not have found otherwise |
| 01:41:36 | → | tri joins (~tri@ool-18bc2e74.dyn.optonline.net) |
| 01:43:14 | <jackdk> | Are they the same ones that come from hlint? |
| 01:44:41 | <hexology> | i wouldn't know |
| 01:44:48 | <geekosaur> | they are |
| 01:45:25 | <dibblego> | ski: I agree. |
| 01:47:15 | <geekosaur> | tri, you missed from https://ircbrowse.tomsmeding.com/browse/lchaskell?id=1166072#trid1166072 |
| 01:47:31 | × | tri quits (~tri@ool-18bc2e74.dyn.optonline.net) (Ping timeout: 268 seconds) |
| 01:47:35 | <geekosaur> | sigh |
| 01:48:13 | → | szkl joins (uid110435@id-110435.uxbridge.irccloud.com) |
| 01:57:28 | × | machinedgod quits (~machinedg@93-136-52-133.adsl.net.t-com.hr) (Ping timeout: 255 seconds) |
| 01:58:28 | → | tri joins (~tri@ool-18bc2e74.dyn.optonline.net) |
| 01:59:27 | → | machinedgod joins (~machinedg@93-136-135-211.adsl.net.t-com.hr) |
| 01:59:49 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:d128:ce35:54e1:65e2) |
| 02:01:31 | <ski> | tri : are you there ? |
| 02:04:28 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:d128:ce35:54e1:65e2) (Ping timeout: 268 seconds) |
| 02:05:34 | × | FinnElija quits (~finn_elij@user/finn-elija/x-0085643) (Remote host closed the connection) |
| 02:05:52 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:d128:ce35:54e1:65e2) |
| 02:06:04 | <jackdk> | that's cool. I learned a lot from the hlint suggestiosn |
| 02:06:14 | → | FinnElija joins (~finn_elij@user/finn-elija/x-0085643) |
| 02:06:16 | <jackdk> | Not spelling, admittedly, but a lot of other things |
| 02:16:11 | <ski> | tri,dibblego,geekosaur : the, imho, bad term "higher-kinded types" refers to (a) being able to have polymorphic operations that are polymorphic in type functions, e.g. `empty :: Alternative f => f a'; .. |
| 02:16:23 | <ski> | .. and (b) being able to parameterize type functions (including type classes) over other type functions, e.g. `newtype MaybeT m a = MaybeT (m (Maybe a))' and `class Applicative i => Alternative i where empty :: i a; ...', iow higher-order type functions |
| 02:16:39 | <dibblego> | I also agree! |
| 02:17:08 | <ski> | most other languages with parametric polymorphism and parameterized types ("generics") only allow the universally (and existentially, in case of Mercury) quantified variables in type signatures, as well as the type variable parameters in definitions of parameterized data types (iow type functions) to be of "concrete" kind, .. |
| 02:17:16 | <ski> | .., iow in Haskell terms of kind `*'/`Type' (or other concrete kinds, like unboxed stuff), rather than of a kind of shape `... -> ...', iow a type function having a function kind |
| 02:21:02 | <ski> | a type like `Map Integer [Integer]' (perhaps used to keep track of which other nodes each node in a graph is connected to) is a "template", with the "holes" filled by the types `Integer' (type of keys) and `[Integer]' (type of values). in some other language, this might be written as `Map<Integer,List<Integer>>' |
| 02:21:19 | × | jle` quits (~jle`@2603-8001-3b02-84d4-bd21-edb6-1dc1-99d4.res6.spectrum.com) (Ping timeout: 260 seconds) |
| 02:22:06 | <ski> | most languages supporting such generics / parameterized types / "templates", though only allow "concrete" types to be parameters of the "templates", not allow other "templates" to be passed as parameters. Haskell does. templates in C++ also allows this, afaiui |
| 02:34:15 | × | tri quits (~tri@ool-18bc2e74.dyn.optonline.net) (Ping timeout: 252 seconds) |
| 02:44:30 | <iqubic> | Does anyone here use Emacs? I have an LSP set up, but I'm wondering if it's possible to get inline evaluation working. Like, I type a comment of the form "-- >>> 1+2" and then hit a key combo and the code is evaluated and the result is put in the buffer. |
| 02:47:16 | → | tri joins (~tri@ool-18bc2e74.dyn.optonline.net) |
| 02:50:39 | ski | looks at tri |
| 02:51:33 | <iqubic> | Why? |
| 02:52:17 | × | maars quits (uid160334@id-160334.uxbridge.irccloud.com) (Quit: Connection closed for inactivity) |
| 02:52:20 | <ski> | because i was trying to reply to them, but they keep disconnecting and reconnecting, and doesn't appear to be noticing IRC at the moment, for whatever reason |
| 02:52:46 | × | tri quits (~tri@ool-18bc2e74.dyn.optonline.net) (Ping timeout: 246 seconds) |
| 02:52:54 | <ski> | (see ?) |
| 02:53:16 | × | Pixi quits (~Pixi@user/pixi) (Quit: Leaving) |
| 02:53:32 | <iqubic> | I see. |
| 02:56:35 | × | qqq quits (~qqq@92.43.167.61) (Quit: leaving) |
| 02:57:47 | <iqubic> | Basically, the emacs package Dante has this feature, and I want to see if I can have that done without installing a whole plugin for this. https://github.com/jyp/dante#reploid |
| 02:59:40 | × | mrmr15533 quits (~mrmr@user/mrmr) (Ping timeout: 276 seconds) |
| 03:00:16 | <iqubic> | I want to see if I can have that done with just the plugins I have. |
| 03:01:47 | × | YoungFrog quits (~youngfrog@39.129-180-91.adsl-dyn.isp.belgacom.be) (Ping timeout: 264 seconds) |
| 03:02:31 | → | peterbecich joins (~Thunderbi@047-229-123-186.res.spectrum.com) |
| 03:02:46 | × | hsw quits (~hsw@2001-b030-2303-0104-0172-0025-0012-0132.hinet-ip6.hinet.net) (Ping timeout: 256 seconds) |
| 03:04:32 | → | tri joins (~tri@ool-18bc2e74.dyn.optonline.net) |
| 03:05:45 | → | finn_elija joins (~finn_elij@user/finn-elija/x-0085643) |
| 03:05:45 | × | FinnElija quits (~finn_elij@user/finn-elija/x-0085643) (Killed (NickServ (Forcing logout FinnElija -> finn_elija))) |
| 03:05:45 | finn_elija | is now known as FinnElija |
| 03:05:51 | × | Unicorn_Princess quits (~Unicorn_P@user/Unicorn-Princess/x-3540542) (Quit: Leaving) |
| 03:08:25 | → | urdh joins (~urdh@user/urdh) |
| 03:10:26 | × | tri quits (~tri@ool-18bc2e74.dyn.optonline.net) (Ping timeout: 260 seconds) |
| 03:12:43 | → | Pixi joins (~Pixi@user/pixi) |
| 03:15:31 | × | FinnElija quits (~finn_elij@user/finn-elija/x-0085643) (Remote host closed the connection) |
| 03:15:55 | → | FinnElija joins (~finn_elij@user/finn-elija/x-0085643) |
| 03:16:12 | → | nate4 joins (~nate@c-98-45-158-125.hsd1.ca.comcast.net) |
| 03:20:05 | → | tri joins (~tri@ool-18bc2e74.dyn.optonline.net) |
| 03:21:10 | × | nate4 quits (~nate@c-98-45-158-125.hsd1.ca.comcast.net) (Ping timeout: 255 seconds) |
| 03:30:07 | × | bitdex quits (~bitdex@gateway/tor-sasl/bitdex) (Ping timeout: 240 seconds) |
| 03:30:11 | → | [itchyjunk] joins (~itchyjunk@user/itchyjunk/x-7353470) |
| 03:33:09 | → | bitdex joins (~bitdex@gateway/tor-sasl/bitdex) |
| 03:33:56 | × | [_] quits (~itchyjunk@user/itchyjunk/x-7353470) (Ping timeout: 256 seconds) |
| 03:36:51 | × | machinedgod quits (~machinedg@93-136-135-211.adsl.net.t-com.hr) (Ping timeout: 256 seconds) |
| 03:37:36 | ← | tri parts (~tri@ool-18bc2e74.dyn.optonline.net) () |
| 03:37:46 | → | tri joins (~tri@ool-18bc2e74.dyn.optonline.net) |
| 03:38:56 | → | hsw joins (~hsw@2001-b030-2303-0104-0172-0025-0012-0132.hinet-ip6.hinet.net) |
| 03:39:33 | ski | glances in the general direction of tri |
| 03:40:09 | → | [_] joins (~itchyjunk@user/itchyjunk/x-7353470) |
| 03:40:12 | × | renzhi quits (~xp@2607:fa49:6500:b100::3ce6) (Quit: WeeChat 3.0) |
| 03:43:41 | × | [itchyjunk] quits (~itchyjunk@user/itchyjunk/x-7353470) (Ping timeout: 245 seconds) |
| 03:46:24 | × | peterbecich quits (~Thunderbi@047-229-123-186.res.spectrum.com) (Ping timeout: 256 seconds) |
| 03:46:32 | × | pagnol quits (~user@2a02:a210:a3c:b00:87aa:b531:d3b2:73fa) (Ping timeout: 268 seconds) |
| 03:46:39 | → | nate4 joins (~nate@c-98-45-158-125.hsd1.ca.comcast.net) |
| 03:49:44 | → | Feuermagier_ joins (~Feuermagi@user/feuermagier) |
| 03:49:44 | × | Feuermagier quits (~Feuermagi@user/feuermagier) (Killed (calcium.libera.chat (Nickname regained by services))) |
| 03:49:45 | Feuermagier_ | is now known as Feuermagier |
| 04:00:00 | × | Taneb quits (~Taneb@runciman.hacksoc.org) (Quit: I seem to have stopped.) |
| 04:00:10 | → | [itchyjunk] joins (~itchyjunk@user/itchyjunk/x-7353470) |
| 04:00:32 | × | Square quits (~Square@user/square) (Ping timeout: 256 seconds) |
| 04:01:07 | → | Taneb joins (~Taneb@2001:41c8:51:10d:aaaa:0:aaaa:0) |
| 04:02:19 | × | emmanuelux quits (~emmanuelu@user/emmanuelux) (Quit: au revoir) |
| 04:03:41 | × | [_] quits (~itchyjunk@user/itchyjunk/x-7353470) (Ping timeout: 240 seconds) |
| 04:04:44 | → | trev joins (~trev@user/trev) |
| 04:22:43 | × | hgolden quits (~hgolden@2603-8000-9d00-3ed1-dd4f-298a-9c49-a0ed.res6.spectrum.com) (Remote host closed the connection) |
| 04:24:30 | → | hgolden joins (~hgolden@2603-8000-9d00-3ed1-dd4f-298a-9c49-a0ed.res6.spectrum.com) |
| 04:28:35 | × | johnw quits (~johnw@69.62.242.138) (Quit: ZNC - http://znc.in) |
| 04:29:23 | × | hgolden quits (~hgolden@2603-8000-9d00-3ed1-dd4f-298a-9c49-a0ed.res6.spectrum.com) (Remote host closed the connection) |
| 04:31:27 | → | hgolden joins (~hgolden@2603-8000-9d00-3ed1-dd4f-298a-9c49-a0ed.res6.spectrum.com) |
| 04:39:56 | → | aforemny_ joins (~aforemny@2001:9e8:6cdd:be00:6f70:eeee:fde4:e2c7) |
| 04:41:16 | × | aforemny quits (~aforemny@2001:9e8:6cf6:8a00:1295:f852:5f8f:52b5) (Ping timeout: 255 seconds) |
| 04:48:53 | × | nate4 quits (~nate@c-98-45-158-125.hsd1.ca.comcast.net) (Ping timeout: 240 seconds) |
| 04:50:36 | × | jargon quits (~jargon@32.sub-174-238-226.myvzw.com) (Remote host closed the connection) |
| 05:02:45 | × | chexum quits (~quassel@gateway/tor-sasl/chexum) (Remote host closed the connection) |
| 05:03:02 | → | chexum joins (~quassel@gateway/tor-sasl/chexum) |
| 05:05:09 | → | [_] joins (~itchyjunk@user/itchyjunk/x-7353470) |
| 05:08:51 | × | [itchyjunk] quits (~itchyjunk@user/itchyjunk/x-7353470) (Ping timeout: 268 seconds) |
| 05:14:22 | <brettgilio> | evening all |
| 05:16:06 | × | chexum quits (~quassel@gateway/tor-sasl/chexum) (Remote host closed the connection) |
| 05:16:19 | → | chexum joins (~quassel@gateway/tor-sasl/chexum) |
| 05:24:30 | × | pastly quits (~pastly@gateway/tor-sasl/pastly) (Remote host closed the connection) |
| 05:24:53 | → | pastly joins (~pastly@gateway/tor-sasl/pastly) |
| 05:24:53 | × | gabriel_sevecek quits (~gabriel@188-167-229-200.dynamic.chello.sk) (Ping timeout: 268 seconds) |
| 05:34:24 | → | gabriel_sevecek joins (~gabriel@188-167-229-200.dynamic.chello.sk) |
| 05:50:35 | → | YoungFrog joins (~youngfrog@2a02:a03f:ca07:f900:85cf:2f10:75d0:1ac9) |
| 05:56:56 | <ski> | ello |
| 06:01:35 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 260 seconds) |
| 06:01:54 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 06:05:02 | → | bilegeek joins (~bilegeek@2600:1008:b05f:7f4e:ace3:2d9c:d35a:2195) |
| 06:09:40 | → | _ht joins (~Thunderbi@28-52-174-82.ftth.glasoperator.nl) |
| 06:13:07 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 256 seconds) |
| 06:13:39 | → | euleritian joins (~euleritia@dynamic-046-114-204-232.46.114.pool.telefonica.de) |
| 06:22:34 | → | takuan joins (~takuan@178-116-218-225.access.telenet.be) |
| 06:28:41 | → | Maeda joins (~Maeda@91-161-10-149.subs.proxad.net) |
| 06:30:10 | × | bilegeek quits (~bilegeek@2600:1008:b05f:7f4e:ace3:2d9c:d35a:2195) (Quit: Leaving) |
| 06:31:03 | → | igemnace joins (~ian@user/igemnace) |
| 06:31:29 | → | rosco joins (~rosco@175.136.152.56) |
| 06:40:45 | → | tornato joins (uid197568@id-197568.tinside.irccloud.com) |
| 06:43:26 | × | pastly quits (~pastly@gateway/tor-sasl/pastly) (Remote host closed the connection) |
| 06:43:48 | → | pastly joins (~pastly@gateway/tor-sasl/pastly) |
| 06:48:13 | × | FinnElija quits (~finn_elij@user/finn-elija/x-0085643) (Remote host closed the connection) |
| 06:48:56 | → | FinnElija joins (~finn_elij@user/finn-elija/x-0085643) |
| 06:58:19 | × | tri quits (~tri@ool-18bc2e74.dyn.optonline.net) (Ping timeout: 268 seconds) |
| 06:59:19 | <hc> | hexology: ah, makes sense |
| 07:00:11 | → | johnw joins (~johnw@69.62.242.138) |
| 07:03:33 | × | phma quits (~phma@2001:5b0:211c:d608:d6b3:ddaf:3415:a75) (Read error: Connection reset by peer) |
| 07:04:38 | → | phma joins (~phma@2001:5b0:2172:9948:cd8c:ca14:f1db:8548) |
| 07:06:09 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 07:09:35 | × | CrunchyFlakes quits (~CrunchyFl@ip92348280.dynamic.kabel-deutschland.de) (Ping timeout: 264 seconds) |
| 07:12:48 | → | CrunchyFlakes joins (~CrunchyFl@ip92348280.dynamic.kabel-deutschland.de) |
| 07:18:22 | × | shriekingnoise quits (~shrieking@186.137.175.87) (Ping timeout: 276 seconds) |
| 07:24:06 | → | sord937 joins (~sord937@gateway/tor-sasl/sord937) |
| 07:31:16 | → | pagnol joins (~user@i159006.upc-i.chello.nl) |
| 07:32:59 | → | acidjnk_new joins (~acidjnk@p200300d6e72b9326b4dc018a2c6658c2.dip0.t-ipconnect.de) |
| 07:34:47 | → | alp_ joins (~alp@2001:861:e3d6:8f80:c12e:3d55:b6:f405) |
| 07:38:38 | → | peterbecich joins (~Thunderbi@047-229-123-186.res.spectrum.com) |
| 07:39:12 | × | gdown quits (~gavin@h69-11-149-109.kndrid.broadband.dynamic.tds.net) (Remote host closed the connection) |
| 07:39:22 | × | chiselfuse quits (~chiselfus@user/chiselfuse) (Remote host closed the connection) |
| 07:39:35 | × | Pixi quits (~Pixi@user/pixi) (Ping timeout: 264 seconds) |
| 07:39:54 | → | chiselfuse joins (~chiselfus@user/chiselfuse) |
| 07:43:26 | × | ricardo1 quits (~ricardo@84.16.179.218) (Read error: Connection reset by peer) |
| 07:44:57 | → | Guest65 joins (~Guest16@136.169.59.60) |
| 07:45:35 | × | Guest65 quits (~Guest16@136.169.59.60) (Client Quit) |
| 07:45:45 | → | Guest61 joins (~Guest16@136.169.59.60) |
| 07:48:21 | × | Guest61 quits (~Guest16@136.169.59.60) (Client Quit) |
| 07:50:33 | → | pretty_dumm_guy joins (trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655) |
| 07:51:23 | → | lortabac joins (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) |
| 07:56:11 | → | Pixi joins (~Pixi@user/pixi) |
| 07:58:18 | × | Sgeo quits (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 07:58:27 | × | euleritian quits (~euleritia@dynamic-046-114-204-232.46.114.pool.telefonica.de) (Read error: Connection reset by peer) |
| 07:58:44 | → | euleritian joins (~euleritia@77.22.252.56) |
| 08:03:52 | × | dcoutts quits (~duncan@cpc69402-oxfd27-2-0-cust903.4-3.cable.virginm.net) (Ping timeout: 276 seconds) |
| 08:10:10 | → | [itchyjunk] joins (~itchyjunk@user/itchyjunk/x-7353470) |
| 08:14:07 | × | [_] quits (~itchyjunk@user/itchyjunk/x-7353470) (Ping timeout: 260 seconds) |
| 08:14:27 | → | gmg joins (~user@user/gehmehgeh) |
| 08:15:49 | → | akegalj joins (~akegalj@78-3-59-204.adsl.net.t-com.hr) |
| 08:17:13 | × | peterbecich quits (~Thunderbi@047-229-123-186.res.spectrum.com) (Ping timeout: 256 seconds) |
| 08:20:17 | → | Guest18 joins (~Guest18@41.73.1.72) |
| 08:20:18 | → | coot joins (~coot@89-69-206-216.dynamic.chello.pl) |
| 08:23:25 | × | euleritian quits (~euleritia@77.22.252.56) (Ping timeout: 268 seconds) |
| 08:23:47 | → | euleritian joins (~euleritia@dynamic-046-114-204-232.46.114.pool.telefonica.de) |
| 08:36:20 | → | ricardo1 joins (~ricardo@84.16.179.218) |
| 08:39:14 | <haskellbridge> | 12<Celestial> The IORef worked perfectly, thanks again ski, monochrom and EvanR. |
| 08:39:15 | <haskellbridge> | 12<Celestial> The only problem I now have is that I can't access the value of it in my renderer as it's not in any monad transformer with IO. I could store the value in the state manually but that would be annoying to keep track of |
| 08:42:02 | <[exa]> | Celestial: can you do with some other kind of shared var? (TVar?) |
| 08:42:22 | <[exa]> | (TVars don't require IO, just "any" kind of STM) |
| 08:43:28 | <[exa]> | anyway if the renderer doesn't modify the variable, just smash an extra Reader to the monad stack. :] |
| 08:43:38 | <haskellbridge> | 12<Celestial> the `appDraw` context is merely `ApplicationState -> [Widget ()]` |
| 08:45:16 | <[exa]> | okay with that type it can't work very easily |
| 08:46:42 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:d128:ce35:54e1:65e2) (Remote host closed the connection) |
| 08:49:17 | → | fendor joins (~fendor@2a02:8388:1605:d100:267b:1353:13d7:4f0c) |
| 08:49:52 | → | CiaoSen joins (~Jura@2a05:5800:285:a500:ca4b:d6ff:fec1:99da) |
| 08:50:15 | → | danza joins (~danza@151.19.241.170) |
| 08:52:01 | × | FinnElija quits (~finn_elij@user/finn-elija/x-0085643) (Remote host closed the connection) |
| 08:52:28 | → | FinnElija joins (~finn_elij@user/finn-elija/x-0085643) |
| 08:54:12 | <tomsmeding> | if you don't have any side effects, you'll need the functional approach to state, which is, unsurprisingly, State |
| 08:54:52 | <tomsmeding> | ah but even that wouldn't work |
| 09:03:22 | → | td_ joins (~td@i5387090E.versanet.de) |
| 09:07:34 | × | danza quits (~danza@151.19.241.170) (Ping timeout: 276 seconds) |
| 09:10:59 | × | aku quits (~aku@65.108.245.241) (Remote host closed the connection) |
| 09:11:57 | → | aku joins (~aku@65.108.245.241) |
| 09:12:20 | <ski> | why not ? |
| 09:13:43 | → | chele joins (~chele@user/chele) |
| 09:19:23 | <tomsmeding> | because the type is ApplicationState -> [Widget ()] :p |
| 09:19:30 | <tomsmeding> | there be no returned state in there |
| 09:19:52 | <tomsmeding> | oh, unless you're only reading here and the rest of the code does use the State monad with ApplicationState |
| 09:21:49 | <[Leary]> | They probably are, looks like brick to me: https://hackage.haskell.org/package/brick-2.1.1/docs/Brick-Main.html#v:appDraw |
| 09:23:29 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:d128:ce35:54e1:65e2) |
| 09:24:26 | × | myxos quits (~myxos@065-028-251-121.inf.spectrum.com) (Remote host closed the connection) |
| 09:25:09 | → | myxos joins (~myxos@065-028-251-121.inf.spectrum.com) |
| 09:25:31 | → | danza joins (~danza@151.37.255.204) |
| 09:26:20 | ski | was thinking the current `IORef' contents could be part of `ApplicationState', perhaås |
| 09:29:15 | × | ft quits (~ft@p3e9bc784.dip0.t-ipconnect.de) (Quit: leaving) |
| 09:31:18 | × | tzh quits (~tzh@c-71-193-181-0.hsd1.or.comcast.net) (Quit: zzz) |
| 09:31:46 | × | pretty_dumm_guy quits (trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655) (Ping timeout: 246 seconds) |
| 09:33:50 | → | pretty_dumm_guy joins (trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655) |
| 09:34:47 | × | tornato quits (uid197568@id-197568.tinside.irccloud.com) (Quit: Connection closed for inactivity) |
| 09:39:07 | → | __monty__ joins (~toonn@user/toonn) |
| 09:39:16 | × | danza quits (~danza@151.37.255.204) (Ping timeout: 268 seconds) |
| 09:40:19 | × | Luj quits (~Luj@mail.julienmalka.me) (Quit: Ping timeout (120 seconds)) |
| 09:40:35 | → | Luj joins (~Luj@2a01:e0a:5f9:9681:cb3c:6a2b:179a:30d3) |
| 09:43:29 | × | euleritian quits (~euleritia@dynamic-046-114-204-232.46.114.pool.telefonica.de) (Read error: Connection reset by peer) |
| 09:43:47 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 09:48:26 | → | danse-nr3 joins (~danse@151.37.255.204) |
| 09:58:22 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
| 09:58:49 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 10:01:38 | × | Guest18 quits (~Guest18@41.73.1.72) (Quit: Ping timeout (120 seconds)) |
| 10:16:05 | → | machinedgod joins (~machinedg@93-136-135-211.adsl.net.t-com.hr) |
| 10:16:28 | × | machinedgod quits (~machinedg@93-136-135-211.adsl.net.t-com.hr) (Client Quit) |
| 10:17:34 | → | machinedgod joins (~machinedg@93-136-135-211.adsl.net.t-com.hr) |
| 10:18:11 | → | idgaen joins (~idgaen@2a01:e0a:498:fd50:fcc6:bb5d:489a:ce8c) |
| 10:18:44 | × | not_reserved quits (~not_reser@45.88.222.248) (Quit: Client closed) |
| 10:19:06 | → | Lord_of_Life_ joins (~Lord@user/lord-of-life/x-2819915) |
| 10:19:40 | × | Lord_of_Life quits (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 256 seconds) |
| 10:20:03 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 10:21:04 | <dminuoso_> | Say I have a tree of labels, and a tree of patterns - now I have a notion of testing whether the PatTree matches a given LabelTree (by just checking whether they have the same shape and whether each pattern matches is structurally matching label. |
| 10:21:46 | <dminuoso_> | Labels themselves are Text, and a pattern could be either a literal "foo" (which is just a Text, that I would match against the label by equality), or a wildcard. |
| 10:22:04 | Lord_of_Life_ | is now known as Lord_of_Life |
| 10:24:35 | <dminuoso_> | Now sometimes a LabelTree and a PatTree share some structural similarity (but not straight up equality), where a PatTree is somehow larger than a LabelTree - but when you lay them ontop of each other, in the intersection they do match. |
| 10:24:39 | <dminuoso_> | What would you call this sort of relationship? |
| 10:25:21 | <dminuoso_> | I really want to call this a sort of "subtree"/"supertree" (in the sense of a subset/superset) |
| 10:25:40 | <dminuoso_> | Though that name seems to be used for branches inside a given tree already |
| 10:26:18 | <danse-nr3> | also depends on what are your plans. Will the patterns always be either literals or wildcards? Sounds unlikely. That intersection, it would be interesting to know better what it means |
| 10:27:08 | <dminuoso_> | danse-nr3: There's also the notion of a globstar (a recursive wildcard, where any "subtree" in the traditional sense is allowed). |
| 10:27:18 | <dminuoso_> | There is no plan for other patterns. |
| 10:34:27 | × | mikess quits (~sam@user/mikess) (Ping timeout: 268 seconds) |
| 10:36:35 | <danse-nr3> | i am not sure whether this is a matter of naming the relationship or thinking about the code structure. If patterns do not completely match labels, what does one do with the rest? Also, i would expect a tree to mostly match from the root up. If this is not the case, it becomes more interesting |
| 10:39:55 | × | forell quits (~forell@user/forell) (Ping timeout: 255 seconds) |
| 10:39:56 | → | jinsun_ joins (~jinsun@user/jinsun) |
| 10:39:56 | jinsun | is now known as Guest9536 |
| 10:39:57 | × | Guest9536 quits (~jinsun@user/jinsun) (Killed (silver.libera.chat (Nickname regained by services))) |
| 10:39:57 | jinsun_ | is now known as jinsun |
| 10:40:29 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 10:40:42 | → | forell joins (~forell@user/forell) |
| 10:42:29 | <dminuoso_> | Okay let me rephrase: is there a particular name for a subtree ST or T that (necessarily) shares the root of T? |
| 10:43:39 | <danse-nr3> | do subtrees always share the root? Good question |
| 10:44:12 | <danse-nr3> | no |
| 10:45:37 | <danse-nr3> | and did not find interesting results via a quick "root sharing subtree" search |
| 10:45:38 | → | hgolden_ joins (~hgolden@2603-8000-9d00-3ed1-dd4f-298a-9c49-a0ed.res6.spectrum.com) |
| 10:46:30 | <danse-nr3> | but it sounds like an useful abstraction, probably existent, maybe try #math |
| 10:47:05 | <ski> | "but when you lay them ontop of each other, in the intersection they do match" -- elaborate ? |
| 10:47:16 | → | nate4 joins (~nate@c-98-45-158-125.hsd1.ca.comcast.net) |
| 10:47:22 | × | lawt quits (~lawt@2603:c024:c008:d000:5b4f:1ef2:fed2:ef3d) (Ping timeout: 246 seconds) |
| 10:47:31 | × | hgolden quits (~hgolden@2603-8000-9d00-3ed1-dd4f-298a-9c49-a0ed.res6.spectrum.com) (Read error: Connection reset by peer) |
| 10:47:36 | <danse-nr3> | label tree is a subset of pattern tree including the root |
| 10:47:55 | → | lawt joins (~lawt@2603:c024:c008:d000:5b4f:1ef2:fed2:ef3d) |
| 10:48:05 | <danse-nr3> | a subtree to be more precise |
| 10:48:44 | <ski> | "a subtree ST or T that (necessarily) shares the root of T" -- sounds maybe related to the notion of "bar" |
| 10:49:14 | <danse-nr3> | a more searchable term? "tree bar"? |
| 10:49:16 | <ski> | dminuoso_ ^ |
| 10:51:24 | <ski> | Brouwer's "bar induction/recursion" is about having a tree with all branches infinite, but each path from the root eventually becomes constant (the elements in the nodes), and so there's a "bar", crossing every path from the root, so that after the bar, each path is definitely constant |
| 10:51:39 | <danse-nr3> | cheers |
| 10:52:00 | × | nate4 quits (~nate@c-98-45-158-125.hsd1.ca.comcast.net) (Ping timeout: 252 seconds) |
| 10:52:40 | <ski> | (so, you can represent such an infinite tree with a finite tree, down to the bar, and in the leaves you put the element that repeats forever from there .. and you can also put some "result" for every path through that leaf) |
| 10:53:11 | <dminuoso_> | ski: Take any given tree, call it T, it has the root R. Now, T may have a number of subtrees ST. But Im not interested in every subtree, but precisely those subtrees that have the same root R that T has. |
| 10:54:09 | <danse-nr3> | yes that does seem to relate to bars |
| 10:54:55 | <dminuoso_> | If I flip the relationship around, I might call T an extension of ST maybe. |
| 10:54:58 | <ski> | specifically, a (computable) function from `Stream Bool'/`Nat -> Bool' to some finite datatype (e.g. `Bool') could be argued to only look at a finite prefix of its input stream, before deciding on its output (because otherwise it would require looking at infinite information in finite time). and so, we can visualize such a function as an infinite tree, with a bar, with leaves indicating the finite result |
| 10:55:04 | <ski> | value for each path passing through that leaf (corresponding to a bar node) |
| 10:55:04 | <ski> | this is related to |
| 10:55:07 | <ski> | @where impossible |
| 10:55:08 | <lambdabot> | <http://math.andrej.com/2007/09/28/seemingly-impossible-functional-programs/>,<http://math.andrej.com/2008/11/21/a-haskell-monad-for-infinite-search-in-finite-time/> |
| 10:55:56 | <ski> | (you could take streams of other types as input, getting a different branching factor in the trees) |
| 10:56:44 | <ski> | dminuoso_ : i'm still wondering about the "intersection" part, what you mean by that |
| 10:57:02 | <ski> | was that about the "globstar" patterns, or something else ? |
| 10:57:14 | <dminuoso_> | Okay, so let me reduce the problem slightly. |
| 10:57:27 | ncf | . o O ( uniform continuity ) |
| 10:58:09 | <dminuoso_> | Say I have domain names. Domain names are lists of labels ["www", "google", "de"]. Now I may want to specify on what domain names one may operator by describing a pattern [Glob, Lit "google", Lit "de"] |
| 10:58:20 | ski | would possibly also parameterize, so `LabelTree = Tree Label' and `PatTree = Tree Pat' .. or maybe something with zippers for the latter, due to "globstar" |
| 10:58:22 | <dminuoso_> | Instead of trees, this is lists now. |
| 10:58:59 | <ski> | you want to build like tries ? |
| 10:59:22 | <dminuoso_> | I do build a lot of tries at the end, yes. |
| 10:59:37 | <dminuoso_> | So given this simplified version, in some situations I might pose the question "is the pattern *.google.de something inside the google.de zone" |
| 11:00:12 | <dminuoso_> | Which becomes just checking whether the domain is a suffix of the pattern |
| 11:01:17 | <ski> | hm, maybe the terms "crop" or "extend" could be useful, wrt these trees |
| 11:01:37 | <ski> | one tree being a cropped/pruned version of the other, or the other being an extended version of the first |
| 11:03:00 | <danse-nr3> | it would be interesting to check which terms Brouwer used, maybe there is already a "pruned" |
| 11:03:01 | <dminuoso_> | ski: cropped/pruned doesnt sound all too bad. Or maybe I should just do the math thing and make something up, like "rooted subtree", define it in a note somewhere, and put a bunch of "See Note [Rooted Subtree]" all over the place. |
| 11:04:52 | <ski> | data Tree b e a = Leaf a | Node e (b (Tree b e a)) |
| 11:05:20 | <ski> | type LabelTree e a = Tree (Map Text) e a |
| 11:06:10 | <dminuoso_> | But yeah, Im beginning to see the similarity to Brouwers work here. |
| 11:06:32 | <ski> | type PatTree e a = Tree (Map (Maybe (Either Label Text))) e (Either Label a) |
| 11:06:39 | <ski> | something along those lines, maybe |
| 11:07:30 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
| 11:07:34 | <ski> | (`a' for making it a `Monad') |
| 11:08:10 | → | euleritian joins (~euleritia@dynamic-046-114-204-232.46.114.pool.telefonica.de) |
| 11:08:33 | × | euleritian quits (~euleritia@dynamic-046-114-204-232.46.114.pool.telefonica.de) (Read error: Connection reset by peer) |
| 11:08:50 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 11:11:10 | <ski> | hm |
| 11:11:38 | <ski> | type PatTree e = Tree (Map (Maybe (Either Label Text))) e Label -- perhaps instead |
| 11:12:15 | <ski> | then doing `patTree >>= subst' replaces the `Label' leaves according to `subst :: Label -> PatTree e' |
| 11:12:16 | → | Joao003 joins (~Joao003@190.108.99.32) |
| 11:14:29 | → | kritzefitz_ joins (~kritzefit@debian/kritzefitz) |
| 11:15:09 | × | kritzefitz quits (~kritzefit@debian/kritzefitz) (Ping timeout: 256 seconds) |
| 11:15:55 | × | gabriel_sevecek quits (~gabriel@188-167-229-200.dynamic.chello.sk) (Ping timeout: 255 seconds) |
| 11:19:21 | kritzefitz_ | is now known as kritzefitz |
| 11:20:32 | → | gabriel_sevecek joins (~gabriel@188-167-229-200.dynamic.chello.sk) |
| 11:22:43 | × | lortabac quits (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Ping timeout: 246 seconds) |
| 11:25:41 | → | yaroot_ joins (~yaroot@2400:4052:ac0:d901:1cf4:2aff:fe51:c04c) |
| 11:25:45 | × | yaroot quits (~yaroot@p2987138-ipngn7501souka.saitama.ocn.ne.jp) (Read error: Connection reset by peer) |
| 11:25:46 | yaroot_ | is now known as yaroot |
| 11:29:47 | <danse-nr3> | my ADA doubled in value since november |
| 11:31:46 | <ski> | you're coding Ada ? |
| 11:32:54 | <danse-nr3> | no, unfortunately blockchain tech is not easy to approach without previous experience, and i have heard that doing that in haskell is not the easiest. I just bought a small amount of them |
| 11:32:55 | × | pastly quits (~pastly@gateway/tor-sasl/pastly) (Ping timeout: 240 seconds) |
| 11:33:28 | <ski> | mhm |
| 11:34:29 | → | pastly joins (~pastly@gateway/tor-sasl/pastly) |
| 11:34:29 | × | machinedgod quits (~machinedg@93-136-135-211.adsl.net.t-com.hr) (Ping timeout: 240 seconds) |
| 11:40:29 | × | phma quits (~phma@2001:5b0:2172:9948:cd8c:ca14:f1db:8548) (Read error: Connection reset by peer) |
| 11:41:16 | → | phma joins (~phma@host-67-44-208-181.hnremote.net) |
| 11:41:39 | → | cfricke joins (~cfricke@user/cfricke) |
| 11:44:28 | → | eayus joins (~eayus@8afbc74e.st-andrews.ac.uk) |
| 11:48:19 | → | lortabac joins (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) |
| 11:49:31 | <eayus> | Using Data.Data/Data.Typeable, is it possible to `cast` to a polymorphic type (introducing some existential type variables perhaps). |
| 11:49:32 | <eayus> | For example, suppose I wanted to transform all `Maybe`s in a term to `Nothing`, regardless of what type `Maybe` is instantiated with. Does anyone know how I might acheive this? |
| 11:51:14 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
| 11:51:49 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 11:52:21 | <dminuoso_> | :t Nothing |
| 11:52:22 | <lambdabot> | Maybe a |
| 11:52:25 | <dminuoso_> | eayus: It's already builtin. |
| 11:52:37 | <dminuoso_> | That is, Nothing *is* already polymorphic. |
| 11:52:51 | <dminuoso_> | Keep in mind that a "polymorphic type" means something else, namely one that is polymorphic in its kind. |
| 11:53:12 | <dminuoso_> | (You probably meant to say quantified type instead) |
| 11:53:38 | <dminuoso_> | eayus: The bigger question I have is what you mean by "transform" and "term" exactly. |
| 11:56:33 | × | xdej quits (~xdej@quatramaran.salle-s.org) (Remote host closed the connection) |
| 11:57:36 | <ski> | (a universal type (a `forall'-type) is also quite distinct from an existential type (an `exists'-type)) |
| 11:57:54 | <ski> | (but perhaps by "existential type variables", you really meant "meta-variables" or something ..) |
| 11:58:00 | <eayus> | Perhaps I misexplained my problem. Using Data.Data and Data.Typeable, I can generically transform any data type which implements those classes. For example I could increment all `Int`s using `gmapT`, and `cast`, without knowing what type I am working on. I want to make a similar generic function which turns all `Maybe`s into `Nothing`s. |
| 11:58:01 | <eayus> | The issue is that `cast` requires a concrete type, but I want to transform any `Maybe` regardless of what type it is instantiated with |
| 11:58:33 | <eayus> | By existential type variables I mean a variable which is "forall" quantified with a constructor |
| 11:58:36 | <dminuoso_> | :t cast |
| 11:58:37 | <lambdabot> | (Typeable a, Typeable b) => a -> Maybe b |
| 11:58:46 | <ski> | @type gcast |
| 11:58:47 | <lambdabot> | forall k (a :: k) (b :: k) (c :: k -> *). (Typeable a, Typeable b) => c a -> Maybe (c b) |
| 11:59:44 | <ski> | eayus : that would be a universal type variable, then. (`forall' means universal quantification. `exists' means existential quantification) |
| 12:00:41 | <lortabac> | well, forall in Haskell syntax also means existential quantification |
| 12:00:59 | <ski> | .. but if you mean `data SomeFoo = forall a. Cxt a => WrapFoo (Foo a)', then `WrapFoo' is polymorphic, having type `forall a. Cxt a => Foo a -> SomeFoo', but that's equivalent to `(exists a. Cxt a *> Foo a) -> SomeFoo', so `SomeFoo' amounts to `exists a. Cxt a *> Foo a' here |
| 12:01:08 | <ski> | lortabac : it doesn't |
| 12:01:53 | <ski> | `WrapFoo' is polymorphic, has a universally quantified type. it's not "abstract(ed)". its *argument* could be said to be abstract(ed) (as in abstract data types) |
| 12:02:58 | <ski> | (also, imho, the extension name `ExistentialQuantification' is a misnomer. a better (more accurate) name might be perhaps `ExistentialConstructors' .. i'd want to reserve `ExistentialQuantification' for if we ever get an actual `exists' syntax (distinct from the aforementioned extension)) |
| 12:03:39 | <ski> | (also, that extension isn't the only way to encode existentials. the other way is using `Rank2Types', as `forall o. (forall a. Cxt a => Foo a -> o) -> o') |
| 12:05:30 | <ski> | (if you're saying the `forall' there at `WrapFoo' means existentials, you could also say the `forall' in `length :: forall a. [a] -> Int' means existentials, because this is equivalent to `length :: (exists a. [a]) -> Int'. saying that for any type `a', `length' can take a list of `a's and returns an `Int', is the same as saying that `length' returns an `Int', as long as there exists some type `a' such that |
| 12:05:36 | <ski> | you apply `length' to a list of `a's) |
| 12:05:45 | → | waleee joins (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) |
| 12:11:28 | <lortabac> | I see what you mean |
| 12:12:46 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 246 seconds) |
| 12:13:00 | <lortabac> | I was trying to understand what eayus said. It seems they are referring to ExistentialQuantification |
| 12:13:32 | → | euleritian joins (~euleritia@dynamic-046-114-204-232.46.114.pool.telefonica.de) |
| 12:13:43 | <eayus> | I was referring to the use of a forall in a type constructor, as described here: https://wiki.haskell.org/Existential_type |
| 12:13:56 | <eayus> | I.e. pattern matching introduces a type variable |
| 12:17:04 | <Joao003> | can i ask for context? |
| 12:18:55 | × | danse-nr3 quits (~danse@151.37.255.204) (Ping timeout: 255 seconds) |
| 12:23:19 | <eayus> | I want to find all free variables in an AST. Rather than write the recursion manually introducing a lot of boiler plate, it makes sense to do a generic traversal. |
| 12:23:20 | <eayus> | The idea is to introduce a `Binder` type used whenever a avariable is bound. This can be identified by the generic traversal to make sure that variable is not classified as free. |
| 12:23:20 | <eayus> | If `Binder` has kind `*`, I can use `cast` to tell whether im looking at a binder. However, sometimes I'm binding different things of different type, so `Binder` needs to be of type `* -> *`. |
| 12:23:21 | <eayus> | This is what causes the problem, as I can no longer use `cast` to tell whether I'm looking at a `Binder` |
| 12:23:27 | × | euleritian quits (~euleritia@dynamic-046-114-204-232.46.114.pool.telefonica.de) (Read error: Connection reset by peer) |
| 12:23:44 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 12:24:37 | × | pagnol quits (~user@i159006.upc-i.chello.nl) (Remote host closed the connection) |
| 12:24:54 | <eayus> | Here is an example with a non polymorphic binder: https://paste.tomsmeding.com/wf5s1TQj |
| 12:25:47 | × | Joao003 quits (~Joao003@190.108.99.32) (Read error: Connection reset by peer) |
| 12:26:07 | × | waleee quits (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) (Ping timeout: 256 seconds) |
| 12:29:05 | <dminuoso_> | "free variables in an AST" |
| 12:30:20 | <dminuoso_> | eayus: Mind my asking, any particular reason you arent using say unbound? |
| 12:34:03 | → | Joao003 joins (~Joao003@190.108.99.207) |
| 12:35:48 | <eayus> | It's an option though it seems using bound/unbound would limit my generic programming to only variable related stuff. I might want to also do a generic traversal when normalising terms for example |
| 12:38:04 | <ski> | hm. sounds like you want something like `someCast :: (Typeable a,Typeable f) => a -> Maybe (Some f)' |
| 12:38:14 | <eayus> | yeah exactly |
| 12:39:56 | <ski> | (so, you don't want to cast to a universal type (getting a polymorphic value), but you do want to cast to an existential type (getting an abstracted value)) |
| 12:40:24 | ski | decides to try using "abstracted" for these, for a while |
| 12:42:49 | → | danse-nr3 joins (~danse@151.19.230.254) |
| 12:48:00 | <eayus> | Another approach I've considered is using the Functor/Fix pattern. |
| 12:48:01 | <eayus> | Perhaps defining the AST as a type like |
| 12:48:01 | <eayus> | `data ExprF ( binder :: ( * -> * ) -> * ) ( expr :: * )`. |
| 12:48:02 | <eayus> | `data Binder ( f :: * -> * ) = Binder Name (f Expr)` |
| 12:48:02 | <eayus> | `type Expr = Fix (ExprF Binder)` |
| 12:48:24 | → | alexherbo2 joins (~alexherbo@2a02-8440-3341-aec3-516d-6fbd-7275-d6e8.rev.sfr.net) |
| 12:49:18 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 12:50:23 | <eayus> | For `ExprF` i can derive functor, though I would have to write something like this manually maybe |
| 12:50:24 | <eayus> | `f :: (forall f. Functor f => Binder f -> Binder f) -> ExprF binder expr -> ExprF binder expr` |
| 12:51:39 | <eayus> | That's incorrect actually, this instead: |
| 12:51:40 | <eayus> | `_ :: (forall f. Functor f => binder f -> binder f) -> ExprF binder expr -> ExprF binder expr` |
| 12:54:22 | <poscat> | Anyone using the ghc package provided by fedora? Why I'm I unable to use the :doc command? (it says "Try re-compiling with '-haddock'.") |
| 12:57:23 | <danse-nr3> | could be that ghc was not compiled with -haddock, although i think it refers to the specific haskell package you want to query the docs about, therefore it should not matter that you are using a fedora ghc package |
| 13:03:47 | × | Joao003 quits (~Joao003@190.108.99.207) (Remote host closed the connection) |
| 13:03:58 | → | dcoutts joins (~duncan@cpc69402-oxfd27-2-0-cust903.4-3.cable.virginm.net) |
| 13:04:11 | → | Joao003 joins (~Joao003@190.108.99.207) |
| 13:08:20 | → | eayus70 joins (~eayus@8afbc74e.st-andrews.ac.uk) |
| 13:09:04 | × | eayus quits (~eayus@8afbc74e.st-andrews.ac.uk) (Ping timeout: 250 seconds) |
| 13:11:58 | × | CiaoSen quits (~Jura@2a05:5800:285:a500:ca4b:d6ff:fec1:99da) (Ping timeout: 276 seconds) |
| 13:12:19 | × | bitdex quits (~bitdex@gateway/tor-sasl/bitdex) (Quit: = "") |
| 13:16:53 | → | hamster joins (~ham@user/ham) |
| 13:18:50 | → | ircbrowse_tom joins (~ircbrowse@2a01:4f8:1c1c:9319::1) |
| 13:18:56 | Server | sets mode +Cnt |
| 13:27:20 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 13:27:31 | <eayus70> | Ok, for anyone curious, I think i've managed to find a solution to my earlier problem. The idea is to not have an explicit binder type, but use the structure of the AST to encode where a variable is bound. |
| 13:27:32 | <eayus70> | Everything to the right of a binding name in the AST will have that name in scope. A function such as free variable computation can be implemented by folding over the constructors arguments |
| 13:27:33 | → | sawilagar joins (~sawilagar@user/sawilagar) |
| 13:28:00 | → | bonaogeto joins (~bonaogeto@105.163.158.10) |
| 13:29:47 | <Joao003> | is there any function to clear the terminal output? |
| 13:30:01 | <danse-nr3> | C-l? |
| 13:30:35 | × | bonaogeto quits (~bonaogeto@105.163.158.10) (Client Quit) |
| 13:30:44 | <Joao003> | wdym? |
| 13:31:00 | <danse-nr3> | press Control and l at the same time |
| 13:31:18 | <eayus70> | `clearScreen` from ansi-terminal package maybe |
| 13:31:24 | <Joao003> | i want a haskell function to clear terminal output, bruh |
| 13:35:09 | <ncf> | putStr "\ESC[H\ESC[2J" |
| 13:35:20 | <ncf> | (not portable) |
| 13:40:43 | → | tri joins (~tri@ool-18bc2e74.dyn.optonline.net) |
| 13:43:05 | <ski> | % System.Cmd.system "tput clear" |
| 13:43:05 | <yahb2> | tput: No value for $TERM and no -T specified ; ExitFailure 2 |
| 13:43:37 | <Joao003> | this isn't really portable |
| 13:45:22 | × | tri quits (~tri@ool-18bc2e74.dyn.optonline.net) (Ping timeout: 256 seconds) |
| 13:45:52 | <Rembane> | Joao003: Which platforms do you need to support? |
| 13:46:16 | <Joao003> | i just want the most reliable way to clear screen, Rembane |
| 13:46:43 | <exarkun> | There is not one uniform "terminal" though. It is completely true that there is no one single way to clear any arbitrary terminal. |
| 13:46:52 | <Joao003> | true |
| 13:46:59 | <Joao003> | i use windows tho |
| 13:47:21 | <exarkun> | Windows isn't a terminal. It isn't even a terminal emulator. ;) |
| 13:47:43 | <Joao003> | yes ik, but for cmd.exe, what is a reliable tool to clear its console? |
| 13:48:10 | <exarkun> | "cls" |
| 13:48:11 | <Rembane> | Joao003: print "cls\n" and see what happens. :) |
| 13:48:42 | <Joao003> | just prints cls |
| 13:49:02 | <eayus70> | I think powershell and console apps are ANSI compatible if you dont mind using them instead of the old command prompt |
| 13:49:20 | <Joao003> | yeah, cmd.exe is 30 yrs old |
| 13:49:44 | <eayus70> | Maybe `system "cls"` |
| 13:49:47 | <eayus70> | https://hackage.haskell.org/package/process-1.0.1.3/docs/System-Cmd.html |
| 13:50:45 | <mauke> | putStr (replicate 9999 '\n') |
| 13:51:34 | <Joao003> | works, but slow |
| 13:51:50 | <Joao003> | maybe a 150 is enough |
| 13:51:58 | <Joao003> | or even just 100 |
| 13:52:07 | × | rvalue quits (~rvalue@user/rvalue) (Read error: Connection reset by peer) |
| 13:52:26 | → | rvalue joins (~rvalue@user/rvalue) |
| 13:52:58 | <Joao003> | afaik, most people don't have 9999-line high monitors |
| 13:53:59 | <eayus70> | I belive this wont put the cursor at the top however |
| 13:54:15 | <eayus70> | so it is different to "cls" functionally |
| 13:54:19 | <Joao003> | yeah |
| 13:54:28 | <Joao003> | i just tested it |
| 13:55:32 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
| 13:55:43 | → | thegeekinside joins (~thegeekin@189.217.90.224) |
| 13:55:43 | × | igemnace quits (~ian@user/igemnace) (Read error: Connection reset by peer) |
| 13:55:49 | → | shriekingnoise joins (~shrieking@186.137.175.87) |
| 13:55:57 | → | euleritian joins (~euleritia@dynamic-046-114-204-232.46.114.pool.telefonica.de) |
| 13:59:05 | <ski> | eayus70 : did you try `system' ? |
| 13:59:28 | <Joao003> | <interactive>:9:1: error: Variable not in scope: system |
| 13:59:43 | <Joao003> | % system "clear" |
| 13:59:43 | <yahb2> | <interactive>:45:1: error: ; Variable not in scope: system :: String -> t |
| 13:59:48 | <Joao003> | lol |
| 13:59:55 | <eayus70> | You neen to add the "process" package |
| 13:59:55 | <ski> | <ski> % System.Cmd.system "tput clear" |
| 14:00:20 | <Joao003> | how? using cabal? i don't like using package managers |
| 14:00:37 | <eayus70> | Yeah using cabal |
| 14:01:05 | <ski> | Joao003 : `:set -package process' in GHCi |
| 14:01:34 | <Joao003> | still same error |
| 14:01:36 | <ski> | (or `ghci -package process', when you start it, also works) |
| 14:01:48 | <ski> | you also need to qualify the module path |
| 14:01:55 | <ski> | (or import the module) |
| 14:02:10 | <ski> | % System.Cmd.system "cls" |
| 14:02:10 | <yahb2> | /bin/sh: 1: cls: not found ; ExitFailure 127 |
| 14:02:15 | <ski> | % System.Cmd.system "tput clear" |
| 14:02:15 | <yahb2> | tput: No value for $TERM and no -T specified ; ExitFailure 2 |
| 14:06:09 | <Joao003> | have you ever used (,,) |
| 14:07:21 | → | eayus joins (~eayus@8afbc74e.st-andrews.ac.uk) |
| 14:07:30 | <danse-nr3> | yeah |
| 14:07:46 | <Joao003> | i imagine it being used for a 3d point |
| 14:07:59 | <Joao003> | what about a (,,,) |
| 14:08:17 | <danse-nr3> | the longer, the worse |
| 14:08:21 | <Joao003> | lol |
| 14:08:30 | <Joao003> | ghc supports (,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,) |
| 14:08:40 | <Joao003> | aka a 64-plet |
| 14:08:46 | <ski> | % :ǃ uname -a |
| 14:08:46 | <yahb2> | Linux play-haskell 6.6.2-arch1-1 #1 SMP PREEMPT_DYNAMIC Mon, 20 Nov 2023 23:18:21 +0000 x86_64 x86_64 x86_64 GNU/Linux |
| 14:09:15 | <Joao003> | % :q |
| 14:09:15 | <yahb2> | <bye> |
| 14:09:17 | <Joao003> | lol |
| 14:09:21 | <Joao003> | % 1 |
| 14:09:21 | <yahb2> | 1 |
| 14:10:36 | × | eayus70 quits (~eayus@8afbc74e.st-andrews.ac.uk) (Ping timeout: 250 seconds) |
| 14:13:34 | → | igemnace joins (~ian@user/igemnace) |
| 14:16:22 | <Joao003> | why do type definitions use () instead of Unit? |
| 14:17:11 | <ski> | it's the empty tuple type |
| 14:17:11 | → | edr joins (~edr@user/edr) |
| 14:17:38 | <Joao003> | @hoogle Unit |
| 14:17:39 | <lambdabot> | GHC.Tuple data Unit a |
| 14:17:39 | <lambdabot> | GHC.Tuple Unit :: a -> Unit a |
| 14:17:39 | <lambdabot> | module Graphics.Rendering.Chart.Axis.Unit |
| 14:17:56 | <Joao003> | @hoogle () |
| 14:17:56 | <lambdabot> | GHC.Tuple data () |
| 14:17:56 | <lambdabot> | GHC.Tuple () :: () |
| 14:18:02 | <Joao003> | different... |
| 14:18:21 | <ski> | in the MLs, tuple types `(T,U,V)' are spelled `t * u * v'. the empty tuple type `()' is spelled `unit' |
| 14:18:53 | <ski> | yea, that `Unit' is the "unituple type", a tuple with one component, not zero components (which is what `() |
| 14:18:56 | <ski> | ' has) |
| 14:19:53 | <Joao003> | lemme copy from hackage: "The unit datatype Unit has one non-undefined member, the nullary constructor ()." |
| 14:19:56 | <ski> | - {1 = 2,2 = 1}; |
| 14:19:57 | <ski> | val it = (2,1) : int * int |
| 14:20:10 | <ski> | - {1 = 2}; |
| 14:20:12 | <ski> | val it = {1=2} : {1:int} |
| 14:20:21 | <ski> | - {}; |
| 14:20:23 | <Joao003> | what's t hat |
| 14:20:23 | <ski> | val it = () : unit |
| 14:20:26 | <ski> | that's SML |
| 14:20:40 | <ski> | tuples are records, with field names being positive integers |
| 14:21:22 | <ski> | "The unit datatype Unit has one non-undefined member, the nullary constructor ()." -- that's about the `()' type, not the `Unit' type above in `GHC.Tuple' |
| 14:22:22 | <Joao003> | It says "data Unit" and also says that one of its constructors is () |
| 14:22:43 | <ski> | where ? |
| 14:22:58 | <Joao003> | https://hackage.haskell.org/package/ghc-prim-0.11.0/docs/GHC-Tuple-Prim.html |
| 14:23:45 | × | danse-nr3 quits (~danse@151.19.230.254) (Ping timeout: 252 seconds) |
| 14:24:05 | <Joao003> | also, isn't Solo the 1-tuple datatype? |
| 14:25:15 | <ski> | ok, i suppose `GHC.Tuple.Unit' was renamed into `GHC.Tuple.Solo' |
| 14:25:30 | <ski> | it says "Since: ghc-prim-0.11.0" |
| 14:25:44 | <Joao003> | oh |
| 14:25:47 | <ski> | so it looks like that was probably recently |
| 14:25:58 | <Joao003> | yeah |
| 14:34:04 | <ski> | % $(return (TupE [])) |
| 14:34:04 | <yahb2> | () |
| 14:34:08 | <ski> | % $(return (TupE [Just (VarE 'otherwise)])) |
| 14:34:09 | <yahb2> | Solo True |
| 14:34:13 | <ski> | % :t $(return (TupE [Nothing])) |
| 14:34:13 | <yahb2> | $(return (TupE [Nothing])) :: t -> Solo t |
| 14:34:33 | <Joao003> | the solo type is the most useless thing ever |
| 14:37:28 | × | alexherbo2 quits (~alexherbo@2a02-8440-3341-aec3-516d-6fbd-7275-d6e8.rev.sfr.net) (Ping timeout: 250 seconds) |
| 14:38:21 | <ski> | % case $(return (UnboxedTupE [Just (VarE 'otherwise)])) of (# b #) -> b |
| 14:38:21 | <yahb2> | True |
| 14:38:23 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 14:38:29 | <ski> | % case $(return (UnboxedTupE [])) of (# #) -> b |
| 14:38:29 | <yahb2> | <interactive>:75:45: error: Variable not in scope: b |
| 14:38:33 | <ski> | % case $(return (UnboxedTupE [])) of (# #) -> () |
| 14:38:33 | <yahb2> | () |
| 14:38:41 | <ski> | % case $(return (UnboxedSumE (VarE 'otherwise) 1 2)) of (# x | #) -> Left x; (# | y #) -> Right y |
| 14:38:41 | <yahb2> | Left True |
| 14:38:45 | <ski> | % case $(return (UnboxedSumE (VarE 'otherwise) 2 2)) of (# x | #) -> Left x; (# | y #) -> Right y |
| 14:38:45 | <yahb2> | Right True |
| 14:39:40 | → | waleee joins (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) |
| 14:39:44 | × | alp_ quits (~alp@2001:861:e3d6:8f80:c12e:3d55:b6:f405) (Ping timeout: 256 seconds) |
| 14:40:05 | <Joao003> | ski? |
| 14:42:50 | <ski> | hm ? |
| 14:43:36 | → | alexherbo2 joins (~alexherbo@2a02-8440-3341-aec3-516d-6fbd-7275-d6e8.rev.sfr.net) |
| 14:44:23 | × | waleee quits (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) (Ping timeout: 264 seconds) |
| 14:47:05 | <Joao003> | say one thing we need in ghc |
| 14:47:55 | <Joao003> | i think better error messages are needed |
| 14:48:01 | <ski> | @ghc |
| 14:48:01 | <lambdabot> | For basic information, try the `--help' option. |
| 14:48:10 | <ski> | @ghc |
| 14:48:11 | <lambdabot> | the eta-reduction property does not hold |
| 14:48:26 | → | nate4 joins (~nate@c-98-45-158-125.hsd1.ca.comcast.net) |
| 14:48:48 | <Joao003> | @ghc |
| 14:48:48 | <lambdabot> | Can't mix generic and non-generic equations for class method |
| 14:49:13 | <Joao003> | this bot can mock ghc lol |
| 14:49:37 | <Joao003> | @help ghc |
| 14:49:37 | <lambdabot> | ghc. Choice quotes from GHC. |
| 14:49:47 | <Joao003> | @ghc |
| 14:49:47 | <lambdabot> | eval_thunk_selector: strange selectee |
| 14:49:57 | <Joao003> | i'm really thonking |
| 14:50:02 | <Joao003> | @ghc |
| 14:50:02 | <lambdabot> | Can't happen |
| 14:50:14 | <Joao003> | will never happen |
| 14:50:15 | <Joao003> | @ghc |
| 14:50:15 | <lambdabot> | No explicit method nor default method |
| 14:50:20 | <Joao003> | @ghc |
| 14:50:20 | <lambdabot> | On Alpha, I can only handle 4 non-floating-point arguments to foreign export dynamic |
| 14:50:25 | <Joao003> | @ghc |
| 14:50:25 | <lambdabot> | GHCi's bytecode generation machinery can't handle 64-bit code properly yet. |
| 14:50:30 | <Joao003> | @ghc |
| 14:50:30 | <lambdabot> | Use -fglasgow-exts to allow multi-parameter classes |
| 14:50:47 | <Joao003> | @ghc |
| 14:50:47 | <lambdabot> | Inferred type is less polymorphic than expected |
| 14:52:04 | <Joao003> | @help |
| 14:52:04 | <lambdabot> | help <command>. Ask for help for <command>. Try 'list' for all commands |
| 14:52:08 | <Joao003> | @list |
| 14:52:08 | <lambdabot> | What module? Try @listmodules for some ideas. |
| 14:52:13 | <Joao003> | @help list |
| 14:52:13 | <lambdabot> | list [module|command]. Show commands for [module] or the module providing [command]. |
| 14:53:22 | × | nate4 quits (~nate@c-98-45-158-125.hsd1.ca.comcast.net) (Ping timeout: 256 seconds) |
| 14:57:47 | → | Square2 joins (~Square4@user/square) |
| 14:58:00 | → | danza joins (~danza@151.19.230.254) |
| 15:01:00 | → | blastoise joins (~blastoise@205.185.193.149) |
| 15:01:15 | → | flounders joins (~flounders@24.246.176.178) |
| 15:03:23 | × | danza quits (~danza@151.19.230.254) (Ping timeout: 260 seconds) |
| 15:09:03 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 15:09:16 | × | euleritian quits (~euleritia@dynamic-046-114-204-232.46.114.pool.telefonica.de) (Read error: Connection reset by peer) |
| 15:09:33 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 15:10:14 | → | danse-nr3 joins (~danse@151.35.255.237) |
| 15:12:08 | × | eayus quits (~eayus@8afbc74e.st-andrews.ac.uk) (Ping timeout: 250 seconds) |
| 15:12:31 | × | stiell quits (~stiell@gateway/tor-sasl/stiell) (Ping timeout: 240 seconds) |
| 15:15:18 | × | alexherbo2 quits (~alexherbo@2a02-8440-3341-aec3-516d-6fbd-7275-d6e8.rev.sfr.net) (Remote host closed the connection) |
| 15:15:31 | → | Sgeo joins (~Sgeo@user/sgeo) |
| 15:15:49 | → | stiell joins (~stiell@gateway/tor-sasl/stiell) |
| 15:16:05 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 240 seconds) |
| 15:16:51 | → | euleritian joins (~euleritia@dynamic-046-114-204-232.46.114.pool.telefonica.de) |
| 15:19:40 | → | alexherbo2 joins (~alexherbo@2a02-8440-3341-aec3-516d-6fbd-7275-d6e8.rev.sfr.net) |
| 15:23:27 | × | euleritian quits (~euleritia@dynamic-046-114-204-232.46.114.pool.telefonica.de) (Read error: Connection reset by peer) |
| 15:23:44 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 15:25:20 | × | akegalj quits (~akegalj@78-3-59-204.adsl.net.t-com.hr) (Ping timeout: 252 seconds) |
| 15:26:08 | × | califax quits (~califax@user/califx) (Remote host closed the connection) |
| 15:26:54 | → | akegalj joins (~akegalj@78-1-93-196.adsl.net.t-com.hr) |
| 15:27:44 | → | califax joins (~califax@user/califx) |
| 15:29:51 | × | alexherbo2 quits (~alexherbo@2a02-8440-3341-aec3-516d-6fbd-7275-d6e8.rev.sfr.net) (Remote host closed the connection) |
| 15:30:27 | × | dwt_ quits (~dwt_@2601:2c6:8381:e5c:606f:34a3:7300:6f05) (Ping timeout: 260 seconds) |
| 15:30:34 | × | cimento quits (CO2@gateway/vpn/protonvpn/cimento) (Ping timeout: 260 seconds) |
| 15:31:10 | → | alexherbo2 joins (~alexherbo@2a02-8440-3341-aec3-516d-6fbd-7275-d6e8.rev.sfr.net) |
| 15:32:06 | → | dwt_ joins (~dwt_@2601:2c6:8381:e5c:c917:e876:d8ba:f05f) |
| 15:34:02 | → | alp_ joins (~alp@2001:861:e3d6:8f80:66b0:842b:748c:f4e2) |
| 15:35:21 | × | akegalj quits (~akegalj@78-1-93-196.adsl.net.t-com.hr) (Ping timeout: 245 seconds) |
| 15:39:03 | → | cimento joins (CO2@gateway/vpn/protonvpn/cimento) |
| 15:40:31 | × | chiselfuse quits (~chiselfus@user/chiselfuse) (Ping timeout: 240 seconds) |
| 15:42:22 | → | akegalj joins (~akegalj@95.168.120.43) |
| 15:43:05 | → | chiselfuse joins (~chiselfus@user/chiselfuse) |
| 15:46:52 | → | xdej joins (~xdej@quatramaran.salle-s.org) |
| 15:50:14 | → | mmhat joins (~mmh@p200300f1c702cd13ee086bfffe095315.dip0.t-ipconnect.de) |
| 15:50:27 | × | akegalj quits (~akegalj@95.168.120.43) (Read error: Connection reset by peer) |
| 15:53:21 | × | lortabac quits (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Quit: WeeChat 4.1.1) |
| 15:53:57 | → | Fischmiep joins (~Fischmiep@user/Fischmiep) |
| 15:59:45 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 268 seconds) |
| 16:01:08 | × | cfricke quits (~cfricke@user/cfricke) (Quit: WeeChat 4.0.5) |
| 16:02:16 | × | mmhat quits (~mmh@p200300f1c702cd13ee086bfffe095315.dip0.t-ipconnect.de) (Ping timeout: 276 seconds) |
| 16:02:38 | → | mmhat joins (~mmh@p200300f1c702cdcaee086bfffe095315.dip0.t-ipconnect.de) |
| 16:03:24 | → | Pixi` joins (~Pixi@user/pixi) |
| 16:03:50 | → | mikess joins (~sam@user/mikess) |
| 16:05:59 | × | Pixi quits (~Pixi@user/pixi) (Ping timeout: 264 seconds) |
| 16:06:10 | <Joao003> | i hate the fact that there's min and minimum |
| 16:06:42 | <danse-nr3> | > %t min |
| 16:06:44 | <lambdabot> | <hint>:1:1: error: parse error on input ‘%’ |
| 16:06:50 | <danse-nr3> | % :t min |
| 16:06:50 | <yahb2> | min :: Ord a => a -> a -> a |
| 16:06:54 | <danse-nr3> | % :t minimum |
| 16:06:55 | <yahb2> | minimum :: (Foldable t, Ord a) => t a -> a |
| 16:07:00 | → | zetef joins (~quassel@95.77.17.251) |
| 16:07:01 | × | thegeekinside quits (~thegeekin@189.217.90.224) (Read error: Connection reset by peer) |
| 16:07:26 | <danse-nr3> | you can just use min if you want |
| 16:07:32 | <Joao003> | no |
| 16:07:37 | <Joao003> | min is for 2 arguments |
| 16:07:43 | <Joao003> | while minimum is for foldables |
| 16:07:58 | <Joao003> | % min [1,2,3] |
| 16:07:59 | <yahb2> | <interactive>:87:1: error: ; • No instance for (Show ([Integer] -> [Integer])) ; arising from a use of ‘Yahb2Defs.limitedPrint’ ; (maybe you haven't applied a function to enough... |
| 16:08:04 | <Joao003> | % minimum [1,2,3] |
| 16:08:04 | <yahb2> | 1 |
| 16:08:09 | × | trev quits (~trev@user/trev) (Quit: trev) |
| 16:08:58 | → | trev joins (~trev@user/trev) |
| 16:09:52 | <danse-nr3> | @hoogle (Foldable t, Ord a) => (a -> a -> a) -> t a -> a |
| 16:09:53 | <lambdabot> | Prelude foldr1 :: Foldable t => (a -> a -> a) -> t a -> a |
| 16:09:53 | <lambdabot> | Prelude foldl1 :: Foldable t => (a -> a -> a) -> t a -> a |
| 16:09:53 | <lambdabot> | Data.List foldl1 :: Foldable t => (a -> a -> a) -> t a -> a |
| 16:10:15 | <Joao003> | @src Foldable |
| 16:10:15 | <lambdabot> | Source not found. :( |
| 16:10:17 | <Joao003> | ... |
| 16:10:23 | <Joao003> | @t Foldable |
| 16:10:23 | <lambdabot> | Maybe you meant: tell thank you thanks thesaurus thx tic-tac-toe ticker time todo todo-add todo-delete type v @ ? . |
| 16:12:42 | × | Joao003 quits (~Joao003@190.108.99.207) (Quit: Bye!) |
| 16:12:53 | <danse-nr3> | @hoogle (Foldable t, Ord a, Monoid a) => (a -> a -> a) -> t a -> a |
| 16:12:53 | <lambdabot> | Safe.Foldable foldl1Safe :: (Monoid m, Foldable t) => (m -> m -> m) -> t m -> m |
| 16:12:53 | <lambdabot> | Safe.Foldable foldr1Safe :: (Monoid m, Foldable t) => (m -> m -> m) -> t m -> m |
| 16:12:53 | <lambdabot> | Prelude foldr1 :: Foldable t => (a -> a -> a) -> t a -> a |
| 16:15:25 | × | mechap quits (~mechap@user/mechap) (Quit: WeeChat 4.1.2) |
| 16:19:49 | <glguy> | I boiled down last night's problem into basically two left folds (per part) https://github.com/glguy/advent/blob/main/solutions/src/2023/11.hs |
| 16:26:04 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 16:28:24 | → | tri joins (~tri@ool-18bc2e74.dyn.optonline.net) |
| 16:36:05 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 16:36:46 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:d128:ce35:54e1:65e2) (Remote host closed the connection) |
| 16:37:01 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:444f:4a45:c596:a200) |
| 16:37:47 | → | hasevil joins (~hasevil@host-138-37-254-167.qmul.ac.uk) |
| 16:38:39 | <hasevil> | Hi guys, it showing parse error on data. I don't understand what I'm dooing wrong here https://paste.tomsmeding.com/uutJGKZP |
| 16:39:13 | <geekosaur> | on line 13 you're using `data` as a variable, but it's a keyword |
| 16:39:19 | × | azimut quits (~azimut@gateway/tor-sasl/azimut) (Ping timeout: 240 seconds) |
| 16:44:00 | <hasevil> | oh, dumb me |
| 16:44:01 | × | califax quits (~califax@user/califx) (Remote host closed the connection) |
| 16:44:25 | → | califax joins (~califax@user/califx) |
| 16:46:40 | × | hasevil quits (~hasevil@host-138-37-254-167.qmul.ac.uk) (Quit: nyaa~) |
| 16:49:56 | → | finn_elija joins (~finn_elij@user/finn-elija/x-0085643) |
| 16:49:56 | × | FinnElija quits (~finn_elij@user/finn-elija/x-0085643) (Killed (NickServ (Forcing logout FinnElija -> finn_elija))) |
| 16:49:56 | finn_elija | is now known as FinnElija |
| 16:50:40 | × | zetef quits (~quassel@95.77.17.251) (Ping timeout: 246 seconds) |
| 16:57:46 | <iqubic> | glguy: How are you computing where the blank lines are? |
| 17:01:57 | <glguy> | The blank lines are the space between locations where galaxies are |
| 17:03:01 | <glguy> | So there - here - 1 counts the blank lines |
| 17:05:07 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 17:05:58 | → | thegeekinside joins (~thegeekin@189.217.90.224) |
| 17:05:59 | × | danse-nr3 quits (~danse@151.35.255.237) (Ping timeout: 264 seconds) |
| 17:06:56 | → | Joao003 joins (~Joao003@190.108.99.207) |
| 17:07:25 | × | rosco quits (~rosco@175.136.152.56) (Quit: Lost terminal) |
| 17:07:28 | <Joao003> | is `(==) :: Char -> Char -> Bool' case sensitive? |
| 17:07:51 | <c_wraith> | yes |
| 17:09:06 | <c_wraith> | I'm curious, though.. WHat made you decide to ask us instead of ghci? We might lie! |
| 17:09:42 | <glguy> | Maybe ghci would lie the first time and then change? |
| 17:10:30 | × | tri quits (~tri@ool-18bc2e74.dyn.optonline.net) (Ping timeout: 256 seconds) |
| 17:11:14 | <exarkun> | To ask ghc you'd have to find all Char in the alphabetic category with uppercase and lowercase variations and test each of them, or you wouldn't know if it was _consistently_ case sensitive or insensitive |
| 17:11:49 | <Joao003> | thx, it's because i didn't read the description of a kata |
| 17:11:59 | <Joao003> | on codewars |
| 17:11:59 | → | peterbecich joins (~Thunderbi@047-229-123-186.res.spectrum.com) |
| 17:12:00 | <Joao003> | srry |
| 17:13:08 | <exarkun> | but you could also think about some laws, which would probably be a more Haskelly solution than asking irc or ghci |
| 17:13:41 | × | Feuermagier quits (~Feuermagi@user/feuermagier) (Remote host closed the connection) |
| 17:14:29 | → | econo_ joins (uid147250@id-147250.tinside.irccloud.com) |
| 17:14:31 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:444f:4a45:c596:a200) (Remote host closed the connection) |
| 17:15:44 | <iqubic> | glguy: It looks like l is the count of all galaxies that are in the current column or left of it? Is that correct? |
| 17:15:57 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:444f:4a45:c596:a200) |
| 17:19:00 | × | blastoise quits (~blastoise@205.185.193.149) (Quit: Leaving) |
| 17:20:08 | → | Unicorn_Princess joins (~Unicorn_P@user/Unicorn-Princess/x-3540542) |
| 17:22:45 | → | tri joins (~tri@ool-18bc2e74.dyn.optonline.net) |
| 17:24:17 | <glguy> | yeah |
| 17:24:48 | → | danza joins (~danza@151.35.255.237) |
| 17:26:37 | <int-e> | Space stretches a million times as I walk from here to there. I watch the galaxies as I walk, l behind, and r ahead. |
| 17:26:51 | <Joao003> | what are you talking about |
| 17:27:07 | <int-e> | glguy's code |
| 17:27:09 | <glguy> | https://adventofcode.com/2023/day/11 |
| 17:27:36 | <iqubic> | It's much better than what I did. |
| 17:28:23 | <glguy> | space travel would be just the worst if we had to take manhattan routes to get everywhere. Imagine satellite orbits :-o |
| 17:28:40 | <glguy> | and this 2D situation? We'd have so many collisions |
| 17:28:44 | <int-e> | I missed the big shortcut today, which was to use <rot13>yvarne rkgencbyngvb</rot13> |
| 17:28:45 | <iqubic> | My algorithm is an O(N^2) thing where I compute the distance between each pair of points. |
| 17:29:22 | <int-e> | oh I wrote totally naive code at first too |
| 17:29:40 | <glguy> | yeah, being not clever got me 15th on the first star |
| 17:29:40 | <iqubic> | How does your shortcut help you? |
| 17:29:44 | × | DerDummNemetzkii quits (~John_Ivan@user/john-ivan/x-1515935) (Ping timeout: 256 seconds) |
| 17:29:57 | <int-e> | It explains how people did part 2 in 1-2 minutes. |
| 17:30:08 | <int-e> | (some people) |
| 17:30:46 | → | darchitect joins (~darchitec@2a00:23c6:3584:df01:4cbc:8ff2:73ae:d845) |
| 17:31:24 | <int-e> | Even if they start out with a naive full grid based solution. Which is a good fit for Haskell's lists. |
| 17:32:42 | <iqubic> | My initial code had "expand xss = concatMap (\xs -> if '#' `elem` xs then [xs] else [xs, xs]" and "expanded = expand . transposs . expand . lines" |
| 17:33:02 | <int-e> | Yeah I had something like that too. |
| 17:33:54 | <iqubic> | The formatting is a bit off there. I should I have closed the lambda on the concatMap. But you get the idea. |
| 17:34:08 | <int-e> | You also typo-d "transpose". |
| 17:35:00 | <Joao003> | yo you just got me into advent of code (i'm coding in python though) |
| 17:35:15 | <iqubic> | So I did. I usually have LSP tell me about those issues. |
| 17:36:17 | <darchitect> | hey guys - do you think a sufficiently expressive type system can be a replacement to unit tests? |
| 17:36:27 | <glguy> | nope |
| 17:36:33 | <darchitect> | P.S. I'm a newb in functinal progrmming |
| 17:36:49 | <darchitect> | glguy: I guess I was going after a more explanatory answer :( |
| 17:36:55 | <iqubic> | Yeah. Unit tests are always gonna be needed. |
| 17:36:57 | <monochrom> | Yes, but so expressive, you will give up type inference. |
| 17:37:02 | <probie> | A sufficiently expressive type system _can_ be a replacement to unit tests |
| 17:37:10 | <probie> | You just put the fact that the unit test passes in the type |
| 17:37:23 | → | aruns joins (~aruns@user/aruns) |
| 17:37:38 | <int-e> | Even if your type system is so needy, I mean dependent, that it entails proofs of correctness, you'll still want to check that the properties that the types encode do what you want. |
| 17:37:42 | <monochrom> | In fact, you will give up proof inference. That's right, you go all out write correctness proofs in the type system, that's how you replace tests. |
| 17:38:13 | <glguy> | proofs don't even really replace unit tests |
| 17:38:20 | <glguy> | YOu still need to check what it is you actually proved |
| 17:38:37 | <glguy> | properties can be wrong, too |
| 17:39:07 | <ski> | darchitect : property-based testing can be quite nice |
| 17:39:14 | <int-e> | . o O ( In another universe it's proofs all the way down. ) |
| 17:39:17 | <darchitect> | no I guess I meant that - in light of current LLM developments you can easily have LLMs write tests based on your type and then implement the function that passes the tests with some guidance on whether you want your program to be readable/fast/memory-efficient etc.. and then they would just do it |
| 17:39:44 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 17:39:44 | <glguy> | You generally can't generate unit tests from types |
| 17:39:56 | <glguy> | (at least not in a useful way) |
| 17:39:58 | <int-e> | And also... so you'll still have tests? |
| 17:40:12 | <darchitect> | yeah but you won't have to write them |
| 17:40:31 | <int-e> | I wouldn't get my hopes up. |
| 17:40:32 | <probie> | but that's not replacing them, that's just outsourcing them |
| 17:40:39 | <darchitect> | yeah to a machine |
| 17:40:41 | <monochrom> | That's interesting. Now we have to prove that the generated tests are correct! |
| 17:41:02 | <int-e> | And interesting! |
| 17:41:29 | <glguy> | unit tests generally test things that the types don't check or even indicate |
| 17:41:31 | <int-e> | (We can already automate throwing a million random tests at code. But we have a harder time automating covering all corner cases.) |
| 17:42:06 | <int-e> | (Kerword fuzzing... I think I've read about people coupling that with SMT solvers to get more coverage.) |
| 17:42:18 | <int-e> | Ker -> Key |
| 17:42:51 | <darchitect> | I mainly started teh conversation because I work in ML and I feel like that LLMs will never replace the necessity to express your thoughts with mathematical precision not just using natural language. So I am wondering what would the role be for LLMs in cases where you do need to express precisely what you need to happen and for now I think using the type system as spec and letting the model |
| 17:42:53 | <darchitect> | implement the code, then write tests based off of the function and our job would be to decide whether the tests are all covered... |
| 17:43:27 | × | peterbecich quits (~Thunderbi@047-229-123-186.res.spectrum.com) (Ping timeout: 256 seconds) |
| 17:43:27 | <darchitect> | I don't know if I am making too much sense here just thinking out loud |
| 17:44:00 | <int-e> | The role of LLMs will be to fool people into thinking that they've understood a specification... until the bug reports come pouring in. |
| 17:44:08 | <monochrom> | It is an open question because there is no data on training LLMs on formulas instead of prose. |
| 17:44:24 | <iqubic> | Let's say you wrote a function "rev :: [a] -> [a]" to reverse lists. How would you verify that your code is actually doing the right thing? |
| 17:44:37 | <darchitect> | if you were able to encode the ordering in the type you could |
| 17:44:47 | <dminuoso_> | int-e │ The role of LLMs will be to fool people into thinking that they've understood a specification... until the bug reports come pouring in. |
| 17:44:47 | <int-e> | I believe that LLMs (in their current state) do not have a sufficiently deep feedback loop for formal reasoning. |
| 17:44:58 | <dminuoso_> | And this is different from actual math publications exactly.. how? |
| 17:45:05 | <monochrom> | OK I guess Microsoft Copilot is data on training an LLM on code. That's something. |
| 17:45:08 | <int-e> | But they make excellent electric monks. |
| 17:45:17 | <ski> | darchitect : Ocaml or SML ? |
| 17:45:34 | <monochrom> | (The result is not great.) |
| 17:45:34 | <darchitect> | ski: just any functional language relaly |
| 17:45:44 | <ski> | yes, but you said ML |
| 17:46:05 | <int-e> | monochrom: I imagine it tends to work for boilerplate, which is like 99% of all code these days. :P |
| 17:46:07 | <darchitect> | ski: no no Machine Learning, sorry forgot I'm not in an AI chat :D |
| 17:46:22 | <ski> | oh .. not Machine Language, either, then .. :/ |
| 17:46:30 | <monochrom> | My LLM says that if both "ML" and "LLM" appear in the same sentence then "ML" means machine learning. :D |
| 17:46:35 | <ski> | (or Mailing Lists .. guess there's a bunch) |
| 17:46:42 | <int-e> | monochrom: And because we have LLMs now we can afford writing even more boilerplate code! |
| 17:46:47 | × | TheCoffeMaker quits (~TheCoffeM@user/thecoffemaker) (Ping timeout: 264 seconds) |
| 17:46:55 | <int-e> | Productivity is going to go through the roof. |
| 17:47:03 | <dminuoso_> | I mean when I make a merge request to some github repo, my role too is to fool people into thinking Ive understood their code and that my code adds some value. |
| 17:47:07 | ski | . o O ( more places for bugs to hide in. luvly jubly ! ) |
| 17:47:10 | <monochrom> | This is one more reason why programming is a scam. |
| 17:47:17 | <dminuoso_> | With something like GHC there's a lot of "fooling" in the way you phrase and present your changes. |
| 17:47:28 | <int-e> | (productivity is, of course, measured in lines of code per day) |
| 17:47:32 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:444f:4a45:c596:a200) (Remote host closed the connection) |
| 17:47:58 | <monochrom> | Previously, I already said that lack of static type checking is already a scam because you are hiding bugs from the user at pay time. |
| 17:48:07 | <darchitect> | I still don't see how a probabilistic model can replace programmers |
| 17:48:20 | <monochrom> | Now it is a scam the second time because you get paid to write boilerplate code. |
| 17:48:20 | → | TheCoffeMaker joins (~TheCoffeM@user/thecoffemaker) |
| 17:48:21 | <dminuoso_> | darchitect: Programers themselves prove to be probabilitistic models too. |
| 17:48:21 | <darchitect> | at some point you just need to be specific on what you want to do to the last detail |
| 17:48:39 | <dminuoso_> | Its just that currently some individuals tend to have better training. |
| 17:49:09 | <ski> | and perhaps somewhat better judgement |
| 17:49:21 | <EvanR> | average number of "wtfs" per minute in code review |
| 17:49:33 | <darchitect> | I would find it weird to have an AI model write the spec for an airplane based off of text from the internet :D |
| 17:49:35 | <int-e> | dminuoso_: The proper way to read a math publication is to take the guidance of the text and follow the formal reasoning steps yourself with a critical eye. I guess that's similar to how you interact with an LLM, but with a math paper there's a chance that the author actually reasoned through the things they wrote about. |
| 17:49:43 | → | John_Ivan joins (~John_Ivan@user/john-ivan/x-1515935) |
| 17:50:45 | <tromp> | has any LLM been tried on solving AoC puzzles? |
| 17:51:54 | <geekosaur> | no doubt ssomeone's using it now |
| 17:51:55 | <EvanR> | probably, though it's against the rules this year |
| 17:52:01 | <int-e> | Specifically? Hmm. There's all this fine tuning of LLMs going on which is relatively cheap... somebody must have tried that with AoC. |
| 17:52:52 | <tromp> | Oh, I see it now in the About section: Can I use AI to get on the global leaderboard? |
| 17:53:16 | <int-e> | Yeah, direct link: https://adventofcode.com/about#faq_ai_leaderboard |
| 17:53:36 | <int-e> | Note that they don't care once the top 100 is filled up. |
| 17:54:01 | <int-e> | (Well, I guess they care, but who would want to police that...) |
| 17:54:27 | <tromp> | it would be nice if they simply allowed ppl to sign up an AI, which would keep them out of the human leaderboard |
| 17:54:36 | <darchitect> | will type theory still be a thing of the future ? As in what would it's main use be in programming if we're all writing "good-enough" programs with lots of empirical tests and no proofs |
| 17:54:45 | <darchitect> | in the future * |
| 17:54:48 | <tromp> | and show them on an exclusive and separate AI leaderboard |
| 17:55:05 | <EvanR> | it makes sense to say "if you want an AI contest try another contest" |
| 17:55:29 | <EvanR> | since it takes a lot of human work to put this one together |
| 17:55:33 | <Joao003> | i installed deskpins just to pin my irc client |
| 17:55:48 | <monochrom> | We don't all write good-enough programs. |
| 17:56:06 | <tromp> | doesn't a separate AI leaderboard make more sense? More data from same design effort |
| 17:56:06 | <dminuoso_> | int-e: This is no different from say a program. Unless this went through a automated theorem prover (whose correctness Ill just assume axiomatically for the sake of discussion), the mere fact that you cannot trust the author himself is why you cant necessarily trust your personal judgement. Its how various Jacobian Conjecture were accepted for a while, despite ultimately being proven wrong. |
| 17:56:12 | <int-e> | monochrom: not-to-bad is where the money's at ;) |
| 17:56:20 | <monochrom> | heehee |
| 17:56:23 | <int-e> | *too |
| 17:56:25 | <dminuoso_> | We're just deeply flawed - its just that especially mathematicians strike to reduce the errors. |
| 17:56:26 | <EvanR> | well some of the questions don't have randomly generated input data |
| 17:56:36 | <dminuoso_> | No different from LLM engineers trying to reduce their models errors. |
| 17:56:39 | <monochrom> | But there are niches that insist on proofs. |
| 17:56:42 | <int-e> | (but that was a good place for inserting a typo) |
| 17:56:43 | <EvanR> | AI on those would disrupt the humans |
| 17:56:52 | → | Square joins (~Square@user/square) |
| 17:56:58 | × | Square2 quits (~Square4@user/square) (Ping timeout: 256 seconds) |
| 17:57:00 | <dminuoso_> | monochrom: But how do you know correctness of a proof! |
| 17:57:03 | <EvanR> | the first AI to reach the goal solves it for everyone |
| 17:57:23 | <int-e> | dminuoso_: Yes, math is an empirical science where the experiment is taking a paper and letting an expert in its respective field read it. |
| 17:57:38 | × | ChaiTRex quits (~ChaiTRex@user/chaitrex) (Remote host closed the connection) |
| 17:57:53 | <monochrom> | Well yeah their real goal is extremely high confidence, and they have chosen proofs as the means. |
| 17:57:53 | <ski> | math is also an aesthetic endeavor |
| 17:58:02 | → | ChaiTRex joins (~ChaiTRex@user/chaitrex) |
| 17:58:09 | <int-e> | But no, LLMs at this point cannot sufficiently imitate a mathematician to produce papers that are worth subjecting to that experiment. |
| 17:58:47 | <dminuoso_> | Not yet, anyhow. |
| 17:58:47 | <Franciman> | int-e: i think they can do fine enough in the history of mathematics |
| 17:58:51 | <int-e> | Will future LLMs be different? Maybe. They'll need a different architecture. |
| 17:59:40 | <monochrom> | You know, I'm very cynical about human abilities too. |
| 17:59:52 | <dminuoso_> | In fact Im going to argue that in general scientific publications there is a feedback loop that trains scientists to act precisely like LLM: Try and convince people about your idea being right. Whether it is right is often irrelevant: |
| 17:59:58 | <int-e> | ("large language model" is a stupidly generic term. And stupid in that it sounds as if it's just about size.) |
| 18:00:02 | <dminuoso_> | Impact factor of a Nature or Science publication: Thats what counts. |
| 18:00:14 | <dminuoso_> | Not correctness of science. |
| 18:00:17 | <monochrom> | My model of human thought: A backend that's correct >70% of the time, and a not-gate for the front end. |
| 18:00:41 | <monochrom> | So yes I agree that LLMs are stupid but humans are beyond stupid. |
| 18:01:26 | <monochrom> | At present, LLMs already make better politicians than human politicians. |
| 18:02:07 | <EvanR> | on a practical matter they make better sports writers |
| 18:02:14 | <trev> | monochrom: careful...that means they can lie and steal better too |
| 18:02:17 | <monochrom> | (Well, at least until some robot overlord changes politics from "verbally convincing" to "actual proofs".) |
| 18:02:28 | <dminuoso_> | trev: Oh ChatGPT has no problem with confabulating the world. |
| 18:02:32 | <trev> | lolz |
| 18:02:35 | × | araujo quits (~araujo@216.73.163.11) (Ping timeout: 260 seconds) |
| 18:02:58 | <trev> | it's so confident |
| 18:03:10 | <dminuoso_> | The kind of stories you see, where it confabulates imaginary papers, quoting them and describing them in great detail... |
| 18:03:25 | <dminuoso_> | Describing history events that never occured.. |
| 18:03:43 | <dminuoso_> | Id say ChatGPT is ripe to evolve into politics. |
| 18:03:57 | <ski> | or to get into textbook writing |
| 18:04:11 | <EvanR> | there was an AI generated political ad a few months back, kind of disturbing |
| 18:04:14 | <darchitect> | do you reckon if we had all math encapsulated in a proof assistant and then the ai explored possible reasoing paths to come to a proof, then I guess we can the proof for truth |
| 18:04:28 | <dminuoso_> | darchitect: This is already being explored by Google at least. |
| 18:04:46 | <darchitect> | are you getting this from the latest reasoning example for Gemini ? |
| 18:06:35 | <monochrom> | Yeah a proof assistant is great at checking an alleged proof, an LLM is great at creating an alleged proof, the two of them yelling at each other can get things done right, afterall that's how I work too. |
| 18:06:56 | <monochrom> | "I argue with myself all the time. It adds sparks to my arguments." |
| 18:06:58 | <dminuoso_> | darchitect: As just a single small excerpt: https://www.nature.com/articles/s41586-022-05172-4 |
| 18:07:49 | <monochrom> | There are also people hooking up ChatGPT with Mathematica or Wolfram Alpha. |
| 18:08:16 | <dminuoso_> | Glue code written by ChatGPT? |
| 18:09:06 | <darchitect> | yeah I mean everything we do in our heads is ultimately search, question is whether reinforcement learning + LLM is what we really do in our heads |
| 18:09:40 | <darchitect> | or actually the question is - is it better to do RL + LLM or is our mind better |
| 18:09:55 | <dminuoso_> | Id start by asking the question: How do you even measure "better"? |
| 18:10:32 | × | gmg quits (~user@user/gehmehgeh) (Remote host closed the connection) |
| 18:11:07 | <duncan> | A backend that's correct 70% of the time is.. hideously bad |
| 18:11:09 | <darchitect> | well in terms of producing faster code for example, or shorter and faster code |
| 18:11:18 | <dminuoso_> | Take Copilot and the latest 10,000 internal junior developer issues at Microsoft. If Copilot can fix those bugs while costing less on average (in terms of service outages, or human costs involved in fixing broken systems) - is it better than a junior developer? |
| 18:11:22 | → | gmg joins (~user@user/gehmehgeh) |
| 18:11:27 | <dminuoso_> | From a business perspective: it probably is. |
| 18:11:39 | <darchitect> | dminuoso_: yeah deffinitely |
| 18:11:41 | <Rembane> | I wonder how much it will slow down development on those code bases. |
| 18:11:58 | <darchitect> | dminuoso_: I was talking more about new math or for mission-critical systems programming |
| 18:12:23 | <darchitect> | is there a way to get the LLMs to be better than humans or is it a fundamental barier to AI |
| 18:12:43 | <dminuoso_> | Look at SpaceX, they use an awful lot of C++ in their systems - not the primary candidate for proven and reliable hard real time systems if you asked anyone from 20 years ago. |
| 18:13:00 | × | alexherbo2 quits (~alexherbo@2a02-8440-3341-aec3-516d-6fbd-7275-d6e8.rev.sfr.net) (Remote host closed the connection) |
| 18:13:04 | <dminuoso_> | But it seems to work? |
| 18:13:17 | <duncan> | darchitect: if you are asking "is there a way to get the LLMs to be better than humans", you have a fatal issue of problem specification |
| 18:14:07 | <duncan> | It's the equivalent of consultants criticising the technical people for focusing on data management instead of getting on and doing the real work of modelling |
| 18:14:46 | <dminuoso_> | We already live in a world where domain specific machines are better than humans. Robot arms are faster and more precise than human arms. Pumps have higher throughput than a person with a bucket. Neural networks can recognize writing with a much higher speed and precision than average humans. |
| 18:15:35 | <duncan> | sure, and the neural networks not infrequently don't perform better than linear regression. touché? |
| 18:16:11 | <dminuoso_> | Sorry, too many negatives in there. |
| 18:16:24 | <dminuoso_> | My neural net cannot process this. >:) |
| 18:16:33 | <darchitect> | yeah true, I guess what I'm really getting at is this - For some programs, expressing your throughts precisely will still be necessary, because we are the agents that "will things" and models are things that bring them "into being", what is the future of programming? Will there be programs that NEED to be written in code as opposed to explained in a natural language ? If not, then the robots can |
| 18:16:34 | <darchitect> | just write assembly because nobody needs to read their code if we know it's correct and it's going to run with "sufficient reliability" |
| 18:16:40 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:444f:4a45:c596:a200) |
| 18:17:14 | <int-e> | what |
| 18:17:30 | <duncan> | darchitect: ask yourself, does this pass the "so what" test |
| 18:17:31 | <dminuoso_> | My biggest issue is having no answers when my girlfriend asks me how to deal with students submitting homework solutions that were seemingly produced by ChatGPT. |
| 18:17:33 | <int-e> | higher level languages *structure* programs |
| 18:17:36 | <darchitect> | sorry not great enlgish here |
| 18:18:20 | <darchitect> | int-e: simplified - does PL research have any value if we go in the direction of full on AI ? |
| 18:18:25 | <int-e> | It's not just about readability, it's about hiding complexity and providing layers of abstraction. |
| 18:18:32 | <int-e> | Yes, it does. |
| 18:20:29 | <darchitect> | int-e: Right, but in this case - don't we all just need to build 1 good language the machines speak and that's it. They can just forever optimize on it because the data will grow and grow. |
| 18:20:51 | → | Tuplanolla joins (~Tuplanoll@91-159-68-236.elisa-laajakaista.fi) |
| 18:21:12 | <ski> | dminuoso_ : tell her to ask them to explain it, in person ? |
| 18:21:19 | <int-e> | /If/ that ever happens, that would just mean they'd do their own PL research, at least when translated to human terms. |
| 18:21:29 | → | tzh joins (~tzh@c-71-193-181-0.hsd1.or.comcast.net) |
| 18:21:29 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 18:22:48 | <dminuoso_> | ski: The student denies, improves their ChatGPT prompt the next time. The real issue isnt necessarily the single incident, but rather the impact on learning. |
| 18:22:55 | <ski> | dminuoso_ : what if there won't be as many junior developers who get enough experience to develop past that ? |
| 18:23:20 | <darchitect> | int-e: well why would we need to hide complexity in this case, if they will do PL research as an emergent feature of having trillions of neurons |
| 18:23:48 | <ski> | dminuoso_ : yea, ignore whether they actually used ChatGPT to produce it. ask them to explain how it works |
| 18:23:56 | <ski> | in person |
| 18:24:10 | <dminuoso_> | ski: Like I said, the deeper problem isnt how to reveal someone who used it. |
| 18:24:29 | × | pavonia quits (~user@user/siracusa) (Quit: Bye!) |
| 18:24:34 | <dminuoso_> | Its just that the tool has become to easily accessible, that this is slowly having an impact on student learning. |
| 18:24:39 | <dminuoso_> | Not in a good way. |
| 18:24:42 | <ski> | well, if ChatGPT wrote the code, then ChatGPT should earn the grade, no ? |
| 18:24:44 | <dminuoso_> | At least in heir classes. |
| 18:24:52 | <dminuoso_> | ski: This is Biology, mind you. |
| 18:25:02 | <ski> | mhm |
| 18:25:41 | ski | . o O ( "To Heir or not to Heir" -- some King's Quest game (IV ?) ) |
| 18:26:01 | <int-e> | darchitect: You have way more faith in the power of big numbers than I do. |
| 18:26:08 | → | mrmr15533 joins (~mrmr@user/mrmr) |
| 18:26:21 | <dminuoso_> | Prague University has stopped requiring written Bachelor thesis - though there's more facettes to this. However, the advance of language models tipped the scale. |
| 18:26:58 | <dminuoso_> | Perhaps in 20 years from now, we will have changed education systems to cope with such tools. |
| 18:27:06 | <dminuoso_> | But education changes rather slowly. |
| 18:27:32 | <darchitect> | int-e: no, no I don't I think these are just probabilistic machines after all and I don't think they are doing anything we're doing in our heads, but I just want to have a more precise confirmation (or refutal) to my own thinking. |
| 18:27:35 | <ski> | well .. i do guess, with podcasts and the like, more people have started to focus more again on auditory learning, over visual learning |
| 18:27:39 | → | ft joins (~ft@p3e9bc784.dip0.t-ipconnect.de) |
| 18:27:46 | <ski> | (which was more the case, before the printing press) |
| 18:28:30 | <EvanR> | makes sense, the percent of human population stuck in traffic increases |
| 18:29:15 | <darchitect> | int-e: I really want to continue studying PL design, but in my mind I am always thinking whether I should study the classic PL design or I should study PL design the machines will find useful one day... or I've probably had too much tea today |
| 18:29:18 | <darchitect> | :d |
| 18:30:04 | × | alp_ quits (~alp@2001:861:e3d6:8f80:66b0:842b:748c:f4e2) (Ping timeout: 246 seconds) |
| 18:30:05 | <ski> | (e.g. with "mind/memory castle/palace/journey/space"/"method of loci". <https://en.wikipedia.org/wiki/Mind_palace> being used since ancient times) |
| 18:30:12 | <int-e> | darchitect: If these things reason in any way like humans do, they will need layers of abstraction to have a fighting chance against bugs. If they don't then any speculation that I can hope to offer is completely meaningless. This isn't even philosophical anymore, it's becoming a matter of beliefs, so it's bascially religious. |
| 18:30:32 | <ephemient> | https://youtu.be/rhgwIhB58PA "The Biggest Myth In Education. You are not a visual learner — learning styles are a stubborn myth." |
| 18:32:01 | <darchitect> | int-e: yeah I agree.. |
| 18:32:49 | → | alexherbo2 joins (~alexherbo@2a02-8440-3341-aec3-516d-6fbd-7275-d6e8.rev.sfr.net) |
| 18:33:54 | <darchitect> | int-e: I wonder if there is any research of using LLMs on doing just that -> getting a program in a typed lambda calculus and asking it to generate the abstractions it thinks are most useful, but then I presume it would just regurgitate something it read on reddit or github :( |
| 18:36:28 | ski | . o O ( "Autism, Academics, and Animals | Dr. Temple Grandin" <https://www.youtube.com/watch?v=XYZP1wuGBD8#t=3m8s> (re different kinds of thinkers, verbal, object-visual, visual-spatial .. and other things, like lack of hands-on shops leading to wear and tear of machinery, and about improvement of animal handling in meat processing) ) |
| 18:37:05 | → | qqq joins (~qqq@92.43.167.61) |
| 18:38:17 | × | wagle quits (~wagle@quassel.wagle.io) (Quit: http://quassel-irc.org - Chat comfortably. Anywhere.) |
| 18:38:35 | → | wagle joins (~wagle@quassel.wagle.io) |
| 18:38:40 | × | alexherbo2 quits (~alexherbo@2a02-8440-3341-aec3-516d-6fbd-7275-d6e8.rev.sfr.net) (Remote host closed the connection) |
| 18:39:00 | × | wagle quits (~wagle@quassel.wagle.io) (Client Quit) |
| 18:39:52 | → | alexherbo2 joins (~alexherbo@60.37.22.93.rev.sfr.net) |
| 18:39:52 | → | wagle joins (~wagle@quassel.wagle.io) |
| 18:43:22 | × | tri quits (~tri@ool-18bc2e74.dyn.optonline.net) (Ping timeout: 246 seconds) |
| 18:44:36 | → | danik292 joins (~danik292@109-81-93-115.rct.o2.cz) |
| 18:48:00 | → | mechap joins (~mechap@user/mechap) |
| 18:48:00 | × | danik292 quits (~danik292@109-81-93-115.rct.o2.cz) (Client Quit) |
| 18:49:56 | → | nate4 joins (~nate@c-98-45-158-125.hsd1.ca.comcast.net) |
| 18:52:32 | → | danik292 joins (~danik292@109-81-93-115.rct.o2.cz) |
| 18:54:51 | × | nate4 quits (~nate@c-98-45-158-125.hsd1.ca.comcast.net) (Ping timeout: 256 seconds) |
| 18:57:50 | → | tri joins (~tri@ool-18bc2e74.dyn.optonline.net) |
| 18:59:06 | → | bratwurst joins (~blaadsfa@2604:3d09:2083:a200:216:3eff:fe5a:a1f8) |
| 19:00:32 | × | bratwurst quits (~blaadsfa@2604:3d09:2083:a200:216:3eff:fe5a:a1f8) (Client Quit) |
| 19:03:41 | × | tri quits (~tri@ool-18bc2e74.dyn.optonline.net) (Ping timeout: 252 seconds) |
| 19:04:57 | × | danik292 quits (~danik292@109-81-93-115.rct.o2.cz) (Quit: Client closed) |
| 19:06:13 | × | danza quits (~danza@151.35.255.237) (Read error: Connection reset by peer) |
| 19:07:22 | → | danik292 joins (~danik292@109-81-93-115.rct.o2.cz) |
| 19:15:16 | × | danik292 quits (~danik292@109-81-93-115.rct.o2.cz) (Quit: Client closed) |
| 19:16:27 | → | tri joins (~tri@ool-18bc2e74.dyn.optonline.net) |
| 19:18:01 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 19:19:16 | × | sord937 quits (~sord937@gateway/tor-sasl/sord937) (Quit: sord937) |
| 19:19:45 | × | John_Ivan quits (~John_Ivan@user/john-ivan/x-1515935) (Quit: Disrupting the dragon's slumber one time too often shall eventually bestow upon all an empirical and indiscriminate conflagration that will last for all goddamn eternity.) |
| 19:20:46 | × | tri quits (~tri@ool-18bc2e74.dyn.optonline.net) (Ping timeout: 245 seconds) |
| 19:20:58 | → | danza joins (~danza@151.37.252.39) |
| 19:26:49 | → | danik292 joins (~danik292@109-81-93-115.rct.o2.cz) |
| 19:27:01 | × | danik292 quits (~danik292@109-81-93-115.rct.o2.cz) (Client Quit) |
| 19:28:21 | → | bilegeek joins (~bilegeek@2600:1008:b08b:7355:7869:26c7:cf9e:bac4) |
| 19:31:18 | × | mikess quits (~sam@user/mikess) (Quit: leaving) |
| 19:33:19 | → | tri joins (~tri@ool-18bc2e74.dyn.optonline.net) |
| 19:39:11 | × | tri quits (~tri@ool-18bc2e74.dyn.optonline.net) (Ping timeout: 260 seconds) |
| 19:39:16 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:444f:4a45:c596:a200) (Remote host closed the connection) |
| 19:43:33 | → | johnw_ joins (~johnw@69.62.242.138) |
| 19:43:46 | → | Guest25 joins (~Guest25@46.39.53.144) |
| 19:45:51 | × | johnw quits (~johnw@69.62.242.138) (Ping timeout: 256 seconds) |
| 19:47:45 | → | alp_ joins (~alp@2001:861:e3d6:8f80:c150:fb83:d53f:eaf2) |
| 19:49:09 | × | Guest25 quits (~Guest25@46.39.53.144) (Quit: Client closed) |
| 19:51:29 | → | tri joins (~tri@ool-18bc2e74.dyn.optonline.net) |
| 19:53:17 | ← | Joao003 parts (~Joao003@190.108.99.207) (Bye!) |
| 19:53:27 | → | Joao003 joins (~Joao003@190.108.99.207) |
| 20:03:41 | × | aruns quits (~aruns@user/aruns) (Ping timeout: 240 seconds) |
| 20:05:23 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 20:10:28 | × | _ht quits (~Thunderbi@28-52-174-82.ftth.glasoperator.nl) (Quit: _ht) |
| 20:10:39 | → | [_] joins (~itchyjunk@user/itchyjunk/x-7353470) |
| 20:11:15 | × | fr33domlover quits (~fr33domlo@towards.vision) (Quit: The Lounge - https://thelounge.chat) |
| 20:14:44 | × | [itchyjunk] quits (~itchyjunk@user/itchyjunk/x-7353470) (Ping timeout: 268 seconds) |
| 20:14:47 | → | fr33domlover joins (~fr33domlo@towards.vision) |
| 20:16:36 | → | jargon joins (~jargon@32.sub-174-238-226.myvzw.com) |
| 20:19:08 | × | mjs2600 quits (~mjs2600@c-174-169-225-239.hsd1.vt.comcast.net) (Quit: ZNC 1.8.2 - https://znc.in) |
| 20:19:37 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:444f:4a45:c596:a200) |
| 20:19:52 | → | cwdar^ joins (~cd@c-98-242-74-66.hsd1.ga.comcast.net) |
| 20:21:15 | → | ec joins (~ec@gateway/tor-sasl/ec) |
| 20:22:07 | × | Maeda quits (~Maeda@91-161-10-149.subs.proxad.net) (Quit: stop) |
| 20:23:23 | → | mjs2600 joins (~mjs2600@c-174-169-225-239.hsd1.vt.comcast.net) |
| 20:24:10 | × | alexherbo2 quits (~alexherbo@60.37.22.93.rev.sfr.net) (Remote host closed the connection) |
| 20:24:26 | → | alexherbo2 joins (~alexherbo@2a02-8440-3341-aec3-39e5-e6a4-25fc-cb4b.rev.sfr.net) |
| 20:37:09 | → | mikess joins (~sam@user/mikess) |
| 20:38:48 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 20:58:12 | <haskellbridge> | 12<Celestial> I don't know what that video is about specifically, but I just can't listen to Jordan Peterson. He is a right-wing freak who time and time again targets trans-people and spews bigoted nonsense |
| 20:59:32 | → | Square2 joins (~Square4@user/square) |
| 21:01:12 | <ncf> | +1 |
| 21:01:41 | <Rembane> | +1 |
| 21:02:01 | × | Square quits (~Square@user/square) (Ping timeout: 245 seconds) |
| 21:05:40 | × | trev quits (~trev@user/trev) (Quit: trev) |
| 21:08:00 | × | thegeekinside quits (~thegeekin@189.217.90.224) (Read error: Connection reset by peer) |
| 21:13:50 | × | rvalue quits (~rvalue@user/rvalue) (Quit: ZNC - https://znc.in) |
| 21:14:04 | → | rvalue joins (~rvalue@user/rvalue) |
| 21:14:47 | → | thegeekinside joins (~thegeekin@189.217.90.224) |
| 21:14:47 | × | thegeekinside quits (~thegeekin@189.217.90.224) (Read error: Connection reset by peer) |
| 21:15:11 | <mauke> | yes (also why would you link to his youtube channel) |
| 21:19:47 | → | drdo9 joins (~drdo@bl14-14-49.dsl.telepac.pt) |
| 21:19:55 | × | mikess quits (~sam@user/mikess) (Quit: leaving) |
| 21:20:25 | × | drdo quits (~drdo@bl14-14-49.dsl.telepac.pt) (Killed (NickServ (GHOST command used by drdo9))) |
| 21:20:34 | drdo9 | is now known as drdo |
| 21:21:16 | → | thegeekinside joins (~thegeekin@189.217.90.224) |
| 21:21:19 | × | thegeekinside quits (~thegeekin@189.217.90.224) (Read error: Connection reset by peer) |
| 21:27:06 | × | danza quits (~danza@151.37.252.39) (Ping timeout: 260 seconds) |
| 21:27:07 | → | drdo8 joins (~drdo@bl14-14-49.dsl.telepac.pt) |
| 21:28:50 | × | fendor quits (~fendor@2a02:8388:1605:d100:267b:1353:13d7:4f0c) (Remote host closed the connection) |
| 21:29:13 | × | drdo quits (~drdo@bl14-14-49.dsl.telepac.pt) (Ping timeout: 276 seconds) |
| 21:29:44 | drdo8 | is now known as drdo |
| 21:30:57 | → | Guest70 joins (~Guest70@137.59.204.20) |
| 21:31:09 | × | mmhat quits (~mmh@p200300f1c702cdcaee086bfffe095315.dip0.t-ipconnect.de) (Quit: WeeChat 4.1.2) |
| 21:31:46 | × | Guest70 quits (~Guest70@137.59.204.20) (Client Quit) |
| 21:50:59 | → | azimut joins (~azimut@gateway/tor-sasl/azimut) |
| 21:51:05 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 21:52:54 | × | igemnace quits (~ian@user/igemnace) (Read error: Connection reset by peer) |
| 21:53:21 | → | igemnace joins (~ian@user/igemnace) |
| 21:59:49 | → | mikess joins (~sam@user/mikess) |
| 21:59:49 | → | thegeekinside joins (~thegeekin@189.217.90.224) |
| 22:00:11 | × | coot quits (~coot@89-69-206-216.dynamic.chello.pl) (Quit: coot) |
| 22:03:44 | → | pavonia joins (~user@user/siracusa) |
| 22:04:35 | × | takuan quits (~takuan@178-116-218-225.access.telenet.be) (Remote host closed the connection) |
| 22:13:11 | × | __monty__ quits (~toonn@user/toonn) (Quit: leaving) |
| 22:16:15 | <Joao003> | how do i extract `x' out of `Just x' without pattern-matching? |
| 22:16:36 | <monochrom> | Cannot. Use pattern matching. |
| 22:16:53 | <Joao003> | @hoogle Maybe a -> a |
| 22:16:54 | <lambdabot> | Data.Maybe fromJust :: HasCallStack => Maybe a -> a |
| 22:16:54 | <lambdabot> | Network.AWS.Prelude fromJust :: () => Maybe a -> a |
| 22:16:54 | <lambdabot> | Data.Maybe.Utils forceMaybe :: Maybe a -> a |
| 22:17:03 | <monochrom> | If you find yourself doing it a million times, then: |
| 22:17:10 | <monochrom> | 1. Write a helper function? |
| 22:17:18 | <Joao003> | 2: |
| 22:17:25 | <monochrom> | 2. Perhaps don't have Maybe in the first place? |
| 22:17:35 | <Joao003> | % Data.Maybe.fromJust (Just 8) |
| 22:17:35 | <yahb2> | 8 |
| 22:19:09 | <geekosaur> | note that it throws if it's Nothing |
| 22:19:55 | <Joao003> | but in my case it's guaranteed* to be just |
| 22:20:22 | <Joao003> | * guaranteed under the circumstances of the codewars kata that i'm doing |
| 22:21:50 | <monochrom> | In that kind of situations I usually use pattern matching and have "Nothing -> error "shouldn't happen because ..."" |
| 22:22:16 | <Joao003> | i'm pointless |
| 22:22:23 | <monochrom> | I am too lazy to import Data.Maybe so I would rather write that longer error message! |
| 22:22:31 | <Joao003> | lol |
| 22:22:34 | <glguy> | vscode will import it for me |
| 22:22:38 | <c_wraith> | :t fromMaybe (error "message") |
| 22:22:39 | <lambdabot> | Maybe a -> a |
| 22:22:42 | <glguy> | *full speed ahead* |
| 22:22:50 | → | machinedgod joins (~machinedg@93-136-135-211.adsl.net.t-com.hr) |
| 22:22:50 | <Joao003> | :t fromMaybe |
| 22:22:51 | <lambdabot> | a -> Maybe a -> a |
| 22:23:07 | <Joao003> | :t fromJust |
| 22:23:08 | <lambdabot> | Maybe a -> a |
| 22:23:15 | <monochrom> | Well yeah approximately the only IDE feature that I miss is auto imports. |
| 22:23:15 | <Joao003> | @src fromJust |
| 22:23:15 | <lambdabot> | fromJust Nothing = undefined |
| 22:23:15 | <lambdabot> | fromJust (Just x) = x |
| 22:23:25 | <Joao003> | IT USES PATTERN MATCHING NOOOOO |
| 22:23:29 | <monochrom> | (compared to emacs haskell-mode or dante) |
| 22:23:33 | <c_wraith> | everything uses pattern matching |
| 22:23:39 | <c_wraith> | pattern matching is the primitive operation |
| 22:23:41 | → | tv joins (~tv@user/tv) |
| 22:23:41 | <glguy> | Joao003: if you want to avoid pattern matching, use python |
| 22:23:44 | <c_wraith> | there is no other option |
| 22:23:45 | <Joao003> | ok |
| 22:24:05 | <monochrom> | Yeah pattern matching is the fundamental one. You can write helper functions but it always traces back to pattern matching. |
| 22:24:22 | <monochrom> | Why are you afraid of pattern matching? |
| 22:24:43 | <Joao003> | 'cause i'm pointless |
| 22:25:09 | <Joao003> | see the joke? |
| 22:26:11 | <monochrom> | And when you later graduate to Agda or Coq or Lean or Epigram... then an elimination rule that looks like induction is the even more fundamental one. |
| 22:26:48 | <monochrom> | But patterns or elimination rule, you still cannot escape from addressing "what about the other cases?" |
| 22:27:21 | <darchitect> | monochrom: are you a bot or _ ? |
| 22:27:28 | <glguy> | _ |
| 22:27:38 | <darchitect> | :d |
| 22:27:41 | <monochrom> | I am a Chinese Room, albeit biological. |
| 22:28:19 | <monochrom> | Everyone loves a neurotic Chinese Room, no? \∩/ |
| 22:28:40 | <c_wraith> | hmm. I've seen monochrom accused of many things before, but not being a bot |
| 22:28:55 | <glguy> | c_wraith: time to update your counter |
| 22:29:10 | <c_wraith> | I need a whole new column in on the whiteboard! |
| 22:30:06 | <[Leary]> | If you really want to avoid pattern matching, you can do it by asking GHC to compile System F. |
| 22:30:10 | <monochrom> | Well, consider the other side: I have accused humanity of many things, so it would be absurd if I self-identified as human, no? >:) |
| 22:30:51 | <c_wraith> | nah, that just identifies you as a cynic |
| 22:31:06 | <monochrom> | But System F simply makes you use something close to an elimination rule. |
| 22:32:22 | <monochrom> | And after you have done that in anger, you realize it is only a superficial syntactic difference, it's still pattern matching. |
| 22:32:46 | <Joao003> | to prove monochrom is a bot: |
| 22:32:49 | <Joao003> | monochrom help |
| 22:33:58 | <glguy> | You're going to have to work on your Turing Test |
| 22:34:31 | <c_wraith> | you just need to know the right keyphrase |
| 22:34:32 | <c_wraith> | hey monochrom, how are your students this term? |
| 22:34:44 | <monochrom> | I don't teach a course this term. :) |
| 22:34:52 | <c_wraith> | so.. perfect? |
| 22:34:59 | <monochrom> | Oh next term is going to be nightmare. I have 9am classes. |
| 22:35:40 | <monochrom> | And literally nightmare because normally I should be still sleeping at 9am. >:) |
| 22:35:40 | <c_wraith> | that's inhumane |
| 22:35:53 | × | chele quits (~chele@user/chele) (Remote host closed the connection) |
| 22:36:03 | <darkling> | Could be worse. At least you don't get the 4-5 slot on a Friday afternoon. |
| 22:36:16 | <darchitect> | I like IRC |
| 22:36:17 | <darchitect> | :) |
| 22:36:27 | <Joao003> | darchitect: me too |
| 22:36:41 | <monochrom> | Actually I would enjoy Friday 4-5pm and then tell students "now pub time!" |
| 22:37:09 | <Joao003> | any1 does codewars here? |
| 22:37:19 | <monochrom> | Great saying from Jay Misra after a conference: "Computer science has become a bit too technical, let's go for a drink." |
| 22:37:28 | <c_wraith> | the courses where the instructor said that were some of my favorites |
| 22:37:40 | <monochrom> | And to think that he wrote a lot of very technical papers... |
| 22:37:45 | <Joao003> | monochrom: this is #haskell, not ## |
| 22:38:46 | × | tri quits (~tri@ool-18bc2e74.dyn.optonline.net) (Ping timeout: 276 seconds) |
| 22:39:14 | <xerox> | Joao003: bunch of people in here are doing https://adventofcode.com/ right now |
| 22:39:36 | <monochrom> | I think every 3 years one person comes here and does codewars... |
| 22:39:49 | <Joao003> | xerox: i kno |
| 22:46:32 | <monochrom> | Ugh wait, my colleague has proposed to swap class times with me, now I'm doing the afternoon classes instead! |
| 22:46:51 | <c_wraith> | victory! |
| 22:47:06 | <Joao003> | i hate afternoon classes |
| 22:51:27 | → | nate4 joins (~nate@c-98-45-158-125.hsd1.ca.comcast.net) |
| 22:52:26 | <xerox> | monochrom: when I went to the very first `AngloHaskell's I was very surprised when what you said you would enjoy actually happened every day, I got used to it quite fast (: |
| 22:55:40 | × | alp_ quits (~alp@2001:861:e3d6:8f80:c150:fb83:d53f:eaf2) (Ping timeout: 276 seconds) |
| 22:56:11 | × | nate4 quits (~nate@c-98-45-158-125.hsd1.ca.comcast.net) (Ping timeout: 245 seconds) |
| 22:56:18 | <Joao003> | i think the most useful thing about monads is the fact that `(->) r` is a monad |
| 22:57:59 | × | cwdar^ quits (~cd@c-98-242-74-66.hsd1.ga.comcast.net) (Remote host closed the connection) |
| 23:04:27 | → | not_reserved joins (~not_reser@185.202.220.251) |
| 23:11:58 | × | idgaen quits (~idgaen@2a01:e0a:498:fd50:fcc6:bb5d:489a:ce8c) (Quit: WeeChat 4.1.1) |
| 23:12:31 | → | peterbecich joins (~Thunderbi@047-229-123-186.res.spectrum.com) |
| 23:13:44 | × | acidjnk_new quits (~acidjnk@p200300d6e72b9326b4dc018a2c6658c2.dip0.t-ipconnect.de) (Ping timeout: 256 seconds) |
| 23:23:17 | × | peterbecich quits (~Thunderbi@047-229-123-186.res.spectrum.com) (Ping timeout: 252 seconds) |
| 23:26:40 | × | Tuplanolla quits (~Tuplanoll@91-159-68-236.elisa-laajakaista.fi) (Quit: Leaving.) |
| 23:29:47 | × | jargon quits (~jargon@32.sub-174-238-226.myvzw.com) (Read error: Connection reset by peer) |
| 23:32:20 | → | Joao003_ joins (~Joao003@190.108.99.230) |
| 23:35:23 | × | Joao003 quits (~Joao003@190.108.99.207) (Ping timeout: 252 seconds) |
| 23:35:35 | → | emmanuelux joins (~emmanuelu@user/emmanuelux) |
| 23:35:35 | × | emmanuelux quits (~emmanuelu@user/emmanuelux) (Client Quit) |
| 23:41:58 | × | Joao003_ quits (~Joao003@190.108.99.230) (Quit: Bye!) |
| 23:42:16 | → | Joao003 joins (~Joao003@190.108.99.230) |
| 23:44:08 | → | jargon joins (~jargon@32.sub-174-238-226.myvzw.com) |
| 23:47:06 | <monochrom> | In general, (->)r is very a very underrated functor in programming. It is behind "representable functors" in category theory, and there is a little piece of theory that actually helps a lot with programming, it keeps showing up if you know how to recognize it. |
| 23:47:53 | <monochrom> | s/behind/under the topic of/ |
| 23:48:46 | <ncf> | whenever you need a lemma... |
| 23:48:57 | <monochrom> | Yeah, that. :) |
| 23:51:15 | <monochrom> | So my recent discovery is from learning more about algebraic effects (especially why it's "algebraic"). (And I was interested because Plotkin came to U of Toronto to give a talk on monads and algebraic effects.) (The talk was very dense, but it just means now I really have to read the papers.) |
| 23:52:02 | <Joao003> | monochrom: I mainly use (->) r as a functor in situations involving (>>=) or liftA2 (again, I mainly code pointlessly) |
| 23:52:42 | <monochrom> | The talk and the papers mentioned: for example, if your algebraic effect goes like "choose :: (M a, M a) -> M a", then the "generic" version goes like "() -> M Bool". |
| 23:53:16 | <monochrom> | So I wondered: How is "generic" defined to give that conclusion? |
| 23:54:01 | <monochrom> | After a while, I guessed "Oh! Is it because (X, X) can be represented by Bool -> X?" |
| 23:54:38 | <monochrom> | So I checked the papers and it is like "Theorem: ... Yoneda embedding ..." OK so YES I guessed right! |
| 23:54:53 | <ncf> | should be (a, a) -> M a, probably |
| 23:55:47 | <ncf> | (Bool -> M a) -> M a would be Codensity M Bool |
| 23:55:58 | <monochrom> | Alright here is why it's (M a, M a) -> M a. If you write the free-monad version, you write "data M a = U a | G (M a) (M a)". So G :: M a -> M a -> M a. |
| 23:56:38 | <monochrom> | Err I should have s/G/C/ but meh. |
| 23:57:57 | <monochrom> | And then the generic version will be the actual interface you provide to end users, you provide "c :: MonadChoose m => m Bool" |
All times are in UTC on 2023-12-11.