2021/12/27

2021-12-27 00:00:23 +0100 <web-50> yea, they have very good community too
2021-12-27 00:04:56 +0100wroathe(~wroathe@c-68-54-25-135.hsd1.mn.comcast.net)
2021-12-27 00:04:56 +0100wroathe(~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Changing host)
2021-12-27 00:04:56 +0100wroathe(~wroathe@user/wroathe)
2021-12-27 00:06:40 +0100tromp(~textual@dhcp-077-249-230-040.chello.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
2021-12-27 00:09:27 +0100 <Nolrai2> Lean is very cool.
2021-12-27 00:09:35 +0100wroathe(~wroathe@user/wroathe) (Ping timeout: 256 seconds)
2021-12-27 00:09:46 +0100 <Nolrai2> Is getting hmatrix to work on windows hard?
2021-12-27 00:10:37 +0100 <Nolrai2> The "matrix" libray is 1-indexed which is just painful to use.
2021-12-27 00:15:42 +0100__monty__(~toonn@user/toonn) (Quit: leaving)
2021-12-27 00:16:24 +0100lavaman(~lavaman@98.38.249.169)
2021-12-27 00:20:37 +0100lavaman(~lavaman@98.38.249.169) (Ping timeout: 240 seconds)
2021-12-27 00:27:37 +0100mvk(~mvk@2607:fea8:5cdd:f000::917a) (Ping timeout: 240 seconds)
2021-12-27 00:28:06 +0100jpds(~jpds@gateway/tor-sasl/jpds) (Ping timeout: 276 seconds)
2021-12-27 00:29:40 +0100jpds(~jpds@gateway/tor-sasl/jpds)
2021-12-27 00:30:30 +0100AlexNoo_(~AlexNoo@178.34.163.120)
2021-12-27 00:32:49 +0100Alex_test(~al_test@178.34.160.99) (Ping timeout: 256 seconds)
2021-12-27 00:33:37 +0100AlexZenon(~alzenon@178.34.160.99) (Ping timeout: 240 seconds)
2021-12-27 00:33:57 +0100AlexNoo(~AlexNoo@178.34.160.99) (Ping timeout: 240 seconds)
2021-12-27 00:34:41 +0100eggplantade(~Eggplanta@2600:1700:bef1:5e10:b417:46a:3118:ab81) (Remote host closed the connection)
2021-12-27 00:36:44 +0100merijn(~merijn@83-160-49-249.ip.xs4all.nl)
2021-12-27 00:36:49 +0100zerozzz
2021-12-27 00:37:21 +0100AlexNoo_AlexNoo
2021-12-27 00:38:26 +0100timCF(~timCF@m91-129-100-224.cust.tele2.ee) (Quit: leaving)
2021-12-27 00:38:35 +0100Alex_test(~al_test@178.34.163.120)
2021-12-27 00:39:06 +0100AlexZenon(~alzenon@178.34.163.120)
2021-12-27 00:41:32 +0100Erutuon(~Erutuon@user/erutuon) (Ping timeout: 240 seconds)
2021-12-27 00:42:17 +0100python476(~user@88.160.31.174) (Ping timeout: 250 seconds)
2021-12-27 00:49:18 +0100wroathe(~wroathe@c-68-54-25-135.hsd1.mn.comcast.net)
2021-12-27 00:49:18 +0100wroathe(~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Changing host)
2021-12-27 00:49:18 +0100wroathe(~wroathe@user/wroathe)
2021-12-27 00:51:49 +0100aallen(~aallen@072-182-074-253.res.spectrum.com)
2021-12-27 00:52:42 +0100Guest|70(~Guest|70@c-24-6-12-87.hsd1.ca.comcast.net) (Quit: Ping timeout (120 seconds))
2021-12-27 01:02:49 +0100eggplantade(~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net)
2021-12-27 01:03:25 +0100 <EvanR> is there any state of the art on implicit configurations I'm not aware of... is reflection still the latest for that
2021-12-27 01:07:03 +0100max22-(~maxime@2a01cb088335980093d703d768803864.ipv6.abo.wanadoo.fr) (Remote host closed the connection)
2021-12-27 01:07:29 +0100 <iphy> EvanR: https://github.com/iphydf/hs-cimple/commit/19e45c13acbaea04182674ec6be1db9f23369975
2021-12-27 01:08:46 +0100 <iphy> EvanR: so now I have Fix around everything, how can I put attributes on it?
2021-12-27 01:09:22 +0100 <iphy> I removed the Attr node
2021-12-27 01:09:26 +0100kjak(~kjak@pool-108-45-56-21.washdc.fios.verizon.net) (Ping timeout: 252 seconds)
2021-12-27 01:10:06 +0100 <iphy> I guess I'll need something like Fix but with another property on it
2021-12-27 01:10:32 +0100merijn(~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 240 seconds)
2021-12-27 01:10:34 +0100 <iphy> can TraverseAst be made to work on any arbitrary Fix-like type?
2021-12-27 01:10:58 +0100 <iphy> maybe the Fix-like object needs a class that unwraps it
2021-12-27 01:11:17 +0100 <iphy> this will be a puzzle for another day :)
2021-12-27 01:13:16 +0100dcoutts_(~duncan@71.78.6.51.dyn.plus.net)
2021-12-27 01:18:49 +0100albet70(~xxx@2400:8902::f03c:92ff:fe60:98d8) (Remote host closed the connection)
2021-12-27 01:19:37 +0100dcoutts_(~duncan@71.78.6.51.dyn.plus.net) (Ping timeout: 240 seconds)
2021-12-27 01:23:12 +0100Everything(~Everythin@37.115.210.35) (Quit: leaving)
2021-12-27 01:23:56 +0100dcoutts_(~duncan@71.78.6.51.dyn.plus.net)
2021-12-27 01:24:52 +0100 <iphy> EvanR: I'm not sure what this refactoring bought me, what did I get for free?
2021-12-27 01:24:56 +0100albet70(~xxx@2400:8902::f03c:92ff:fe60:98d8)
2021-12-27 01:25:43 +0100 <iphy> can TraverseAst be automatic now?
2021-12-27 01:26:41 +0100burakcank(~burakcank@has.arrived.and.is.ready-to.party) (Quit: fBNC - https://bnc4free.com)
2021-12-27 01:27:09 +0100burnsidesLlama(~burnsides@dhcp168-010.wadham.ox.ac.uk)
2021-12-27 01:29:14 +0100vysn(~vysn@user/vysn) (Ping timeout: 252 seconds)
2021-12-27 01:31:49 +0100burnsidesLlama(~burnsides@dhcp168-010.wadham.ox.ac.uk) (Ping timeout: 268 seconds)
2021-12-27 01:37:56 +0100DNH(~DNH@2a02:8108:1100:16d8:6043:aa58:f99b:e1b) (Quit: My MacBook has gone to sleep. ZZZzzz…)
2021-12-27 01:40:07 +0100kjak(~kjak@pool-108-45-56-21.washdc.fios.verizon.net)
2021-12-27 01:43:05 +0100seiryn(~seiryn@2a01cb040147e000e4dbf764ff30bd96.ipv6.abo.wanadoo.fr)
2021-12-27 01:44:46 +0100acidjnk(~acidjnk@p200300d0c7271e72b97741cdfe77e27f.dip0.t-ipconnect.de) (Ping timeout: 260 seconds)
2021-12-27 01:48:34 +0100 <iphy> EvanR: what would a function look like that adds attributes to an existing AST wrapped in Fix?
2021-12-27 01:52:52 +0100kupi(uid212005@id-212005.hampstead.irccloud.com)
2021-12-27 02:02:33 +0100mvk(~mvk@2607:fea8:5cdd:f000::917a)
2021-12-27 02:02:49 +0100Nolrai2(~Nolrai2@73.240.1.39) (Quit: Client closed)
2021-12-27 02:09:57 +0100waleee(~waleee@2001:9b0:21d:fc00:398f:b003:b90d:acf4) (Ping timeout: 240 seconds)
2021-12-27 02:10:43 +0100aallen(~aallen@072-182-074-253.res.spectrum.com) (Ping timeout: 256 seconds)
2021-12-27 02:11:49 +0100albet70(~xxx@2400:8902::f03c:92ff:fe60:98d8) (Remote host closed the connection)
2021-12-27 02:17:56 +0100albet70(~xxx@2400:8902::f03c:92ff:fe60:98d8)
2021-12-27 02:27:40 +0100Alleria(~textual@user/alleria) (Quit: Textual IRC Client: www.textualapp.com)
2021-12-27 02:29:55 +0100falafel_(~falafel@2603-8000-d800-688c-502d-7280-71cc-20e7.res6.spectrum.com)
2021-12-27 02:30:24 +0100machinedgod(~machinedg@24.105.81.50) (Ping timeout: 268 seconds)
2021-12-27 02:30:32 +0100falafel__(~falafel@2603-8000-d800-688c-9993-a5d6-8c3d-400e.res6.spectrum.com)
2021-12-27 02:31:35 +0100burakcank(~burakcank@has.arrived.and.is.ready-to.party)
2021-12-27 02:33:22 +0100 <energizer> "broadcast vs map" https://julialang.org/blog/2017/01/moredots/#broadcast_vs_map is there a function like broadcast in haskell?
2021-12-27 02:34:17 +0100falafel_(~falafel@2603-8000-d800-688c-502d-7280-71cc-20e7.res6.spectrum.com) (Ping timeout: 240 seconds)
2021-12-27 02:34:17 +0100dcoutts_(~duncan@71.78.6.51.dyn.plus.net) (Ping timeout: 240 seconds)
2021-12-27 02:36:24 +0100 <dsal> energizer: I don't know Julia. Can you describe what you're trying to do?
2021-12-27 02:36:39 +0100kaph(~kaph@net-2-38-107-19.cust.vodafonedsl.it)
2021-12-27 02:36:40 +0100 <energizer> dsal: this is just idle curiosity
2021-12-27 02:37:21 +0100geekosaur(~geekosaur@xmonad/geekosaur) (Remote host closed the connection)
2021-12-27 02:37:41 +0100 <dsal> Well, sure, but I don't understand what broadcast is meant to do and don't have enough background in julia to figure out what it's trying to do.
2021-12-27 02:39:07 +0100burnsidesLlama(~burnsides@dhcp168-010.wadham.ox.ac.uk)
2021-12-27 02:39:24 +0100geekosaur(~geekosaur@xmonad/geekosaur)
2021-12-27 02:43:17 +0100burnsidesLlama(~burnsides@dhcp168-010.wadham.ox.ac.uk) (Ping timeout: 240 seconds)
2021-12-27 02:47:37 +0100falafel__(~falafel@2603-8000-d800-688c-9993-a5d6-8c3d-400e.res6.spectrum.com) (Ping timeout: 240 seconds)
2021-12-27 02:50:47 +0100arahael(~arahael@203.158.51.1) (Quit: WeeChat 3.1)
2021-12-27 02:56:59 +0100Lycurgus(~juan@98.4.112.204)
2021-12-27 02:57:59 +0100 <Lycurgus> int-e, how did you get 208.94.116.26 for lyah dot com?
2021-12-27 03:00:23 +0100 <Lycurgus> in any case, it having been gone for sure for several days and with that (nearlyfreespeech) as the last hosting
2021-12-27 03:01:26 +0100 <Lycurgus> accepting author has moved on, doesn't care with > 80% confidence
2021-12-27 03:02:40 +0100 <Lycurgus> with the complementary (< 20%) likelihood the author will bring back at his expense
2021-12-27 03:07:20 +0100merijn(~merijn@83-160-49-249.ip.xs4all.nl)
2021-12-27 03:09:10 +0100Vajb(~Vajb@hag-jnsbng11-58c3a8-176.dhcp.inet.fi) (Read error: Connection reset by peer)
2021-12-27 03:09:22 +0100Vajb(~Vajb@hag-jnsbng11-58c3a8-176.dhcp.inet.fi)
2021-12-27 03:17:34 +0100machinedgod(~machinedg@24.105.81.50)
2021-12-27 03:17:44 +0100drewr(~drew@user/drewr)
2021-12-27 03:17:52 +0100AlexNoo_(~AlexNoo@178.34.163.120)
2021-12-27 03:17:56 +0100qrpnxz(abc4f95c31@user/qrpnxz) (Disconnected: Replaced by new connection)
2021-12-27 03:17:57 +0100qrpnxz(abc4f95c31@user/qrpnxz)
2021-12-27 03:18:41 +0100 <EvanR> iphy, maybe Fix (AttrF `Compose` ExprF)
2021-12-27 03:18:48 +0100AlexNoo(~AlexNoo@178.34.163.120) (Read error: Connection reset by peer)
2021-12-27 03:24:57 +0100drewr(~drew@user/drewr) (Ping timeout: 240 seconds)
2021-12-27 03:31:55 +0100jackson99(~bc8147f2@cerf.good1.com)
2021-12-27 03:34:23 +0100 <otherwise> foldl starts at the left side of a list, and moves to the right through the list?
2021-12-27 03:35:01 +0100Midjak(~Midjak@may53-1-78-226-116-92.fbx.proxad.net) (Quit: This computer has gone to sleep)
2021-12-27 03:35:49 +0100 <geekosaur> both foldl and foldr do. (you can't start at the "right end" of a list, and the notion is incompatible with foldr being able to handle infinite lists)
2021-12-27 03:36:03 +0100 <geekosaur> foldl left-associates; foldr right-associates
2021-12-27 03:36:12 +0100 <geekosaur> > foldr f z [a,b,c]
2021-12-27 03:36:13 +0100 <lambdabot> f a (f b (f c z))
2021-12-27 03:36:18 +0100 <geekosaur> > foldl f z [a,b,c]
2021-12-27 03:36:19 +0100 <lambdabot> f (f (f z a) b) c
2021-12-27 03:37:29 +0100 <geekosaur> if anything, left associativity means it's foldl that "starts at the right", as shown there
2021-12-27 03:39:18 +0100 <dsal> otherwise: foldr works with infinite lists. It’s a good default when you don’t care
2021-12-27 03:40:45 +0100 <dsal> > foldr (\x o -> 3) 5 [11..]
2021-12-27 03:40:47 +0100 <lambdabot> 3
2021-12-27 03:41:29 +0100neurocyte0132889(~neurocyte@user/neurocyte) (Ping timeout: 250 seconds)
2021-12-27 03:42:06 +0100 <geekosaur> foldr works more naturally with lists because they're right-associative to begin with
2021-12-27 03:42:11 +0100 <geekosaur> % :info (:)
2021-12-27 03:42:11 +0100 <yahb> geekosaur: type [] :: * -> *; data [] a = ... | a : [a]; -- Defined in `GHC.Types'; infixr 5 :
2021-12-27 03:43:38 +0100BrokenClutch(~pioneer@2804:d41:c2a7:d800:e627:b00b:2c62:134) ()
2021-12-27 03:44:13 +0100merijn(~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 240 seconds)
2021-12-27 03:49:20 +0100xff0x(~xff0x@2001:1a81:538d:1a00:d6e3:ac9b:2d1c:a9e) (Ping timeout: 268 seconds)
2021-12-27 03:50:59 +0100xff0x(~xff0x@2001:1a81:53c9:5600:a4b4:57a2:f2c0:c793)
2021-12-27 03:51:31 +0100seiryn(~seiryn@2a01cb040147e000e4dbf764ff30bd96.ipv6.abo.wanadoo.fr) (Quit: WeeChat 3.3)
2021-12-27 03:51:33 +0100 <otherwise> implementing map with foldr:
2021-12-27 03:51:42 +0100 <otherwise> > let mapFoldr f xs = foldr (\x acc -> f x : acc) [] xs in mapFoldr (+1) [1..5]
2021-12-27 03:51:44 +0100 <lambdabot> [2,3,4,5,6]
2021-12-27 03:52:01 +0100 <EvanR> with eager evaluation, foldr would cause f c z to "happen first", in foldl f z a "happens first", as shown with those expansions from lambdabot
2021-12-27 03:52:23 +0100 <otherwise> then with foldr:
2021-12-27 03:52:25 +0100 <otherwise> > let mapFoldl f xs = foldl (\acc x -> f x : acc) [] xs in mapFoldl (+1) [1..5]
2021-12-27 03:52:26 +0100 <lambdabot> [6,5,4,3,2]
2021-12-27 03:52:34 +0100 <otherwise> it is reversed
2021-12-27 03:52:36 +0100 <EvanR> with lazy evaluation it's neither of those
2021-12-27 03:53:42 +0100 <otherwise> hmm okay, i'll mull it over
2021-12-27 03:54:22 +0100 <EvanR> in particular the expansions don't properly explain the operational aspect of foldl
2021-12-27 03:54:29 +0100 <EvanR> (lazy version)
2021-12-27 03:55:06 +0100fizbin(~fizbin@c-73-33-197-160.hsd1.nj.comcast.net)
2021-12-27 03:56:06 +0100Pickchea(~private@user/pickchea) (Ping timeout: 268 seconds)
2021-12-27 03:58:48 +0100pretty_dumm_guy(trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655) (Quit: WeeChat 3.4)
2021-12-27 03:59:17 +0100fizbin(~fizbin@c-73-33-197-160.hsd1.nj.comcast.net) (Ping timeout: 240 seconds)
2021-12-27 04:00:55 +0100Lycurgus(~juan@98.4.112.204) (Quit: Exeunt)
2021-12-27 04:04:42 +0100lemonsnicks(~lemonsnic@cpc159519-perr18-2-0-cust114.19-1.cable.virginm.net) (Quit: ZNC 1.8.2 - https://znc.in)
2021-12-27 04:06:06 +0100 <iphy> EvanR: hm interesting
2021-12-27 04:09:46 +0100 <otherwise> how do I make ghci do:
2021-12-27 04:09:48 +0100 <otherwise> > foldl f z [a,b,c]
2021-12-27 04:09:49 +0100 <lambdabot> f (f (f z a) b) c
2021-12-27 04:10:19 +0100 <xsperry> :t foldl f z [a,b,c]
2021-12-27 04:10:20 +0100 <lambdabot> Expr
2021-12-27 04:10:24 +0100 <xsperry> @hoogle Expr
2021-12-27 04:10:25 +0100 <lambdabot> Test.Tasty.Patterns.Types data Expr
2021-12-27 04:10:25 +0100 <lambdabot> module Text.Parsec.Expr
2021-12-27 04:10:25 +0100 <lambdabot> module Text.ParserCombinators.Parsec.Expr
2021-12-27 04:10:26 +0100 <otherwise> import Data.lambdabot or something?
2021-12-27 04:14:50 +0100 <xsperry> it is a separate library, but I can't recall its name.
2021-12-27 04:16:19 +0100 <otherwise> after doing "import Text.ParserCombinators.Parsec.Expr" now my prelude is "Prelude Text.ParserCombinators.Parsec.Expr> "
2021-12-27 04:16:45 +0100 <otherwise> and :browse gives something new
2021-12-27 04:17:00 +0100 <xsperry> no that isn't it, Parsec is a parsing package
2021-12-27 04:17:43 +0100lemonsnicks(~lemonsnic@cpc159519-perr18-2-0-cust114.19-1.cable.virginm.net)
2021-12-27 04:18:13 +0100lavaman(~lavaman@98.38.249.169)
2021-12-27 04:21:36 +0100 <dsal> > f [Expr]
2021-12-27 04:21:36 +0100 <otherwise> dsal foldl does not work on infinite lists because there is not an element to start moving left from (last item in the list)? I hope thats the case cause it makes sense to me.
2021-12-27 04:21:38 +0100 <lambdabot> error:
2021-12-27 04:21:38 +0100 <lambdabot> • Data constructor not in scope: Expr
2021-12-27 04:21:38 +0100 <lambdabot> • Perhaps you meant variable ‘expr’ (imported from Debug.SimpleReflect)
2021-12-27 04:21:49 +0100 <dsal> Simple reflect
2021-12-27 04:22:18 +0100 <dsal> otherwise: yeah, you can see it in the expansion above
2021-12-27 04:22:36 +0100kupi(uid212005@id-212005.hampstead.irccloud.com) (Quit: Connection closed for inactivity)
2021-12-27 04:23:14 +0100lavaman(~lavaman@98.38.249.169) (Ping timeout: 268 seconds)
2021-12-27 04:23:17 +0100Rum(~bourbon@user/rum)
2021-12-27 04:34:00 +0100FinnElija(~finn_elij@user/finn-elija/x-0085643) (Killed (NickServ (Forcing logout FinnElija -> finn_elija)))
2021-12-27 04:34:00 +0100finn_elija(~finn_elij@user/finn-elija/x-0085643)
2021-12-27 04:34:00 +0100finn_elijaFinnElija
2021-12-27 04:34:06 +0100 <iphy> EvanR: "well at least you get map and fold for free" <- where is map?
2021-12-27 04:36:15 +0100 <jackson99> otherwise, did you figure out list of functions issue you had earlier today?
2021-12-27 04:40:27 +0100neceve(~quassel@2.26.93.228) (Ping timeout: 256 seconds)
2021-12-27 04:40:56 +0100 <int-e> lyxia: I googled for a cached DNS query (since there are websites that do DNS queries)
2021-12-27 04:41:23 +0100 <int-e> oh no
2021-12-27 04:41:37 +0100 <int-e> that was for Lycurgus who left
2021-12-27 04:41:59 +0100 <otherwise> jackson99 no
2021-12-27 04:42:33 +0100 <jackson99> :t map (*) [1,2,3,4]
2021-12-27 04:42:33 +0100 <lambdabot> Num a => [a -> a]
2021-12-27 04:42:35 +0100 <otherwise> I still don't know how to use take on (map (*) [0..5])
2021-12-27 04:42:37 +0100 <otherwise> or any list
2021-12-27 04:42:52 +0100 <jackson99> > map ($10) (map (*) [1,2,3,4])
2021-12-27 04:42:53 +0100 <lambdabot> [10,20,30,40]
2021-12-27 04:42:54 +0100 <otherwise> I can get it to evaluate the head of a list
2021-12-27 04:43:13 +0100 <otherwise> hmm
2021-12-27 04:43:15 +0100 <jackson99> or with lambda
2021-12-27 04:43:23 +0100 <jackson99> > map (\f -> f 10) (map (*) [1,2,3,4])
2021-12-27 04:43:25 +0100 <lambdabot> [10,20,30,40]
2021-12-27 04:43:35 +0100 <jackson99> or you can just do:
2021-12-27 04:43:58 +0100 <jackson99> > map (*10) [1,2,3,4]
2021-12-27 04:44:00 +0100 <lambdabot> [10,20,30,40]
2021-12-27 04:44:11 +0100 <jackson99> unless the goal was specifically to build a list of functions for some reason
2021-12-27 04:46:59 +0100 <otherwise> okay, i'll see if I can not make take work on (map (*) [0..])
2021-12-27 04:48:18 +0100aallen(~aallen@072-182-074-253.res.spectrum.com)
2021-12-27 04:48:45 +0100 <otherwise> > let funList = map (*) [0..] in take 3 (map ($10) funList)
2021-12-27 04:48:46 +0100 <lambdabot> [0,10,20]
2021-12-27 04:48:58 +0100 <otherwise> dear god. that took hours to make work
2021-12-27 04:49:06 +0100 <otherwise> 100's of failed attempts
2021-12-27 04:49:21 +0100 <otherwise> thank you dearly
2021-12-27 04:50:12 +0100aallen(~aallen@072-182-074-253.res.spectrum.com) (Client Quit)
2021-12-27 04:52:07 +0100burnsidesLlama(~burnsides@dhcp168-010.wadham.ox.ac.uk)
2021-12-27 04:52:54 +0100 <otherwise> > let funList n m = take n (map ($m) (map (*) [0..])) in funList 10 3
2021-12-27 04:52:55 +0100 <lambdabot> [0,3,6,9,12,15,18,21,24,27]
2021-12-27 04:53:13 +0100 <otherwise> awwww, how refreshing
2021-12-27 04:53:54 +0100 <jackson99> do you know what $ is?
2021-12-27 04:54:36 +0100 <otherwise> precedence demoter
2021-12-27 04:54:45 +0100 <jackson99> > let funList n m = take n (map (*m) [0..])) in funList 10 3
2021-12-27 04:54:46 +0100 <otherwise> or something like that
2021-12-27 04:54:47 +0100 <lambdabot> <hint>:1:42: error: parse error on input ‘)’
2021-12-27 04:54:51 +0100 <jackson99> > let funList n m = take n (map (*m) [0..]) in funList 10 3
2021-12-27 04:54:53 +0100 <lambdabot> [0,3,6,9,12,15,18,21,24,27]
2021-12-27 04:54:57 +0100 <jackson99> no need for double map
2021-12-27 04:56:17 +0100burnsidesLlama(~burnsides@dhcp168-010.wadham.ox.ac.uk) (Ping timeout: 240 seconds)
2021-12-27 04:56:46 +0100 <otherwise> right, but that is skipping the whole notion of "I have a list of partial application functions, how do I enter it and evaluate the function"
2021-12-27 04:57:16 +0100 <otherwise> I agree, for that line of code, skipping the map (*) is the logical thing to do
2021-12-27 04:57:35 +0100 <iphy> EvanR: https://github.com/TokTok/hs-cimple/blob/master/src/Language/Cimple/Pretty.hs#L389-L397 how would something like this work with foldFix?
2021-12-27 04:57:45 +0100 <jackson99> use a lambda then, easier to understand than $, since you don't seem to know what $ is
2021-12-27 04:58:07 +0100 <otherwise> But I was approaching as if I had a preexisting [(0*), (1*), ..] and then using take on it
2021-12-27 04:58:16 +0100 <otherwise> haha
2021-12-27 04:58:16 +0100 <iphy> https://github.com/iphydf/hs-cimple/blob/fix/src/Language/Cimple/Pretty.hs#L387-L395 <- here is the Fix version
2021-12-27 04:58:54 +0100td_(~td@94.134.91.110) (Ping timeout: 260 seconds)
2021-12-27 04:58:59 +0100nattiestnate(~nate@2001:448a:20a0:4134:25e:715f:d637:5263)
2021-12-27 05:00:00 +0100 <jackson99> that's not a knock on you, $ is confusing at first
2021-12-27 05:00:13 +0100 <dsal> :src ($)
2021-12-27 05:00:18 +0100 <dsal> @src ($)
2021-12-27 05:00:18 +0100 <lambdabot> f $ x = f x
2021-12-27 05:00:24 +0100td_(~td@muedsl-82-207-238-094.citykom.de)
2021-12-27 05:00:35 +0100yauhsien(~yauhsien@61-231-42-148.dynamic-ip.hinet.net)
2021-12-27 05:00:49 +0100mbuf(~Shakthi@122.178.203.86)
2021-12-27 05:02:58 +0100qrpnxz(abc4f95c31@user/qrpnxz) (Disconnected: Replaced by new connection)
2021-12-27 05:02:59 +0100qrpnxz(abc4f95c31@user/qrpnxz)
2021-12-27 05:03:28 +0100qrpnxz(abc4f95c31@user/qrpnxz) (Disconnected: closed)
2021-12-27 05:03:38 +0100qrpnxz(abc4f95c31@user/qrpnxz)
2021-12-27 05:04:57 +0100yauhsien(~yauhsien@61-231-42-148.dynamic-ip.hinet.net) (Ping timeout: 240 seconds)
2021-12-27 05:07:11 +0100 <otherwise> When I try to read :doc in ghci, all the @ symbols throw me off, what do they mean, or better yet, how to I translate it into an english sentence? the same way I'd translate 3+2 into Three plus two, for ex...
2021-12-27 05:07:47 +0100 <dsal> I've never used that feature. I should try it.
2021-12-27 05:08:14 +0100 <dsal> Oh, it's just haddock stuff.
2021-12-27 05:08:52 +0100 <otherwise> > :doc $
2021-12-27 05:08:53 +0100 <lambdabot> <hint>:1:1: error: parse error on input ‘:’
2021-12-27 05:08:56 +0100 <c_wraith> Yeah, that's a major issue with :doc right now
2021-12-27 05:09:09 +0100 <dsal> % :doc ($)
2021-12-27 05:09:09 +0100 <yahb> dsal: Application operator. This operator is redundant, since ordinary; application @(f x)@ means the same as @(f '$' x)@. However, '$' has; low, right-associative binding precedence, so it sometimes allows; parentheses to be omitted; for example:; > f $ g $ h x = f (g (h x)); It is also useful in higher-order situations, such as @'map' ('$' 0) xs@,; or @'Data.List.zipWith' ('$') fs xs@.; Note th
2021-12-27 05:09:18 +0100 <c_wraith> there needs to be some effort made in rendering haddock to plain text
2021-12-27 05:09:25 +0100 <otherwise> its probably better that way, it would just blow up the chat with lots of lines
2021-12-27 05:09:41 +0100 <otherwise> oh, there it is
2021-12-27 05:10:03 +0100 <otherwise> yea, all those @ symbols!
2021-12-27 05:10:07 +0100 <c_wraith> otherwise: haddock uses @ to start and end inline code formatting
2021-12-27 05:10:13 +0100 <c_wraith> they don't mean anything
2021-12-27 05:11:22 +0100 <c_wraith> or rather, they don't mean anything as code, because they're markup. Not code. They're rendering instructions that :doc ignores and decides to print instead
2021-12-27 05:12:37 +0100notzmv(~zmv@user/notzmv) (Ping timeout: 240 seconds)
2021-12-27 05:12:48 +0100 <c_wraith> Same as the ' around identifiers - haddock for "generate a link to this symbol"
2021-12-27 05:13:12 +0100 <otherwise> got it
2021-12-27 05:13:50 +0100yauhsien(~yauhsien@61-231-42-148.dynamic-ip.hinet.net)
2021-12-27 05:20:51 +0100nattiestnate(~nate@2001:448a:20a0:4134:25e:715f:d637:5263) (Quit: WeeChat 3.4)
2021-12-27 05:21:04 +0100nattiestnate(~nate@2001:448a:20a0:4134:25e:715f:d637:5263)
2021-12-27 05:21:58 +0100justsomeguy(~justsomeg@user/justsomeguy)
2021-12-27 05:22:45 +0100 <otherwise> jackson99 and c_wraith thank you :)
2021-12-27 05:25:58 +0100otherwise(~otherwise@c-73-221-44-172.hsd1.wa.comcast.net) ()
2021-12-27 05:26:55 +0100machinedgod(~machinedg@24.105.81.50) (Ping timeout: 256 seconds)
2021-12-27 05:30:03 +0100Feuermagier(~Feuermagi@user/feuermagier)
2021-12-27 05:30:27 +0100deadmarshal(~deadmarsh@95.38.116.71)
2021-12-27 05:38:30 +0100zebrag(~chris@user/zebrag)
2021-12-27 05:40:07 +0100Rum(~bourbon@user/rum) (Quit: WeeChat 3.4)
2021-12-27 05:40:59 +0100merijn(~merijn@83-160-49-249.ip.xs4all.nl)
2021-12-27 05:49:09 +0100Morrow(~quassel@bzq-110-168-31-106.red.bezeqint.net) (Remote host closed the connection)
2021-12-27 05:49:12 +0100yauhsien(~yauhsien@61-231-42-148.dynamic-ip.hinet.net) (Remote host closed the connection)
2021-12-27 05:49:39 +0100yauhsien(~yauhsien@61-231-42-148.dynamic-ip.hinet.net)
2021-12-27 05:50:14 +0100Morrow(~quassel@bzq-110-168-31-106.red.bezeqint.net)
2021-12-27 05:52:53 +0100nattiestnate(~nate@2001:448a:20a0:4134:25e:715f:d637:5263) (Quit: WeeChat 3.4)
2021-12-27 05:54:02 +0100yauhsien(~yauhsien@61-231-42-148.dynamic-ip.hinet.net) (Ping timeout: 240 seconds)
2021-12-27 05:55:09 +0100nattiestnate(~nate@2001:448a:20a0:4134:25e:715f:d637:5263)
2021-12-27 05:59:04 +0100nattiestnate(~nate@2001:448a:20a0:4134:25e:715f:d637:5263) (Client Quit)
2021-12-27 06:00:17 +0100Erutuon(~Erutuon@user/erutuon)
2021-12-27 06:00:19 +0100joo-_(~joo-_@fsf/member/joo--) (Quit: leaving)
2021-12-27 06:00:34 +0100joo-_(~joo-_@87-49-147-205-mobile.dk.customer.tdc.net)
2021-12-27 06:00:34 +0100joo-_(~joo-_@87-49-147-205-mobile.dk.customer.tdc.net) (Changing host)
2021-12-27 06:00:34 +0100joo-_(~joo-_@fsf/member/joo--)
2021-12-27 06:04:05 +0100takuan(~takuan@178-116-218-225.access.telenet.be)
2021-12-27 06:04:27 +0100Morrow(~quassel@bzq-110-168-31-106.red.bezeqint.net) (Remote host closed the connection)
2021-12-27 06:05:17 +0100jinsun(~quassel@user/jinsun) (Ping timeout: 240 seconds)
2021-12-27 06:06:06 +0100jinsun(~quassel@user/jinsun)
2021-12-27 06:07:36 +0100cherryblossom[m](~cherryblo@2001:470:69fc:105::b789)
2021-12-27 06:10:12 +0100[itchyjunk](~itchyjunk@user/itchyjunk/x-7353470)
2021-12-27 06:14:57 +0100merijn(~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 240 seconds)
2021-12-27 06:20:50 +0100 <EvanR> iphy, map is Functor
2021-12-27 06:23:18 +0100joo-_(~joo-_@fsf/member/joo--) (Quit: Lost terminal)
2021-12-27 06:24:02 +0100joo-_(~joo-_@87-49-147-205-mobile.dk.customer.tdc.net)
2021-12-27 06:24:02 +0100joo-_(~joo-_@87-49-147-205-mobile.dk.customer.tdc.net) (Changing host)
2021-12-27 06:24:02 +0100joo-_(~joo-_@fsf/member/joo--)
2021-12-27 06:26:02 +0100 <[itchyjunk]> :i
2021-12-27 06:26:04 +0100 <[itchyjunk]> :o
2021-12-27 06:26:41 +0100justsomeguy(~justsomeg@user/justsomeguy) (Quit: WeeChat 3.3)
2021-12-27 06:29:50 +0100 <jackson99> % :i Functor
2021-12-27 06:29:50 +0100 <yahb> jackson99: type Functor :: (* -> *) -> Constraint; class Functor f where; fmap :: (a -> b) -> f a -> f b; (<$) :: a -> f b -> f a; {-# MINIMAL fmap #-}; -- Defined in `GHC.Base'; instance [safe] Functor m => Functor (WriterT w m) -- Defined in `Control.Monad.Trans.Writer.Lazy'; instance [safe] Functor m => Functor (StateT s m) -- Defined in `Control.Monad.Trans.State.Lazy'; instance [safe] Functor m => Func
2021-12-27 06:31:04 +0100DNH(~DNH@2a02:8108:1100:16d8:6043:aa58:f99b:e1b)
2021-12-27 06:31:30 +0100zebrag(~chris@user/zebrag) (Quit: Konversation terminated!)
2021-12-27 06:33:40 +0100alfonsox(~quassel@103.92.42.104)
2021-12-27 06:34:45 +0100TonyStone(~TonyStone@cpe-74-76-51-197.nycap.res.rr.com) (Remote host closed the connection)
2021-12-27 06:35:30 +0100DNH(~DNH@2a02:8108:1100:16d8:6043:aa58:f99b:e1b) (Ping timeout: 260 seconds)
2021-12-27 06:36:06 +0100 <alfonsox> is learnyouhaskell.com down ?
2021-12-27 06:36:45 +0100otherwise(~otherwise@2601:602:880:90f0:7490:2afa:37a4:523b)
2021-12-27 06:36:59 +0100 <dsal> I've heard resolution complaints today.
2021-12-27 06:37:36 +0100[itchyjunk](~itchyjunk@user/itchyjunk/x-7353470) (Remote host closed the connection)
2021-12-27 06:38:00 +0100 <jackson99> it is down
2021-12-27 06:38:08 +0100 <jackson99> but you can read it in here. https://web.archive.org/web/20211204094509/http://learnyouahaskell.com/
2021-12-27 06:39:44 +0100 <alfonsox> learnyouahaskell.com’s server IP address could not be found. This is what I am getting in chrome.
2021-12-27 06:40:14 +0100 <alfonsox> Thank you @jackson99. I'll use web.archive for now.
2021-12-27 06:42:27 +0100 <alfonsox> Anyone have authors email ? bonus at learnyouahaskell dot com ( mentioned at site), but not sure if email will reach to him due to name resolution error.
2021-12-27 06:49:17 +0100wroathe(~wroathe@user/wroathe) (Ping timeout: 240 seconds)
2021-12-27 06:49:26 +0100 <EvanR> maybe it's time for the next learn you a haskell xD
2021-12-27 06:51:03 +0100yauhsien(~yauhsien@61-231-42-148.dynamic-ip.hinet.net)
2021-12-27 06:56:30 +0100yauhsien(~yauhsien@61-231-42-148.dynamic-ip.hinet.net) (Ping timeout: 260 seconds)
2021-12-27 07:05:26 +0100wroathe(~wroathe@c-68-54-25-135.hsd1.mn.comcast.net)
2021-12-27 07:05:26 +0100wroathe(~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Changing host)
2021-12-27 07:05:26 +0100wroathe(~wroathe@user/wroathe)
2021-12-27 07:07:49 +0100rekahsoft(~rekahsoft@cpe0008a20f982f-cm64777d666260.cpe.net.cable.rogers.com) (Ping timeout: 240 seconds)
2021-12-27 07:07:49 +0100nattiestnate(~nate@182.3.37.200)
2021-12-27 07:08:46 +0100 <otherwise> Are you writing EvanR ?
2021-12-27 07:09:13 +0100 <otherwise> big public irc book reveal?
2021-12-27 07:09:48 +0100 <EvanR> I can't justify that, I don't know enough haskell
2021-12-27 07:10:26 +0100 <EvanR> Besides, I think learning haskell would be better as an old school text adventure (with graphics)
2021-12-27 07:11:31 +0100 <otherwise> Yes, I agree about that format, that should be the next standard. I think haskell.org homepage tutorial is a very rudimentary version of that. It is good and could be expanded creatively
2021-12-27 07:12:04 +0100 <EvanR> as always the key is collecting the proper exercises
2021-12-27 07:13:50 +0100 <otherwise> well the storyline would somewhat dictate that. As long as you keep to the story line, the exercises would just fall in place. (easier said than realized...)
2021-12-27 07:15:09 +0100 <EvanR> one of the two is much harder to come up with
2021-12-27 07:16:17 +0100wroathe(~wroathe@user/wroathe) (Ping timeout: 256 seconds)
2021-12-27 07:19:24 +0100 <otherwise> hmm, I just realized all the haskell I've done is dealing with lists. Is there a way to write a nXm matrix?
2021-12-27 07:19:35 +0100 <EvanR> reflection has a weird side effect... if you have a top level thing that is like foo :: Given MyConfig => Other -> Stuff, then :t foo won't work in ghci. Though foo will still work "if used" correctly
2021-12-27 07:19:59 +0100 <EvanR> no instance for Given MyConfig
2021-12-27 07:20:13 +0100Morrow(~quassel@bzq-110-168-31-106.red.bezeqint.net)
2021-12-27 07:20:20 +0100 <dsal> You could do something along the lines of AoC, but suggest particular things for the solution.
2021-12-27 07:20:41 +0100 <EvanR> otherwise, I've done a few of those. Also available in libraries
2021-12-27 07:20:58 +0100 <dsal> otherwise: There are arrays with arbitrary indexes and Data.Vector. And probably countless actual matrix libraries.
2021-12-27 07:22:51 +0100 <dsal> I end up using Maps a lot.
2021-12-27 07:23:57 +0100 <EvanR> specifically "n x m" matrix is kind of calling for the n and m to be in the type, which you can do
2021-12-27 07:24:28 +0100 <EvanR> and would be great
2021-12-27 07:25:03 +0100 <EvanR> the blog "graphical linear algebra" makes you really want those in the type
2021-12-27 07:26:12 +0100 <EvanR> if you're doing graphics maybe you can get away assuming everything is 4x4
2021-12-27 07:26:32 +0100notzmv(~zmv@user/notzmv)
2021-12-27 07:28:41 +0100farzad(~farzad@5.121.10.41)
2021-12-27 07:30:36 +0100 <otherwise> let split (x:xs) = if length xs < 7 then [] else (take 7 (x:xs)): split (tail xs) in split [1..21]
2021-12-27 07:30:41 +0100 <otherwise> > let split (x:xs) = if length xs < 7 then [] else (take 7 (x:xs)): split (tail xs) in split [1..21]
2021-12-27 07:30:43 +0100 <lambdabot> [[1,2,3,4,5,6,7],[3,4,5,6,7,8,9],[5,6,7,8,9,10,11],[7,8,9,10,11,12,13],[9,10...
2021-12-27 07:31:01 +0100 <otherwise> oh its too big..
2021-12-27 07:31:27 +0100 <otherwise> > let split (x:xs) = if length xs < 3 then [] else (take 3 (x:xs)): split (tail xs) in split [1..15]
2021-12-27 07:31:29 +0100 <lambdabot> [[1,2,3],[3,4,5],[5,6,7],[7,8,9],[9,10,11],[11,12,13]]
2021-12-27 07:31:45 +0100 <EvanR> chunksOf 3
2021-12-27 07:32:00 +0100 <xerox> > takeWhile (not . null) . unfoldr (Just . splitAt 4) $ [1..10]
2021-12-27 07:32:02 +0100 <lambdabot> [[1,2,3,4],[5,6,7,8],[9,10]]
2021-12-27 07:32:27 +0100 <EvanR> > chunksOf 3 [1..15]
2021-12-27 07:32:28 +0100 <lambdabot> [[1,2,3],[4,5,6],[7,8,9],[10,11,12],[13,14,15]]
2021-12-27 07:33:18 +0100 <otherwise> chunksOf is not in my ghci
2021-12-27 07:33:34 +0100 <EvanR> I think it's from a package... called split
2021-12-27 07:33:49 +0100 <EvanR> that is apparently loaded
2021-12-27 07:38:38 +0100 <dsal> @hoogle chunksOf
2021-12-27 07:38:39 +0100 <lambdabot> Data.Sequence chunksOf :: Int -> Seq a -> Seq (Seq a)
2021-12-27 07:38:39 +0100 <lambdabot> Data.Sequence.Internal chunksOf :: Int -> Seq a -> Seq (Seq a)
2021-12-27 07:38:39 +0100 <lambdabot> Data.Text chunksOf :: Int -> Text -> [Text]
2021-12-27 07:41:14 +0100 <EvanR> Data.List.Split
2021-12-27 07:46:44 +0100shapr(~user@pool-100-36-247-68.washdc.fios.verizon.net) (Ping timeout: 268 seconds)
2021-12-27 07:47:45 +0100 <otherwise> > let mapIn = map (1 -) (head (split[1..15]))
2021-12-27 07:47:47 +0100 <lambdabot> <no location info>: error:
2021-12-27 07:47:47 +0100 <lambdabot> not an expression: ‘let mapIn = map (1 -) (head (split[1..15]))’
2021-12-27 07:48:06 +0100 <EvanR> in what
2021-12-27 07:48:54 +0100 <otherwise> I dont think it would work anyway cause I forgot lambdabot doesnt know what I defined as split
2021-12-27 07:49:09 +0100 <EvanR> yeah
2021-12-27 07:52:17 +0100slowButPresent(~slowButPr@user/slowbutpresent) (Quit: leaving)
2021-12-27 07:53:07 +0100fef(~thedawn@user/thedawn)
2021-12-27 07:56:47 +0100fizbin(~fizbin@c-73-33-197-160.hsd1.nj.comcast.net)
2021-12-27 07:58:13 +0100 <otherwise> is it offensive that Haskell is not on codeacademy?
2021-12-27 08:00:10 +0100falafel(~falafel@2603-8000-d800-688c-9993-a5d6-8c3d-400e.res6.spectrum.com)
2021-12-27 08:01:02 +0100fizbin(~fizbin@c-73-33-197-160.hsd1.nj.comcast.net) (Ping timeout: 240 seconds)
2021-12-27 08:02:16 +0100 <EvanR> They have two columns of 7 languages. Making 3 columns of 5 languages may be too much to ask for their web design
2021-12-27 08:02:28 +0100 <dsal> That looks like a vocational thing.
2021-12-27 08:02:37 +0100 <dsal> Not learning to be better, but learning to make money.
2021-12-27 08:02:54 +0100 <EvanR> code academy is who's making the money here
2021-12-27 08:03:43 +0100 <otherwise> is haskell for poor people?
2021-12-27 08:04:08 +0100 <EvanR> it's for anyone who is interested
2021-12-27 08:06:15 +0100 <dsal> Haskell is for making blockchains and NFTs.
2021-12-27 08:06:37 +0100 <dsal> It's just generally a great language that makes programming fun and easy.
2021-12-27 08:07:01 +0100 <dsal> It's used in a few different industries, but it's best when it's not industry specific.
2021-12-27 08:07:04 +0100 <EvanR> I just appointed dsal VP of sales and marketing for haskell
2021-12-27 08:07:16 +0100 <dsal> haha
2021-12-27 08:07:52 +0100 <EvanR> You just have a really good attitude and strong reality distortion field
2021-12-27 08:08:03 +0100 <dsal> Sounds right.
2021-12-27 08:08:09 +0100 <otherwise> Cardano is using haskell, apparently for blockchain tech
2021-12-27 08:08:16 +0100 <dsal> I've had a lot of large codebases, though.
2021-12-27 08:08:23 +0100 <otherwise> alluded by VP of sales
2021-12-27 08:08:49 +0100 <dsal> otherwise: Yeah. A friend of mine into that stuff tried to pull me in a while back for smart contracts and stuff. It was horrifying. I told him they needed people with Haskell experience. Now it's a brain drain as they suck in all the people with haskell experience.
2021-12-27 08:09:07 +0100 <dsal> Getting a job doing Haskell that's *not* blockchain related is a bit harder now.
2021-12-27 08:10:36 +0100 <dsal> Of course, that's assuming you *want* that kind of job. Knowing Haskell makes you a better programmer in general. I did a lot of non-Haskell professional programming while doing all my personal projects in Haskell.
2021-12-27 08:11:42 +0100merijn(~merijn@83-160-49-249.ip.xs4all.nl)
2021-12-27 08:12:01 +0100enikar(~enikar@user/enikar)
2021-12-27 08:12:48 +0100 <otherwise> interesting
2021-12-27 08:13:19 +0100 <EvanR> knowing C is also good. Also not on code academy
2021-12-27 08:13:31 +0100 <EvanR> also hard to get a job in
2021-12-27 08:13:55 +0100 <dibblego> it's way easier
2021-12-27 08:14:25 +0100 <dibblego> There were about 5 jobs using Haskell in the world. It was easy to make 10 more. Today, don't even have to make them.
2021-12-27 08:16:10 +0100Jing(~hedgehog@2604:a840:3::1067)
2021-12-27 08:19:11 +0100nattiestnate(~nate@182.3.37.200) (Ping timeout: 256 seconds)
2021-12-27 08:19:36 +0100lavaman(~lavaman@98.38.249.169)
2021-12-27 08:21:44 +0100nattiestnate(~nate@182.3.37.200)
2021-12-27 08:21:48 +0100yauhsien(~yauhsien@61-231-42-148.dynamic-ip.hinet.net)
2021-12-27 08:24:21 +0100lavaman(~lavaman@98.38.249.169) (Ping timeout: 268 seconds)
2021-12-27 08:24:59 +0100vglfr(~vglfr@88.155.28.231)
2021-12-27 08:26:33 +0100yauhsien(~yauhsien@61-231-42-148.dynamic-ip.hinet.net) (Ping timeout: 256 seconds)
2021-12-27 08:37:12 +0100 <otherwise> trying to implement last, using foldl1, with an edge condition that returns [] if an infinite list is input.... https://paste.tomsmeding.com/xmlgcXmF
2021-12-27 08:37:45 +0100 <dibblego> you won't
2021-12-27 08:38:05 +0100 <otherwise> not possible?
2021-12-27 08:38:14 +0100 <dibblego> you going to count to infinity to check?
2021-12-27 08:38:23 +0100 <otherwise> if i have to
2021-12-27 08:38:29 +0100 <dibblego> ok, I'll wait
2021-12-27 08:38:33 +0100 <otherwise> done
2021-12-27 08:39:09 +0100 <dibblego> I've gone to a party while I wait, but if I were a type-checker instead...
2021-12-27 08:39:35 +0100vglfr(~vglfr@88.155.28.231) (Quit: Quit)
2021-12-27 08:39:47 +0100vglfr(~vglfr@88.155.28.231)
2021-12-27 08:41:07 +0100jackson99(~bc8147f2@cerf.good1.com) (Quit: CGI:IRC (Ping timeout))
2021-12-27 08:42:13 +0100jinsun(~quassel@user/jinsun) (Ping timeout: 240 seconds)
2021-12-27 08:43:21 +0100jinsun(~quassel@user/jinsun)
2021-12-27 08:45:53 +0100merijn(~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 250 seconds)
2021-12-27 08:47:47 +0100nattiestnate(~nate@182.3.37.200) (Ping timeout: 268 seconds)
2021-12-27 08:50:06 +0100nicbk(~nicbk@user/nicbk)
2021-12-27 08:50:09 +0100 <nicbk> #openbsd
2021-12-27 08:51:02 +0100coolnickname(uid531864@user/coolnickname)
2021-12-27 08:57:14 +0100qrpnxz(abc4f95c31@user/qrpnxz) (Disconnected: Replaced by new connection)
2021-12-27 08:57:14 +0100qrpnxz(abc4f95c31@user/qrpnxz)
2021-12-27 09:00:00 +0100qrpnxz(abc4f95c31@user/qrpnxz) (Disconnected: Replaced by new connection)
2021-12-27 09:00:00 +0100qrpnxz(abc4f95c31@user/qrpnxz)
2021-12-27 09:00:31 +0100qrpnxz(abc4f95c31@user/qrpnxz) (Disconnected: closed)
2021-12-27 09:00:54 +0100qrpnxz(abc4f95c31@user/qrpnxz)
2021-12-27 09:01:32 +0100vysn(~vysn@user/vysn)
2021-12-27 09:02:36 +0100burnsidesLlama(~burnsides@dhcp168-010.wadham.ox.ac.uk)
2021-12-27 09:03:05 +0100phma(phma@2001:5b0:211c:1148:9e4d:7400:733a:b6f1) (Read error: Connection reset by peer)
2021-12-27 09:03:17 +0100falafel(~falafel@2603-8000-d800-688c-9993-a5d6-8c3d-400e.res6.spectrum.com) (Ping timeout: 240 seconds)
2021-12-27 09:03:32 +0100phma(phma@2001:5b0:211c:1148:bf01:ab8f:863f:c9a8)
2021-12-27 09:06:05 +0100falafel(~falafel@2603-8000-d800-688c-9993-a5d6-8c3d-400e.res6.spectrum.com)
2021-12-27 09:11:38 +0100tromp(~textual@dhcp-077-249-230-040.chello.nl)
2021-12-27 09:13:17 +0100talismanick(~talismani@2601:644:8500:8350::94b)
2021-12-27 09:13:51 +0100 <talismanick> Is there a resource for "minimal Nix" (just enough needed to manage Haskell packages), or do I need to learn it in full?
2021-12-27 09:17:53 +0100Sgeo(~Sgeo@user/sgeo) (Read error: Connection reset by peer)
2021-12-27 09:24:44 +0100nattiestnate(~nate@182.3.37.200)
2021-12-27 09:24:57 +0100n3rdy1(~n3rdy1@2601:281:c780:a510:84eb:b2e:7b61:4002) (Ping timeout: 240 seconds)
2021-12-27 09:27:22 +0100_ht(~quassel@82-169-194-8.biz.kpn.net)
2021-12-27 09:31:50 +0100farzad(~farzad@5.121.10.41) (Remote host closed the connection)
2021-12-27 09:32:01 +0100Nate[m]12(~m52957mat@2001:470:69fc:105::1:591a)
2021-12-27 09:33:22 +0100snake(~snake@user/snake) (Quit: Quitting)
2021-12-27 09:34:17 +0100farzad(~farzad@5.121.10.41)
2021-12-27 09:36:31 +0100synthmeat(~synthmeat@user/synthmeat)
2021-12-27 09:38:57 +0100zmt00(~zmt00@user/zmt00) (Ping timeout: 240 seconds)
2021-12-27 09:41:53 +0100jespada(~jespada@87.74.33.157)
2021-12-27 09:42:01 +0100max22-(~maxime@2a01cb0883359800761b1c69d9198b7f.ipv6.abo.wanadoo.fr)
2021-12-27 09:42:55 +0100snake(~snake@user/snake)
2021-12-27 09:43:21 +0100gehmehgeh(~user@user/gehmehgeh)
2021-12-27 09:48:16 +0100altern(~Sergii@altern.corbina.com.ua)
2021-12-27 09:50:06 +0100 <altern> Hi! How to properly convert the list of files into a recursive record in Haskell? https://stackoverflow.com/questions/70490845/how-to-properly-convert-the-list-of-files-into-a-recu…
2021-12-27 09:50:15 +0100econo(uid147250@user/econo) (Quit: Connection closed for inactivity)
2021-12-27 09:57:18 +0100acidjnk(~acidjnk@p200300d0c7271e72b97741cdfe77e27f.dip0.t-ipconnect.de)
2021-12-27 09:57:51 +0100tzh(~tzh@c-24-21-73-154.hsd1.wa.comcast.net) (Quit: zzz)
2021-12-27 10:00:20 +0100 <int-e> https://nitter.fdn.fr/gone_things/status/1475245068994838528#m
2021-12-27 10:00:21 +0100burnsidesLlama(~burnsides@dhcp168-010.wadham.ox.ac.uk) (Remote host closed the connection)
2021-12-27 10:08:32 +0100dcoutts_(~duncan@71.78.6.51.dyn.plus.net)
2021-12-27 10:17:42 +0100geekosaur(~geekosaur@xmonad/geekosaur) (Killed (NickServ (GHOST command used by allbery_b)))
2021-12-27 10:17:42 +0100allbery_b(~geekosaur@xmonad/geekosaur)
2021-12-27 10:17:45 +0100allbery_bgeekosaur
2021-12-27 10:22:18 +0100nattiestnate(~nate@182.3.37.200) (Read error: Connection reset by peer)
2021-12-27 10:23:00 +0100nattiestnate(~nate@182.2.164.13)
2021-12-27 10:27:17 +0100eggplantade(~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) (Remote host closed the connection)
2021-12-27 10:27:22 +0100KvL(~KvL@user/KvL)
2021-12-27 10:32:15 +0100snake(~snake@user/snake) (Quit: Leaving)
2021-12-27 10:35:11 +0100stiell(~stiell@gateway/tor-sasl/stiell) (Remote host closed the connection)
2021-12-27 10:35:35 +0100stiell(~stiell@gateway/tor-sasl/stiell)
2021-12-27 10:36:51 +0100Gurkenglas(~Gurkengla@dslb-002-203-144-204.002.203.pools.vodafone-ip.de)
2021-12-27 10:39:57 +0100falafel(~falafel@2603-8000-d800-688c-9993-a5d6-8c3d-400e.res6.spectrum.com) (Ping timeout: 240 seconds)
2021-12-27 10:42:06 +0100burnsidesLlama(~burnsides@dhcp168-010.wadham.ox.ac.uk)
2021-12-27 10:42:12 +0100merijn(~merijn@83-160-49-249.ip.xs4all.nl)
2021-12-27 10:45:13 +0100 <otherwise> I'm trying Day 1 at adventofCode, and the provided input is a large list of numbers, stacked in a vertical collumn, but haskell cannot read it as a list. I managed to add a comma at the end of each number in vim, but I can't get vim to delete the line break in front of every number at one, to make all numbers be on the same line. Any tips?
2021-12-27 10:46:18 +0100 <Rembane> :i lines
2021-12-27 10:46:22 +0100 <Rembane> Meh
2021-12-27 10:46:23 +0100 <Rembane> :t lines
2021-12-27 10:46:24 +0100 <lambdabot> String -> [String]
2021-12-27 10:46:32 +0100burnsidesLlama(~burnsides@dhcp168-010.wadham.ox.ac.uk) (Ping timeout: 240 seconds)
2021-12-27 10:46:36 +0100 <Rembane> > lines "1\n2\n3\n4"
2021-12-27 10:46:37 +0100 <lambdabot> ["1","2","3","4"]
2021-12-27 10:46:54 +0100nicbk(~nicbk@user/nicbk) (Ping timeout: 276 seconds)
2021-12-27 10:57:17 +0100Erutuon(~Erutuon@user/erutuon) (Ping timeout: 256 seconds)
2021-12-27 10:58:59 +0100nattiestnate(~nate@182.2.164.13) (Ping timeout: 256 seconds)
2021-12-27 11:02:33 +0100coot(~coot@89-64-85-93.dynamic.chello.pl)
2021-12-27 11:16:02 +0100merijn(~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 240 seconds)
2021-12-27 11:19:46 +0100jinsun__(~quassel@user/jinsun)
2021-12-27 11:20:30 +0100burnsidesLlama(~burnsides@dhcp168-010.wadham.ox.ac.uk)
2021-12-27 11:21:37 +0100jinsun(~quassel@user/jinsun) (Ping timeout: 240 seconds)
2021-12-27 11:23:46 +0100Lord_of_Life_(~Lord@user/lord-of-life/x-2819915)
2021-12-27 11:25:02 +0100Lord_of_Life(~Lord@user/lord-of-life/x-2819915) (Ping timeout: 268 seconds)
2021-12-27 11:25:04 +0100Lord_of_Life_Lord_of_Life
2021-12-27 11:26:14 +0100burnsidesLlama(~burnsides@dhcp168-010.wadham.ox.ac.uk) (Ping timeout: 260 seconds)
2021-12-27 11:26:41 +0100Rum(~bourbon@user/rum)
2021-12-27 11:27:39 +0100eggplantade(~Eggplanta@2600:1700:bef1:5e10:b417:46a:3118:ab81)
2021-12-27 11:31:57 +0100eggplantade(~Eggplanta@2600:1700:bef1:5e10:b417:46a:3118:ab81) (Ping timeout: 240 seconds)
2021-12-27 11:32:57 +0100mvk(~mvk@2607:fea8:5cdd:f000::917a) (Ping timeout: 240 seconds)
2021-12-27 11:40:27 +0100rito_(~rito_gh@45.112.243.219)
2021-12-27 11:42:37 +0100Akiva(~Akiva@user/Akiva) (Ping timeout: 256 seconds)
2021-12-27 11:43:48 +0100yauhsien(~yauhsien@61-231-42-148.dynamic-ip.hinet.net)
2021-12-27 11:46:17 +0100nattiestnate(~nate@182.2.164.13)
2021-12-27 11:47:02 +0100SummerSonw(~The_viole@203.77.49.232) (Ping timeout: 240 seconds)
2021-12-27 11:47:39 +0100jonathanx(~jonathan@h-178-174-176-109.A357.priv.bahnhof.se) (Remote host closed the connection)
2021-12-27 11:48:17 +0100yauhsien(~yauhsien@61-231-42-148.dynamic-ip.hinet.net) (Ping timeout: 256 seconds)
2021-12-27 11:48:44 +0100shriekingnoise(~shrieking@186.137.144.80) (Quit: Quit)
2021-12-27 11:51:03 +0100nattiestnate(~nate@182.2.164.13) (Read error: Connection reset by peer)
2021-12-27 11:53:10 +0100nattiestnate(~nate@114.122.107.243)
2021-12-27 11:53:59 +0100jonathanx(~jonathan@h-178-174-176-109.A357.priv.bahnhof.se)
2021-12-27 11:58:45 +0100SummerSonw(~The_viole@203.77.49.232)
2021-12-27 11:58:58 +0100fizbin(~fizbin@c-73-33-197-160.hsd1.nj.comcast.net)
2021-12-27 12:01:19 +0100Gurkenglas(~Gurkengla@dslb-002-203-144-204.002.203.pools.vodafone-ip.de) (Ping timeout: 256 seconds)
2021-12-27 12:03:53 +0100fizbin(~fizbin@c-73-33-197-160.hsd1.nj.comcast.net) (Ping timeout: 268 seconds)
2021-12-27 12:06:17 +0100acode(~acode@151.65.31.181)
2021-12-27 12:06:53 +0100nattiestnate(~nate@114.122.107.243) (Quit: WeeChat 3.4)
2021-12-27 12:07:13 +0100nattiestnate(~nate@114.122.105.227)
2021-12-27 12:09:27 +0100max22-(~maxime@2a01cb0883359800761b1c69d9198b7f.ipv6.abo.wanadoo.fr) (Ping timeout: 268 seconds)
2021-12-27 12:10:12 +0100 <acode> Following up on a discussion from a few days ago, has anyone figured out what happened to the learn you a haskell website?
2021-12-27 12:11:49 +0100 <geekosaur> still only conjecture, no definitive answer
2021-12-27 12:12:06 +0100Midjak(~Midjak@may53-1-78-226-116-92.fbx.proxad.net)
2021-12-27 12:12:22 +0100 <iphy> https://github.com/iphydf/hs-cimple/blob/fix/src/Language/Cimple/Pretty.hs#L498-L502 how would one express this using recursion-strategies or data-fix?
2021-12-27 12:12:59 +0100 <acode> I see. Hopefully it'll be back
2021-12-27 12:13:17 +0100vglfr(~vglfr@88.155.28.231) (Ping timeout: 252 seconds)
2021-12-27 12:17:09 +0100acidjnk(~acidjnk@p200300d0c7271e72b97741cdfe77e27f.dip0.t-ipconnect.de) (Ping timeout: 250 seconds)
2021-12-27 12:17:28 +0100mvk(~mvk@2607:fea8:5cdd:f000::917a)
2021-12-27 12:20:37 +0100jinsun__(~quassel@user/jinsun) (Ping timeout: 240 seconds)
2021-12-27 12:21:16 +0100lavaman(~lavaman@98.38.249.169)
2021-12-27 12:22:20 +0100jinsun(~quassel@user/jinsun)
2021-12-27 12:22:31 +0100stiell(~stiell@gateway/tor-sasl/stiell) (Remote host closed the connection)
2021-12-27 12:22:37 +0100noddy(~user@user/noddy) (Quit: WeeChat 3.3)
2021-12-27 12:22:52 +0100stiell(~stiell@gateway/tor-sasl/stiell)
2021-12-27 12:23:37 +0100KvL(~KvL@user/KvL) (Ping timeout: 240 seconds)
2021-12-27 12:23:40 +0100AlexNoo_AlexNoo
2021-12-27 12:25:12 +0100noddy(~user@user/noddy)
2021-12-27 12:25:17 +0100lavaman(~lavaman@98.38.249.169) (Ping timeout: 240 seconds)
2021-12-27 12:27:02 +0100SummerSonw(~The_viole@203.77.49.232) (Ping timeout: 252 seconds)
2021-12-27 12:27:48 +0100KvL(~KvL@user/KvL)
2021-12-27 12:29:07 +0100KvL(~KvL@user/KvL) (Client Quit)
2021-12-27 12:30:53 +0100jinsun(~quassel@user/jinsun) (Quit: https://quassel-irc.org - Chat comfortably. Anywhere.)
2021-12-27 12:32:51 +0100max22-(~maxime@2a01cb08833598007287589cfe6298ed.ipv6.abo.wanadoo.fr)
2021-12-27 12:34:50 +0100KvL(~KvL@user/KvL)
2021-12-27 12:35:37 +0100mvk(~mvk@2607:fea8:5cdd:f000::917a) (Ping timeout: 240 seconds)
2021-12-27 12:37:19 +0100web-50(~web-50@185.202.32.108) (Quit: Client closed)
2021-12-27 12:38:23 +0100max22-(~maxime@2a01cb08833598007287589cfe6298ed.ipv6.abo.wanadoo.fr) (Ping timeout: 250 seconds)
2021-12-27 12:40:36 +0100__monty__(~toonn@user/toonn)
2021-12-27 12:40:45 +0100wroathe(~wroathe@c-68-54-25-135.hsd1.mn.comcast.net)
2021-12-27 12:40:45 +0100wroathe(~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Changing host)
2021-12-27 12:40:45 +0100wroathe(~wroathe@user/wroathe)
2021-12-27 12:43:13 +0100pretty_dumm_guy(trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655)
2021-12-27 12:43:42 +0100zer0bitz(~zer0bitz@185.112.82.230)
2021-12-27 12:45:32 +0100wroathe(~wroathe@user/wroathe) (Ping timeout: 240 seconds)
2021-12-27 12:46:48 +0100vglfr(~vglfr@88.155.28.231)
2021-12-27 12:48:09 +0100coot(~coot@89-64-85-93.dynamic.chello.pl) (Quit: coot)
2021-12-27 12:48:56 +0100coot(~coot@89-64-85-93.dynamic.chello.pl)
2021-12-27 12:53:14 +0100mikoto-chan(~mikoto-ch@esm-84-240-99-143.netplaza.fi) (Ping timeout: 268 seconds)
2021-12-27 12:54:54 +0100 <otherwise> do you use vim (in terminal) or something else for writing haskell programs?
2021-12-27 12:55:17 +0100 <iphy> I use vim in terminal
2021-12-27 12:55:20 +0100 <xerox> me too
2021-12-27 12:55:37 +0100 <iphy> vscode is pretty good these days though
2021-12-27 12:56:32 +0100ProfSimm(~ProfSimm@87.227.196.109)
2021-12-27 12:57:08 +0100SummerSonw(~The_viole@203.77.49.232)
2021-12-27 12:57:12 +0100burnsidesLlama(~burnsides@dhcp168-010.wadham.ox.ac.uk)
2021-12-27 12:57:49 +0100 <otherwise> I dont have a lot of experience, but I use vim in terminal, although it is a little daunting cause there are so many quick commands. I see other people in videos now and again and they are blazing through their code jumping around like a rabbit... kind of a steep learning curve to get proficient
2021-12-27 12:59:18 +0100Vquses Emacs in X11
2021-12-27 13:00:53 +0100 <Vq> I don't use that many fancy features for Haskell development though.
2021-12-27 13:01:25 +0100burnsidesLlama(~burnsides@dhcp168-010.wadham.ox.ac.uk) (Ping timeout: 240 seconds)
2021-12-27 13:01:40 +0100 <Vq> Just plain haskell-mode + stylish-haskell on save.
2021-12-27 13:04:10 +0100KvL(~KvL@user/KvL) (Quit: KvL)
2021-12-27 13:05:12 +0100CiaoSen(~Jura@p200300c957347b002a3a4dfffe84dbd5.dip0.t-ipconnect.de)
2021-12-27 13:05:50 +0100 <otherwise> hmm Emacs eh
2021-12-27 13:07:33 +0100Gurkenglas(~Gurkengla@dslb-002-203-144-204.002.203.pools.vodafone-ip.de)
2021-12-27 13:08:55 +0100 <otherwise> https://paste.tomsmeding.com/0qa2v50r
2021-12-27 13:09:48 +0100 <otherwise> interested in feedback, especially regarding the stupid long list. There must be a better way to deal with it.
2021-12-27 13:10:20 +0100 <otherwise> from AoT, day 1 part 1
2021-12-27 13:12:16 +0100 <otherwise> maybe the long list can live in a separate .hs file, and the main.hs file calls the list file? I haven't done anything like that yet...
2021-12-27 13:12:50 +0100merijn(~merijn@83-160-49-249.ip.xs4all.nl)
2021-12-27 13:13:51 +0100Vajb(~Vajb@hag-jnsbng11-58c3a8-176.dhcp.inet.fi) (Read error: Connection reset by peer)
2021-12-27 13:17:16 +0100Vajb(~Vajb@hag-jnsbng11-58c3a8-176.dhcp.inet.fi)
2021-12-27 13:18:21 +0100Rum(~bourbon@user/rum) (Quit: WeeChat 3.4)
2021-12-27 13:21:52 +0100 <alfonsox> write input to .txt file
2021-12-27 13:23:04 +0100 <alfonsox> use "getContents" to read input file.
2021-12-27 13:25:06 +0100neceve(~quassel@2.26.93.228)
2021-12-27 13:27:26 +0100 <otherwise> alfonsox i'll give that a try now
2021-12-27 13:30:02 +0100eggplantade(~Eggplanta@2600:1700:bef1:5e10:b417:46a:3118:ab81)
2021-12-27 13:30:59 +0100DNH(~DNH@2a02:8108:1100:16d8:6043:aa58:f99b:e1b)
2021-12-27 13:31:01 +0100m1dnight(~christoph@christophe.dev) (Quit: WeeChat 3.1)
2021-12-27 13:31:38 +0100m1dnight(~christoph@christophe.dev)
2021-12-27 13:33:00 +0100max22-(~maxime@2a01cb0883359800eadee1731c9704da.ipv6.abo.wanadoo.fr)
2021-12-27 13:34:17 +0100eggplantade(~Eggplanta@2600:1700:bef1:5e10:b417:46a:3118:ab81) (Ping timeout: 240 seconds)
2021-12-27 13:35:47 +0100Flow(~none@gentoo/developer/flow) (Ping timeout: 250 seconds)
2021-12-27 13:36:17 +0100 <xerox> :t \x y f g h -> do { x' <- f x; y' <- g y; h x' y' }
2021-12-27 13:36:18 +0100 <lambdabot> Monad m => t1 -> t2 -> (t1 -> m t3) -> (t2 -> m t4) -> (t3 -> t4 -> m b) -> m b
2021-12-27 13:36:24 +0100 <xerox> :t \x y f g h -> do { h <*> f x <*> g y }
2021-12-27 13:36:25 +0100 <lambdabot> Applicative f => t1 -> t2 -> (t1 -> f a1) -> (t2 -> f a2) -> f (a1 -> a2 -> b) -> f b
2021-12-27 13:36:44 +0100tromp(~textual@dhcp-077-249-230-040.chello.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
2021-12-27 13:36:52 +0100 <xerox> is there a way to use the second style but achieving the first's objective, with a h :: _ -> _ -> m r
2021-12-27 13:38:38 +0100 <tomsmeding> :t \x y f g h -> do { h <$> f x <*> g y
2021-12-27 13:38:39 +0100 <lambdabot> error:
2021-12-27 13:38:39 +0100 <lambdabot> parse error (possibly incorrect indentation or mismatched brackets)
2021-12-27 13:38:42 +0100 <tomsmeding> :t \x y f g h -> do { h <$> f x <*> g y }
2021-12-27 13:38:43 +0100 <lambdabot> Applicative f => t1 -> t2 -> (t1 -> f a1) -> (t2 -> f a2) -> (a1 -> a2 -> b) -> f b
2021-12-27 13:39:09 +0100 <alfonsox> otherwise - readFile would be better. Check Files and Stream section on https://web.archive.org/web/20211102000749/http://learnyouahaskell.com/input-and-output#files-and-…
2021-12-27 13:40:06 +0100 <tomsmeding> :t \x y f g h -> join (h <$> f x <*> g y)
2021-12-27 13:40:07 +0100 <lambdabot> Monad m => t1 -> t2 -> (t1 -> m a1) -> (t2 -> m a2) -> (a1 -> a2 -> m a3) -> m a3
2021-12-27 13:41:12 +0100Flow(~none@gentoo/developer/flow)
2021-12-27 13:41:22 +0100 <xerox> tomsmeding: alright :)
2021-12-27 13:41:42 +0100[itchyjunk](~itchyjunk@user/itchyjunk/x-7353470)
2021-12-27 13:41:46 +0100 <tomsmeding> feels like join (fmap f x) should be simplifiable
2021-12-27 13:42:23 +0100 <xerox> @pl \f x -> join (fmap f x)
2021-12-27 13:42:23 +0100 <tomsmeding> oh but it's not, it's join (fmap f x <*> y)
2021-12-27 13:42:23 +0100 <lambdabot> (=<<)
2021-12-27 13:42:39 +0100 <xerox> @pl \f x y -> join (fmap f x <*> y)
2021-12-27 13:42:39 +0100 <lambdabot> (((join .) . (<*>)) .) . fmap
2021-12-27 13:42:45 +0100 <xerox> 🤮
2021-12-27 13:42:46 +0100 <tomsmeding> useful :p
2021-12-27 13:43:12 +0100 <xerox> :t liftM2
2021-12-27 13:43:13 +0100 <lambdabot> Monad m => (a1 -> a2 -> r) -> m a1 -> m a2 -> m r
2021-12-27 13:43:16 +0100 <xerox> this also is just pure
2021-12-27 13:43:56 +0100 <tomsmeding> not quite, right?
2021-12-27 13:44:06 +0100 <xerox> yeah I mean just r not m r
2021-12-27 13:44:17 +0100 <tomsmeding> liftM2 = \f x y -> f <$> x <*> y, if the Applicative and Monad instances agree
2021-12-27 13:44:30 +0100 <xerox> :t (>=>)
2021-12-27 13:44:31 +0100 <lambdabot> Monad m => (a -> m b) -> (b -> m c) -> a -> m c
2021-12-27 13:44:33 +0100 <tomsmeding> so your thing is also join (liftM2 h (f x) (g y))
2021-12-27 13:44:44 +0100 <xerox> yup
2021-12-27 13:46:25 +0100 <tomsmeding> :t \x y f g h -> f x >>= (g y >=> h)
2021-12-27 13:46:26 +0100 <lambdabot> Monad m => t1 -> t2 -> (t1 -> m a) -> (t2 -> a -> m b1) -> (b1 -> m b2) -> m b2
2021-12-27 13:46:32 +0100 <tomsmeding> not sure that makes it better :p
2021-12-27 13:46:47 +0100merijn(~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 252 seconds)
2021-12-27 13:47:07 +0100 <tomsmeding> oh it's wrong
2021-12-27 13:48:13 +0100 <tomsmeding> >=> doesn't help
2021-12-27 13:48:45 +0100tomsmedingremembers using liftM always in my early haskell adventures; then I discovered it's just fmap
2021-12-27 13:48:56 +0100machinedgod(~machinedg@24.105.81.50)
2021-12-27 13:49:06 +0100 <hpc> eventually you discover it's just (<$>) :D
2021-12-27 13:49:36 +0100 <tomsmeding> :p yeah I did that at roughly the same time
2021-12-27 13:50:01 +0100 <tomsmeding> 'input <- map (map read) . lines <$> getContents' for the win
2021-12-27 13:50:09 +0100 <tomsmeding> with some 'words' in between
2021-12-27 13:50:24 +0100 <hpc> using straight "fmap" reminds me too much of common lisp, somehow
2021-12-27 13:50:40 +0100 <hpc> where you have to worry about what's a real function, what's a macro, everything is annoyingly prefix, etc etc
2021-12-27 13:50:55 +0100 <hpc> not really sure why that's where my mind goes, but i always prefer (<$>) because of it
2021-12-27 13:50:58 +0100ksqsf(~user@134.209.106.31)
2021-12-27 13:51:23 +0100NinjaTrappeur(~ninja@user/ninjatrappeur)
2021-12-27 13:51:37 +0100jespada(~jespada@87.74.33.157) (Ping timeout: 240 seconds)
2021-12-27 13:51:55 +0100 <otherwise> alfonsox thanks I'll look at that. I think I'm actually just going to continue with LYAH instead, because that is the next section for me anyway :) After that I'll come back and see if I can replace the gargantuan list into a separate txt file that I can call into an [Int}.
2021-12-27 13:52:44 +0100jespada(~jespada@87.74.33.157)
2021-12-27 13:52:53 +0100 <hpc> speaking of lyah, the website is still down :(
2021-12-27 13:53:21 +0100 <otherwise> my PDF is still going strong
2021-12-27 13:53:52 +0100Gurkenglas(~Gurkengla@dslb-002-203-144-204.002.203.pools.vodafone-ip.de) (Remote host closed the connection)
2021-12-27 13:54:10 +0100Gurkenglas(~Gurkengla@dslb-002-203-144-204.002.203.pools.vodafone-ip.de)
2021-12-27 13:54:25 +0100 <otherwise> Yeah I was in the thick of the contents when it just shut down. Hopefully it is a sign of some upgrades to come! (probably not)
2021-12-27 13:54:39 +0100coot(~coot@89-64-85-93.dynamic.chello.pl) (Ping timeout: 256 seconds)
2021-12-27 13:55:08 +0100tromp(~textual@dhcp-077-249-230-040.chello.nl)
2021-12-27 13:58:46 +0100 <[itchyjunk]> I have a non haskell question, are there FP languages without GC?
2021-12-27 13:59:12 +0100 <hpc> hmm, lyah is cc by-nc-sa, maybe it can be rehosted on haskell.org?
2021-12-27 13:59:25 +0100SummerSonw(~The_viole@203.77.49.232) (Ping timeout: 240 seconds)
2021-12-27 13:59:37 +0100Tuplanolla(~Tuplanoll@91-159-69-236.elisa-laajakaista.fi) (Ping timeout: 240 seconds)
2021-12-27 13:59:55 +0100fizbin(~fizbin@c-73-33-197-160.hsd1.nj.comcast.net)
2021-12-27 14:04:23 +0100fizbin(~fizbin@c-73-33-197-160.hsd1.nj.comcast.net) (Ping timeout: 252 seconds)
2021-12-27 14:07:36 +0100SummerSonw(~The_viole@203.77.49.232)
2021-12-27 14:09:26 +0100acidjnk(~acidjnk@p200300d0c7271e72b97741cdfe77e27f.dip0.t-ipconnect.de)
2021-12-27 14:09:58 +0100 <ksqsf> [itchyjunk]: iirc ATS seems to claim to support GC-free FP, but I haven't tried it yet
2021-12-27 14:11:21 +0100 <[itchyjunk]> Apparently I don't know what GC is. Some say scoped memory management implied GC others say it doesn't. ;_;
2021-12-27 14:11:40 +0100 <[exa]> [itchyjunk]: there is a naive super-inefficient implementation of the GCless FP (all copies are deep copies, including the copies of closures/thunks)
2021-12-27 14:12:13 +0100kupi(uid212005@id-212005.hampstead.irccloud.com)
2021-12-27 14:12:57 +0100 <[exa]> [itchyjunk]: most of the MM magic is about dodging by sharing some of the structures while being able to guess when it's safe to free the structure, usually by just tracking everything with a GC
2021-12-27 14:13:58 +0100eyJhb(~eyJhb@user/eyjhb) (WeeChat 3.3)
2021-12-27 14:14:14 +0100 <ksqsf> [itchyjunk]: btw what is 'scoped memory management'? do you mean C++-style RAII?
2021-12-27 14:14:57 +0100dsrt^(~dsrt@207.5.54.6) (Remote host closed the connection)
2021-12-27 14:15:06 +0100 <[itchyjunk]> It was in response to "does C has GC?" it was "no, it only has scoped memory management"
2021-12-27 14:17:24 +0100 <[itchyjunk]> I had never though of it but it does make sense that you'ed be making deep copies as an alternative
2021-12-27 14:17:33 +0100 <[exa]> [itchyjunk]: if you allocate all resources in strictly nested regions, the memory management can be easily done with a stack-like structure, which is precisely what C does for "simple" variables
2021-12-27 14:17:50 +0100 <[itchyjunk]> ah
2021-12-27 14:17:51 +0100 <[exa]> (malloc() and free() doesn't count here, these are kinda "external" to the core language)
2021-12-27 14:19:44 +0100 <[exa]> C++ RAII kinda follows the same principle even with allocations of these "external" structures using malloc/new free/delete, the stack only retains a "handle", usually some kind of a wrapped pointer that can deallocate itself
2021-12-27 14:19:49 +0100NinjaTrappeur(~ninja@user/ninjatrappeur) (Quit: WeeChat 3.3)
2021-12-27 14:20:13 +0100Tuplanolla(~Tuplanoll@91-159-68-119.elisa-laajakaista.fi)
2021-12-27 14:20:49 +0100 <[exa]> with the usual FP that involves lots of functions being passed around, the ability to hide super-complex things in thunks makes the stack-style memory management quite useless
2021-12-27 14:22:18 +0100 <[exa]> there are ways to statically analyze lots of FP and compile it down to stack code, but these usually aren't general and it's technically much easier to go the dynamic way with garbage collection
2021-12-27 14:22:53 +0100 <tomsmeding> [itchyjunk]: https://github.com/carp-lang/Carp/ exists; kind of functional
2021-12-27 14:27:35 +0100 <tomsmeding> [itchyjunk]: if you have a strict language without mutation (haskell is neither :p), reference counting is sufficient. Some count RC as a GC, and it kind of is, but it's impact on program execution is of a very different nature than stop-the-world GCs
2021-12-27 14:28:00 +0100 <tomsmeding> iirc python has RC, but including some kind of cycle detection because (due to mutation) you can create cyclic data structures in python
2021-12-27 14:28:34 +0100 <[itchyjunk]> Oh, is this why there is a hard limit for number of recursion in py?
2021-12-27 14:28:56 +0100 <tomsmeding> no that's just control stack size, unrelated :p
2021-12-27 14:29:02 +0100 <[itchyjunk]> hmmmmm
2021-12-27 14:29:03 +0100 <[itchyjunk]> lol
2021-12-27 14:29:07 +0100 <tomsmeding> (if you're talking about function recursion)
2021-12-27 14:29:12 +0100 <acode> What does RC stand for?
2021-12-27 14:29:16 +0100 <tomsmeding> reference counting
2021-12-27 14:29:41 +0100 <acode> Thanks, time to do some googling
2021-12-27 14:30:13 +0100farzad(~farzad@5.121.10.41) (Quit: Leaving)
2021-12-27 14:30:37 +0100 <[itchyjunk]> if you have no pointer pointing to a datastructure in memory, you can free that part of memory - i think it's something like that
2021-12-27 14:30:39 +0100[itchyjunk]googles too
2021-12-27 14:30:56 +0100 <tomsmeding> RC (without additional cycle detection) fails in a lazy language or in a language with mutable elements (haskell's IORef is enough, even apart from laziness), because RC cannot handle reference cycles; the members of the cycle would keep each other alive
2021-12-27 14:31:51 +0100 <tomsmeding> [itchyjunk]: yeah, the idea is that every time you throw away a reference to an object, you decrement a counter on the object; if that decrement yields zero, deallocate the object (and recursively handle the references contained therein, if any)
2021-12-27 14:32:47 +0100 <tomsmeding> with RC, "GC time", and when "GC" runs, is fully deterministic if your program is deterministic
2021-12-27 14:33:25 +0100 <[itchyjunk]> hmm
2021-12-27 14:33:40 +0100 <tomsmeding> but some stop-the-world GC algorithms have the advantage that they only need to iterate over _live_ memory at each world pause; in contrast, RC needs to perform action on every object that becomes dead (and additionally needs to keep all those reference counters up to date)
2021-12-27 14:33:59 +0100 <tomsmeding> so RC is not necessarily more efficient in terms of throughput than stop-the-world mark-and-sweep
2021-12-27 14:34:03 +0100 <ksqsf> RC usually has lower latency but also has lower throughput; I always prefer traing GCs
2021-12-27 14:34:10 +0100 <ksqsf> tracing *
2021-12-27 14:34:11 +0100 <tomsmeding> but it may be more predictable
2021-12-27 14:34:19 +0100 <tomsmeding> what ksqsf says
2021-12-27 14:35:02 +0100 <[itchyjunk]> hmm why is it lower throughput?
2021-12-27 14:35:03 +0100 <tomsmeding> ksqsf: tracing GC is what stop-the-world that traverses only live memory, right? i.e. what GHC has
2021-12-27 14:35:13 +0100 <tomsmeding> [itchyjunk]: in the end, in total, RC needs to do more work
2021-12-27 14:35:22 +0100 <tomsmeding> because of all the reference count updating
2021-12-27 14:35:27 +0100 <[itchyjunk]> ah
2021-12-27 14:35:53 +0100 <tomsmeding> and if you time a GC pause right, when the working memory is low, that GC only has to traverse the live memory (i.e. a small set if you're lucky), freeing all the dead memory in O(1)
2021-12-27 14:36:33 +0100 <tomsmeding> so, tracing is O(live memory), while RC is O(reference mutations + dead memory), I _think_ (may be missing stuff)
2021-12-27 14:37:30 +0100coot(~coot@89-64-85-93.dynamic.chello.pl)
2021-12-27 14:48:56 +0100jinsun(~quassel@user/jinsun)
2021-12-27 14:49:27 +0100 <int-e> tomsmeding: There's a fun tweak for RC where for every decrease of a reference count, you free a constant number of items from a to-free list (and maybe put new ones on the list), which has real-time properties if each memory item has a bounded number of pointers... essentially you free stuff lazily, smoothing what would otherwise be an amortized cost.
2021-12-27 14:51:01 +0100max22-(~maxime@2a01cb0883359800eadee1731c9704da.ipv6.abo.wanadoo.fr) (Ping timeout: 268 seconds)
2021-12-27 14:55:23 +0100 <tomsmeding> int-e: oh that's neat, indeed relies on objects having a bounded number of references
2021-12-27 14:55:33 +0100 <tomsmeding> s/having/containing/, less ambiguous
2021-12-27 14:59:24 +0100tito(tito@tilde.team)
2021-12-27 15:01:50 +0100drewr(~drew@user/drewr)
2021-12-27 15:07:58 +0100jesser[m](~jessermat@2001:470:69fc:105::d5ae)
2021-12-27 15:10:00 +0100sagax(~sagax_nb@user/sagax) (Quit: Konversation terminated!)
2021-12-27 15:11:43 +0100ksqsf(~user@134.209.106.31) (Remote host closed the connection)
2021-12-27 15:12:04 +0100ksqsf(~user@2001:da8:d800:611:dc11:dfaa:95da:b93d)
2021-12-27 15:12:04 +0100bollu(uid233390@id-233390.helmsley.irccloud.com)
2021-12-27 15:12:14 +0100sagax(~sagax_nb@user/sagax)
2021-12-27 15:12:37 +0100Feuermagier(~Feuermagi@user/feuermagier) (Remote host closed the connection)
2021-12-27 15:12:59 +0100xsperry(~xs@user/xsperry) (Remote host closed the connection)
2021-12-27 15:17:27 +0100fef(~thedawn@user/thedawn) (Quit: Leaving)
2021-12-27 15:17:50 +0100ksqsf(~user@2001:da8:d800:611:dc11:dfaa:95da:b93d) (Read error: Connection reset by peer)
2021-12-27 15:18:09 +0100ksqsf(~user@134.209.106.31)
2021-12-27 15:19:48 +0100sleblanc(~sleblanc@user/sleblanc) (Quit: Leaving)
2021-12-27 15:20:10 +0100totte(~totte@h-82-196-112-155.A166.priv.bahnhof.se)
2021-12-27 15:22:14 +0100yauhsien(~yauhsien@61-231-42-148.dynamic-ip.hinet.net)
2021-12-27 15:24:00 +0100waleee(~waleee@2001:9b0:21d:fc00:398f:b003:b90d:acf4)
2021-12-27 15:25:09 +0100Vajb(~Vajb@hag-jnsbng11-58c3a8-176.dhcp.inet.fi) (Read error: Connection reset by peer)
2021-12-27 15:25:17 +0100drewr(~drew@user/drewr) (Ping timeout: 240 seconds)
2021-12-27 15:26:43 +0100yauhsien(~yauhsien@61-231-42-148.dynamic-ip.hinet.net) (Ping timeout: 250 seconds)
2021-12-27 15:31:49 +0100 <iphy> is there a better way to write this? https://github.com/iphydf/hs-cimple/blob/fix/src/Language/Cimple/Diagnostics.hs#L43-L140
2021-12-27 15:33:41 +0100drewr(~drew@user/drewr)
2021-12-27 15:40:39 +0100max22-(~maxime@2a01cb0883359800b3fa5d9958932079.ipv6.abo.wanadoo.fr)
2021-12-27 15:42:02 +0100wroathe(~wroathe@c-68-54-25-135.hsd1.mn.comcast.net)
2021-12-27 15:42:02 +0100wroathe(~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Changing host)
2021-12-27 15:42:02 +0100wroathe(~wroathe@user/wroathe)
2021-12-27 15:43:27 +0100merijn(~merijn@83-160-49-249.ip.xs4all.nl)
2021-12-27 15:44:57 +0100drewr(~drew@user/drewr) (Ping timeout: 240 seconds)
2021-12-27 15:46:39 +0100coot(~coot@89-64-85-93.dynamic.chello.pl) ()
2021-12-27 15:47:07 +0100kaph(~kaph@net-2-38-107-19.cust.vodafonedsl.it) (Ping timeout: 268 seconds)
2021-12-27 15:47:28 +0100 <pavonia> iphy: I used to use uniplate in such situations. Not sure if this is still a thing today
2021-12-27 15:47:59 +0100 <iphy> Neil Mitchell 2006-2020
2021-12-27 15:48:02 +0100 <iphy> looks like yes
2021-12-27 15:48:18 +0100 <iphy> Uploaded by NeilMitchell at 2020-11-07T19:53:43Z
2021-12-27 15:48:45 +0100 <pavonia> Yeah, but GHC has greater support for generics today. Maybe there's somthing better already built-in
2021-12-27 15:49:27 +0100coot(~coot@2a02:a310:e03f:8500:5cc8:47c:8ec0:b827)
2021-12-27 15:50:15 +0100altern(~Sergii@altern.corbina.com.ua) (Ping timeout: 256 seconds)
2021-12-27 15:50:28 +0100Sgeo(~Sgeo@user/sgeo)
2021-12-27 15:50:46 +0100coot(~coot@2a02:a310:e03f:8500:5cc8:47c:8ec0:b827) (Remote host closed the connection)
2021-12-27 15:51:07 +0100coot(~coot@2a02:a310:e03f:8500:5cc8:47c:8ec0:b827)
2021-12-27 15:51:16 +0100ProfSimm(~ProfSimm@87.227.196.109) (Remote host closed the connection)
2021-12-27 15:52:00 +0100zincy(~zincy@2a00:23c8:970c:4801:bdb9:8c5f:3085:2807)
2021-12-27 15:52:04 +0100 <tomsmeding> fairly sure you can do that with generics, but not sure how easy that is compared to just giving up and writing this out :p
2021-12-27 15:55:27 +0100shriekingnoise(~shrieking@186.137.144.80)
2021-12-27 15:59:17 +0100DNH(~DNH@2a02:8108:1100:16d8:6043:aa58:f99b:e1b) (Quit: My MacBook has gone to sleep. ZZZzzz…)
2021-12-27 16:01:17 +0100Vajb(~Vajb@hag-jnsbng11-58c3a8-176.dhcp.inet.fi)
2021-12-27 16:04:26 +0100coot(~coot@2a02:a310:e03f:8500:5cc8:47c:8ec0:b827) (Remote host closed the connection)
2021-12-27 16:05:28 +0100coot(~coot@2a02:a310:e03f:8500:5cc8:47c:8ec0:b827)
2021-12-27 16:05:55 +0100DNH(~DNH@2a02:8108:1100:16d8:6043:aa58:f99b:e1b)
2021-12-27 16:06:15 +0100ksqsf(~user@134.209.106.31) (Ping timeout: 268 seconds)
2021-12-27 16:07:06 +0100Feuermagier(~Feuermagi@user/feuermagier)
2021-12-27 16:12:26 +0100SummerSonw(~The_viole@203.77.49.232) (Quit: Leaving)
2021-12-27 16:13:34 +0100drewr(~drew@user/drewr)
2021-12-27 16:14:22 +0100 <tomsmeding> pavonia: bit of a mess but it does seem to work https://paste.tomsmeding.com/bIGQNN1J
2021-12-27 16:15:17 +0100 <tomsmeding> ah but it only works if 'lexeme' does not have [] as its outer type
2021-12-27 16:15:22 +0100 <tomsmeding> because of the hacky overlapping instances
2021-12-27 16:16:47 +0100 <tomsmeding> but you should be able to prevent that from going wrong by fmapping a newtype wrapper over the lexeme
2021-12-27 16:17:39 +0100neurocyte0132889(~neurocyte@IP-092119008132.dynamic.medianet-world.de)
2021-12-27 16:17:39 +0100neurocyte0132889(~neurocyte@IP-092119008132.dynamic.medianet-world.de) (Changing host)
2021-12-27 16:17:39 +0100neurocyte0132889(~neurocyte@user/neurocyte)
2021-12-27 16:17:54 +0100merijn(~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 260 seconds)
2021-12-27 16:18:14 +0100fef(~thedawn@user/thedawn)
2021-12-27 16:18:17 +0100CiaoSen(~Jura@p200300c957347b002a3a4dfffe84dbd5.dip0.t-ipconnect.de) (Ping timeout: 240 seconds)
2021-12-27 16:18:29 +0100 <pavonia> iphy: ^
2021-12-27 16:18:31 +0100 <tomsmeding> oh it does work!
2021-12-27 16:18:42 +0100 <tomsmeding> I just forgot to update the type ascription in 'main' :)
2021-12-27 16:20:17 +0100 <tomsmeding> concats' :: NodeF a [a] -> [a] ; concats' = concats
2021-12-27 16:20:20 +0100 <tomsmeding> easier
2021-12-27 16:20:43 +0100fef(~thedawn@user/thedawn) (Remote host closed the connection)
2021-12-27 16:20:47 +0100 <tomsmeding> presumably uniplate makes stuff easier, but never worked with that :P
2021-12-27 16:21:08 +0100fef(~thedawn@user/thedawn)
2021-12-27 16:21:29 +0100n3rdy1(~n3rdy1@2601:281:c780:a510:f129:8ed3:b1ff:82ed)
2021-12-27 16:22:59 +0100lavaman(~lavaman@98.38.249.169)
2021-12-27 16:26:17 +0100 <otherwise> ... that seems like a lot of code to print ['a'..'g']
2021-12-27 16:26:57 +0100wroathe(~wroathe@user/wroathe) (Ping timeout: 240 seconds)
2021-12-27 16:27:42 +0100lavaman(~lavaman@98.38.249.169) (Ping timeout: 260 seconds)
2021-12-27 16:28:57 +0100drewr(~drew@user/drewr) (Ping timeout: 240 seconds)
2021-12-27 16:31:46 +0100eggplantade(~Eggplanta@2600:1700:bef1:5e10:b417:46a:3118:ab81)
2021-12-27 16:32:01 +0100ksqsf(~user@134.209.106.31)
2021-12-27 16:33:04 +0100 <tomsmeding> yes
2021-12-27 16:33:20 +0100 <tomsmeding> but it works for any value of 'Char', and also if you add more constructors to the data type ;)
2021-12-27 16:33:57 +0100drewr(~drew@user/drewr)
2021-12-27 16:35:57 +0100eggplantade(~Eggplanta@2600:1700:bef1:5e10:b417:46a:3118:ab81) (Ping timeout: 240 seconds)
2021-12-27 16:36:37 +0100ksqsf(~user@134.209.106.31) (Ping timeout: 240 seconds)
2021-12-27 16:38:40 +0100burnsidesLlama(~burnsides@dhcp168-010.wadham.ox.ac.uk)
2021-12-27 16:39:22 +0100drewr(~drew@user/drewr) (Ping timeout: 260 seconds)
2021-12-27 16:39:57 +0100slowButPresent(~slowButPr@user/slowbutpresent)
2021-12-27 16:40:37 +0100MoC(~moc@user/moc)
2021-12-27 16:42:57 +0100burnsidesLlama(~burnsides@dhcp168-010.wadham.ox.ac.uk) (Ping timeout: 256 seconds)
2021-12-27 16:44:01 +0100wroathe(~wroathe@c-68-54-25-135.hsd1.mn.comcast.net)
2021-12-27 16:44:01 +0100wroathe(~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Changing host)
2021-12-27 16:44:01 +0100wroathe(~wroathe@user/wroathe)
2021-12-27 16:44:26 +0100bontaq(~user@static-108-32-49-96.pitbpa.fios.verizon.net)
2021-12-27 16:44:27 +0100 <int-e> tomsmeding: Oh you went down that path too... I ended up with https://paste.tomsmeding.com/6mEKw6Ur
2021-12-27 16:45:40 +0100merijn(~merijn@83-160-49-249.ip.xs4all.nl)
2021-12-27 16:45:46 +0100 <int-e> (so ugly)
2021-12-27 16:45:51 +0100 <tomsmeding> int-e: why INCOHERENT and not OVERLAPPING? :p
2021-12-27 16:46:08 +0100 <int-e> because they *are* incoherent
2021-12-27 16:46:21 +0100 <iphy> tomsmeding: nice
2021-12-27 16:46:36 +0100acidjnk(~acidjnk@p200300d0c7271e72b97741cdfe77e27f.dip0.t-ipconnect.de) (Ping timeout: 245 seconds)
2021-12-27 16:46:42 +0100 <iphy> lexeme is always something that's not a list
2021-12-27 16:46:46 +0100 <int-e> if u = v, Fold2_Base u v u and Fold2_Base u v v produce different behavior
2021-12-27 16:46:49 +0100 <iphy> (e.g. it's never String)
2021-12-27 16:47:31 +0100 <int-e> tomsmeding: it's a side effect of dealing with two types rather than one
2021-12-27 16:48:11 +0100 <int-e> And I don't like it. But it seems to work. Make of that what you will...
2021-12-27 16:48:50 +0100wroathe(~wroathe@user/wroathe) (Ping timeout: 252 seconds)
2021-12-27 16:49:11 +0100rekahsoft(~rekahsoft@cpe0008a20f982f-cm64777d666260.cpe.net.cable.rogers.com)
2021-12-27 16:49:34 +0100 <int-e> This means, btw, that manually inlining `fold2` is dangerous.
2021-12-27 16:49:46 +0100ksqsf(~user@134.209.106.31)
2021-12-27 16:53:34 +0100DNH(~DNH@2a02:8108:1100:16d8:6043:aa58:f99b:e1b) (Quit: My MacBook has gone to sleep. ZZZzzz…)
2021-12-27 16:53:55 +0100 <tomsmeding> int-e: interesting
2021-12-27 16:54:57 +0100ksqsf(~user@134.209.106.31) (Ping timeout: 268 seconds)
2021-12-27 16:55:16 +0100 <tomsmeding> oh yeah I didn't add support for Maybe
2021-12-27 16:56:05 +0100 <tomsmeding> but that's easy, the types show the way :D
2021-12-27 16:56:54 +0100 <int-e> tomsmeding: the [a] and (Maybe a) instances are merely OVERLAPPING though
2021-12-27 16:57:01 +0100 <tomsmeding> yeah
2021-12-27 16:59:52 +0100 <mjrosenb> is there a definition of what makes instances incoherent or overlapping? I've never ran into either before.
2021-12-27 17:00:08 +0100ilkecan[m](~ilkecanma@2001:470:69fc:105::1:79b) (Quit: You have been kicked for being idle)
2021-12-27 17:00:43 +0100fef(~thedawn@user/thedawn) (Remote host closed the connection)
2021-12-27 17:01:00 +0100qrpnxz(abc4f95c31@user/qrpnxz) (Disconnected: Replaced by new connection)
2021-12-27 17:01:01 +0100qrpnxz(abc4f95c31@user/qrpnxz)
2021-12-27 17:01:02 +0100 <tomsmeding> mjrosenb: https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/exts/instances.html#overlapping-in…
2021-12-27 17:01:04 +0100fef(~thedawn@user/thedawn)
2021-12-27 17:01:24 +0100 <tomsmeding> if you want all the details :p
2021-12-27 17:01:36 +0100qrpnxz(abc4f95c31@user/qrpnxz) (Disconnected: Replaced by new connection)
2021-12-27 17:01:36 +0100qrpnxz(abc4f95c31@user/qrpnxz)
2021-12-27 17:01:37 +0100xff0x(~xff0x@2001:1a81:53c9:5600:a4b4:57a2:f2c0:c793) (Ping timeout: 240 seconds)
2021-12-27 17:02:35 +0100xff0x(~xff0x@2001:1a81:53c9:5600:a16a:4242:194d:2615)
2021-12-27 17:08:01 +0100ksqsf(~user@134.209.106.31)
2021-12-27 17:08:15 +0100 <iphy> tomsmeding: https://github.com/iphydf/hs-cimple/blob/fix/src/Language/Cimple/Diagnostics.hs#L44
2021-12-27 17:08:24 +0100 <iphy> https://github.com/iphydf/hs-cimple/blob/fix/src/Language/Cimple/Flatten.hs
2021-12-27 17:09:09 +0100mario_(~mario@31.147.205.13)
2021-12-27 17:09:51 +0100 <tomsmeding> iphy: might not need a separate instance for Maybe [a], right?
2021-12-27 17:10:10 +0100 <tomsmeding> the Maybe and OVERLAPPABLE [] instances should cover that
2021-12-27 17:10:11 +0100 <tomsmeding> but nice!
2021-12-27 17:10:27 +0100 <tomsmeding> _might_ want some comments :p
2021-12-27 17:10:29 +0100 <iphy> https://www.irccloud.com/pastebin/rsBXUD6Q/
2021-12-27 17:10:34 +0100 <iphy> tomsmeding: yeah, soon :)
2021-12-27 17:10:57 +0100 <tomsmeding> oh heh
2021-12-27 17:11:26 +0100 <tomsmeding> replace the 'instance GenConcatsFlatten (Maybe a) a' with 'instance GenConcatsFlatten b a => GenConcatsFlatten (Maybe b) a'
2021-12-27 17:11:38 +0100 <tomsmeding> perhaps also OVERLAPPABLE
2021-12-27 17:11:47 +0100 <tomsmeding> (in case 'a' is ever Maybe something)
2021-12-27 17:12:30 +0100 <iphy> yeah
2021-12-27 17:12:39 +0100 <iphy> it's never Maybe something, so this works
2021-12-27 17:12:41 +0100 <tomsmeding> I mean, this also works
2021-12-27 17:12:51 +0100ksqsf(~user@134.209.106.31) (Ping timeout: 245 seconds)
2021-12-27 17:13:12 +0100 <iphy> https://github.com/iphydf/hs-cimple/blob/fix/src/Language/Cimple/Flatten.hs#L46
2021-12-27 17:14:45 +0100 <tomsmeding> yay
2021-12-27 17:14:56 +0100Guest|88(~Guest|88@79.171.77.255)
2021-12-27 17:15:19 +0100Guest|88(~Guest|88@79.171.77.255) (Client Quit)
2021-12-27 17:17:10 +0100xff0x(~xff0x@2001:1a81:53c9:5600:a16a:4242:194d:2615) (Ping timeout: 268 seconds)
2021-12-27 17:17:46 +0100xff0x(~xff0x@2001:1a81:53c9:5600:de59:5c41:aa07:4876)
2021-12-27 17:25:31 +0100ksqsf(~user@134.209.106.31)
2021-12-27 17:27:46 +0100wroathe(~wroathe@c-68-54-25-135.hsd1.mn.comcast.net)
2021-12-27 17:27:46 +0100wroathe(~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Changing host)
2021-12-27 17:27:46 +0100wroathe(~wroathe@user/wroathe)
2021-12-27 17:27:56 +0100 <iphy> lexeme will always be either Lexeme String, Lexeme Text, or some other atomic type (never List or Maybe or another functor)
2021-12-27 17:30:33 +0100zincy(~zincy@2a00:23c8:970c:4801:bdb9:8c5f:3085:2807) (Remote host closed the connection)
2021-12-27 17:30:44 +0100 <geekosaur> String is a list
2021-12-27 17:30:47 +0100 <geekosaur> not atomic
2021-12-27 17:31:10 +0100ksqsf(~user@134.209.106.31) (Ping timeout: 260 seconds)
2021-12-27 17:31:56 +0100 <tomsmeding> geekosaur: Lexeme String != String
2021-12-27 17:32:36 +0100 <tomsmeding> iphy: still you can fmap a newtype wrapper over the thing to ensure that the root type is always that newtype wrapper, so that it can never go wrong even if someone does something stupid later on
2021-12-27 17:32:56 +0100 <tomsmeding> not sure if 'fmap' is the right thing here though
2021-12-27 17:33:02 +0100wroathe(~wroathe@user/wroathe) (Ping timeout: 260 seconds)
2021-12-27 17:33:29 +0100spoofer(~spoofer@64.185.111.205) ()
2021-12-27 17:34:00 +0100xsperry(~xs@user/xsperry)
2021-12-27 17:34:53 +0100gioyik(~gioyik@gateway/tor-sasl/gioyik)
2021-12-27 17:43:20 +0100ksqsf(~user@134.209.106.31)
2021-12-27 17:43:40 +0100burnsidesLlama(~burnsides@dhcp168-010.wadham.ox.ac.uk)
2021-12-27 17:44:34 +0100zmt00(~zmt00@user/zmt00)
2021-12-27 17:46:42 +0100pavonia(~user@user/siracusa) (Quit: Bye!)
2021-12-27 17:47:06 +0100mc47(~mc47@xmonad/TheMC47)
2021-12-27 17:47:57 +0100ksqsf(~user@134.209.106.31) (Ping timeout: 240 seconds)
2021-12-27 17:49:28 +0100wroathe(~wroathe@c-68-54-25-135.hsd1.mn.comcast.net)
2021-12-27 17:49:28 +0100wroathe(~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Changing host)
2021-12-27 17:49:28 +0100wroathe(~wroathe@user/wroathe)
2021-12-27 17:49:43 +0100MoC(~moc@user/moc) (Quit: Konversation terminated!)
2021-12-27 17:50:09 +0100Bartol_(~Bartol@user/Bartol)
2021-12-27 17:51:19 +0100zincy(~zincy@host86-151-99-97.range86-151.btcentralplus.com)
2021-12-27 17:51:27 +0100waleee(~waleee@2001:9b0:21d:fc00:398f:b003:b90d:acf4) (Ping timeout: 250 seconds)
2021-12-27 17:51:41 +0100merijn(~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 268 seconds)
2021-12-27 17:52:53 +0100justsomeguy(~justsomeg@user/justsomeguy)
2021-12-27 17:53:37 +0100wroathe(~wroathe@user/wroathe) (Ping timeout: 240 seconds)
2021-12-27 17:53:50 +0100[itchyjunk](~itchyjunk@user/itchyjunk/x-7353470) (Remote host closed the connection)
2021-12-27 17:55:20 +0100 <mjrosenb> should emacs with hls be able to compile things without invoking haskell-compile?
2021-12-27 17:59:53 +0100nattiestnate(~nate@114.122.105.227) (Read error: Connection reset by peer)
2021-12-27 18:01:32 +0100xb0o2(~xb0o2@user/xb0o2)
2021-12-27 18:03:43 +0100haask(~askham@92.234.0.237)
2021-12-27 18:04:16 +0100merijn(~merijn@83-160-49-249.ip.xs4all.nl)
2021-12-27 18:07:20 +0100zincy(~zincy@host86-151-99-97.range86-151.btcentralplus.com) (Remote host closed the connection)
2021-12-27 18:07:25 +0100 <haask> In this year of 2021, is it possible to take an existing Stack project (say, a REPL for some language) and compile it to run clientside in a browser? I understand the options to be GHCJS (no Stack support), Haste (no TemplateHaskell support), Reflex - any other option I'm overlooking before I go down the rewrite-for-GHCJS rabbithole?
2021-12-27 18:07:33 +0100zincy(~zincy@2a00:23c8:970c:4801:bdb9:8c5f:3085:2807)
2021-12-27 18:07:54 +0100Sgeo(~Sgeo@user/sgeo) (Read error: Connection reset by peer)
2021-12-27 18:08:58 +0100nattiestnate(~nate@114.122.105.227)
2021-12-27 18:09:02 +0100merijn(~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 240 seconds)
2021-12-27 18:09:47 +0100ubert(~Thunderbi@p548c8cd6.dip0.t-ipconnect.de) (Remote host closed the connection)
2021-12-27 18:10:22 +0100mario_spaceseller
2021-12-27 18:11:38 +0100mbuf(~Shakthi@122.178.203.86) (Quit: Leaving)
2021-12-27 18:13:02 +0100 <iphy> tomsmeding: this is good enough now :) Flatten is used internally only
2021-12-27 18:13:19 +0100 <iphy> thanks btw
2021-12-27 18:13:40 +0100 <tomsmeding> iphy: <3
2021-12-27 18:16:37 +0100alfonsox(~quassel@103.92.42.104) (Quit: https://quassel-irc.org - Chat comfortably. Anywhere.)
2021-12-27 18:17:34 +0100Lord_of_Life(~Lord@user/lord-of-life/x-2819915) (Excess Flood)
2021-12-27 18:18:28 +0100Lord_of_Life(~Lord@user/lord-of-life/x-2819915)
2021-12-27 18:24:28 +0100zincy(~zincy@2a00:23c8:970c:4801:bdb9:8c5f:3085:2807) (Remote host closed the connection)
2021-12-27 18:25:08 +0100DNH(~DNH@2a02:8108:1100:16d8:6043:aa58:f99b:e1b)
2021-12-27 18:28:53 +0100zincy(~zincy@2a00:23c8:970c:4801:bdb9:8c5f:3085:2807)
2021-12-27 18:31:24 +0100shapr(~user@pool-100-36-247-68.washdc.fios.verizon.net)
2021-12-27 18:32:17 +0100coot(~coot@2a02:a310:e03f:8500:5cc8:47c:8ec0:b827) (Quit: coot)
2021-12-27 18:32:59 +0100coot(~coot@89-64-85-93.dynamic.chello.pl)
2021-12-27 18:33:34 +0100eggplantade(~Eggplanta@2600:1700:bef1:5e10:b417:46a:3118:ab81)
2021-12-27 18:34:50 +0100zincy(~zincy@2a00:23c8:970c:4801:bdb9:8c5f:3085:2807) (Remote host closed the connection)
2021-12-27 18:35:33 +0100mc47(~mc47@xmonad/TheMC47) (Remote host closed the connection)
2021-12-27 18:35:56 +0100zincy(~zincy@2a00:23c8:970c:4801:bdb9:8c5f:3085:2807)
2021-12-27 18:37:32 +0100ksqsf(~user@134.209.106.31)
2021-12-27 18:38:17 +0100eggplantade(~Eggplanta@2600:1700:bef1:5e10:b417:46a:3118:ab81) (Ping timeout: 252 seconds)
2021-12-27 18:40:24 +0100turlando(~turlando@user/turlando) (Ping timeout: 268 seconds)
2021-12-27 18:40:36 +0100turlando(~turlando@93-42-250-112.ip89.fastwebnet.it)
2021-12-27 18:40:36 +0100turlando(~turlando@93-42-250-112.ip89.fastwebnet.it) (Changing host)
2021-12-27 18:40:36 +0100turlando(~turlando@user/turlando)
2021-12-27 18:41:24 +0100Sgeo(~Sgeo@user/sgeo)
2021-12-27 18:42:08 +0100ksqsf(~user@134.209.106.31) (Ping timeout: 252 seconds)
2021-12-27 18:46:55 +0100justsomeguy(~justsomeg@user/justsomeguy) (Quit: WeeChat 3.3)
2021-12-27 18:52:05 +0100xb0o2(~xb0o2@user/xb0o2) (Quit: Client closed)
2021-12-27 18:53:41 +0100bontaq(~user@static-108-32-49-96.pitbpa.fios.verizon.net) (Ping timeout: 252 seconds)
2021-12-27 18:53:41 +0100waleee(~waleee@2001:9b0:21d:fc00:398f:b003:b90d:acf4)
2021-12-27 18:54:51 +0100albet70(~xxx@2400:8902::f03c:92ff:fe60:98d8) (Remote host closed the connection)
2021-12-27 18:56:07 +0100tzh(~tzh@c-24-21-73-154.hsd1.or.comcast.net)
2021-12-27 18:56:14 +0100 <lyxia> Can I use cabal to compile a single file that depends on packages? `cabal exec ghc` complains that I don't have a cabal.project...
2021-12-27 19:00:58 +0100albet70(~xxx@2400:8902::f03c:92ff:fe60:98d8)
2021-12-27 19:01:42 +0100 <EvanR> it's possible to use ghc with the flags for those packages
2021-12-27 19:01:59 +0100 <EvanR> but would be nice if cabal did that
2021-12-27 19:08:15 +0100nicbk(~nicbk@user/nicbk)
2021-12-27 19:08:16 +0100CiaoSen(~Jura@p200300c957347b002a3a4dfffe84dbd5.dip0.t-ipconnect.de)
2021-12-27 19:12:00 +0100kupi(uid212005@id-212005.hampstead.irccloud.com) (Quit: Connection closed for inactivity)
2021-12-27 19:13:22 +0100Erutuon(~Erutuon@user/erutuon)
2021-12-27 19:14:00 +0100 <sm> I think stack scripts can compile themselves (to an executable you can reuse) but cabal scripts can't
2021-12-27 19:15:52 +0100lavaman(~lavaman@98.38.249.169)
2021-12-27 19:17:58 +0100nattiestnate(~nate@114.122.105.227) (Quit: WeeChat 3.4)
2021-12-27 19:18:17 +0100nattiestnate(~nate@114.122.106.227)
2021-12-27 19:18:52 +0100albet70(~xxx@2400:8902::f03c:92ff:fe60:98d8) (Remote host closed the connection)
2021-12-27 19:19:01 +0100xff0x(~xff0x@2001:1a81:53c9:5600:de59:5c41:aa07:4876) (Ping timeout: 240 seconds)
2021-12-27 19:21:56 +0100econo(uid147250@user/econo)
2021-12-27 19:24:37 +0100ksqsf(~user@134.209.106.31)
2021-12-27 19:24:58 +0100albet70(~xxx@2400:8902::f03c:92ff:fe60:98d8)
2021-12-27 19:25:31 +0100DNH(~DNH@2a02:8108:1100:16d8:6043:aa58:f99b:e1b) (Quit: My MacBook has gone to sleep. ZZZzzz…)
2021-12-27 19:26:05 +0100Sgeo_(~Sgeo@user/sgeo)
2021-12-27 19:28:59 +0100Sgeo(~Sgeo@user/sgeo) (Ping timeout: 256 seconds)
2021-12-27 19:29:31 +0100ksqsf(~user@134.209.106.31) (Ping timeout: 245 seconds)
2021-12-27 19:31:37 +0100DNH(~DNH@2a02:8108:1100:16d8:6043:aa58:f99b:e1b)
2021-12-27 19:34:38 +0100 <iphy> I've refactored my pretty printer to use foldFix. I needed to communicate information from a deeper layer upwards, so I made it part of the accumulator. is that the right way to do this? https://github.com/iphydf/hs-cimple/blob/fix/src/Language/Cimple/Pretty.hs#L28
2021-12-27 19:34:42 +0100gioyik(~gioyik@gateway/tor-sasl/gioyik) (Ping timeout: 276 seconds)
2021-12-27 19:41:16 +0100spaceseller(~mario@31.147.205.13) (Quit: Leaving)
2021-12-27 19:41:17 +0100xff0x(~xff0x@2001:1a81:53c9:5600:de59:5c41:aa07:4876)
2021-12-27 19:42:05 +0100 <EvanR> oh man you can go nuts with pretty printing by mapping each item to nested boxes, each of which carries format info and color!
2021-12-27 19:42:32 +0100 <EvanR> to be interpreted by yet another layer of (over)engineering
2021-12-27 19:42:33 +0100Everything(~Everythin@37.115.210.35)
2021-12-27 19:42:37 +0100gioyik(~gioyik@gateway/tor-sasl/gioyik)
2021-12-27 19:43:25 +0100ksqsf(~user@134.209.106.31)
2021-12-27 19:43:53 +0100pretty_dumm_guy(trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655) (Quit: WeeChat 3.4)
2021-12-27 19:44:03 +0100 <EvanR> at least it would be monomorphic
2021-12-27 19:44:45 +0100 <monochrom> In general, rendering engines are like that. Pretty printing is just a special case.
2021-12-27 19:45:31 +0100 <monochrom> You can regain polymorphism by unifying pretty printing, polygon rendering, ray tracing, and path tracing. >:)
2021-12-27 19:47:26 +0100 <EvanR> in before someone claims that it's very important to distinguish different kinds of syntax by their material properties, mirror, plastic, rubblepile
2021-12-27 19:48:04 +0100 <monochrom> Syntax texturing \∩/
2021-12-27 19:48:10 +0100 <EvanR> (the docs for google filament are pretty cool)
2021-12-27 19:48:22 +0100tromp(~textual@dhcp-077-249-230-040.chello.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
2021-12-27 19:48:51 +0100ksqsf(~user@134.209.106.31) (Ping timeout: 268 seconds)
2021-12-27 19:49:39 +0100gioyik(~gioyik@gateway/tor-sasl/gioyik) (Ping timeout: 276 seconds)
2021-12-27 19:50:17 +0100tromp(~textual@dhcp-077-249-230-040.chello.nl)
2021-12-27 19:50:27 +0100 <zincy> How does parametric polymorphism fall short of dependent functions. Take cons :: a -> [a] -> [a]
2021-12-27 19:50:42 +0100yauhsien(~yauhsien@61-231-42-148.dynamic-ip.hinet.net)
2021-12-27 19:51:01 +0100 <zincy> Is it because you cant cons a Int onto a [Bool] ?
2021-12-27 19:51:43 +0100 <monochrom> I don't understand the question.
2021-12-27 19:51:44 +0100 <zincy> By dependent function I mean something like this in Lean
2021-12-27 19:51:46 +0100 <zincy> constant cons : Π α : Type u, α → list α → list α
2021-12-27 19:52:04 +0100 <EvanR> you can't cons an Int onto a [Bool] with dependent functions either
2021-12-27 19:52:13 +0100 <EvanR> type error
2021-12-27 19:52:20 +0100 <geekosaur> you can't write a function which can do a differrent thing depending on what a is
2021-12-27 19:52:31 +0100 <geekosaur> dependent functions can
2021-12-27 19:52:39 +0100 <zincy> Is that not what a dependent function allows you to do?
2021-12-27 19:52:49 +0100 <EvanR> not exactly like that
2021-12-27 19:52:56 +0100 <geekosaur> Haskell's cons is polymorphic but has to do the same thing regardless of a
2021-12-27 19:53:07 +0100 <monochrom> cons is a confusing example because it will turn out to be parametric even in a non-parametric language.
2021-12-27 19:53:22 +0100 <monochrom> Please choose a truly non-parametric example.
2021-12-27 19:53:55 +0100 <EvanR> that cons in lean example isn't really dependent
2021-12-27 19:54:07 +0100altern(~Sergii@altern.corbina.com.ua)
2021-12-27 19:54:32 +0100 <zincy> ugh I am asking confused questions
2021-12-27 19:54:42 +0100 <zincy> I should probably just read a book on type theory
2021-12-27 19:54:43 +0100nattiestnate(~nate@114.122.106.227) (Read error: Connection reset by peer)
2021-12-27 19:55:21 +0100gioyik(~gioyik@gateway/tor-sasl/gioyik)
2021-12-27 19:55:40 +0100 <EvanR> the overused example is a list whose type contains its length... vect
2021-12-27 19:55:59 +0100 <EvanR> then cons updates that length
2021-12-27 19:56:27 +0100 <zincy> Which makes cons in that case a dependent function right
2021-12-27 19:57:23 +0100 <monochrom> Not convinced it gets closer. "a -> V n a -> V (n+1) a" is still parametric in both a and n.
2021-12-27 19:58:10 +0100 <zincy> Whats the link between being parametric and dependent?
2021-12-27 19:58:22 +0100 <EvanR> yeah it's still polymorphic
2021-12-27 19:58:33 +0100yauhsien(~yauhsien@61-231-42-148.dynamic-ip.hinet.net) (Remote host closed the connection)
2021-12-27 19:58:35 +0100max22-(~maxime@2a01cb0883359800b3fa5d9958932079.ipv6.abo.wanadoo.fr) (Remote host closed the connection)
2021-12-27 19:58:48 +0100max22-(~maxime@2a01cb0883359800c465105b4f1dcedd.ipv6.abo.wanadoo.fr)
2021-12-27 19:59:06 +0100 <monochrom> I don't know of a link. But I know parametricity.
2021-12-27 19:59:34 +0100 <monochrom> I don't expect a link either. Links are overrated.
2021-12-27 20:00:35 +0100 <EvanR> you can't get a proper dependent type without using the name of one of the parameters later in the type after its introduced
2021-12-27 20:00:42 +0100gioyik(~gioyik@gateway/tor-sasl/gioyik) (Ping timeout: 276 seconds)
2021-12-27 20:00:56 +0100ksqsf(~user@134.209.106.31)
2021-12-27 20:00:57 +0100 <EvanR> which pi and sigma let you do
2021-12-27 20:02:12 +0100fizbin(~fizbin@c-73-33-197-160.hsd1.nj.comcast.net)
2021-12-27 20:02:21 +0100 <zincy> Yeah was just reading about pi and sigma
2021-12-27 20:02:33 +0100EvanR(~EvanR@user/evanr) (Remote host closed the connection)
2021-12-27 20:02:53 +0100EvanR(~EvanR@user/evanr)
2021-12-27 20:03:05 +0100 <EvanR> Pi (n : Int) -> (if even n then Bool else Char)
2021-12-27 20:03:25 +0100max22-(~maxime@2a01cb0883359800c465105b4f1dcedd.ipv6.abo.wanadoo.fr) (Ping timeout: 240 seconds)
2021-12-27 20:03:52 +0100 <EvanR> silly example but you can do actual cool things with it
2021-12-27 20:04:43 +0100bollu(uid233390@id-233390.helmsley.irccloud.com) (Quit: Connection closed for inactivity)
2021-12-27 20:05:35 +0100ksqsf(~user@134.209.106.31) (Ping timeout: 250 seconds)
2021-12-27 20:06:21 +0100merijn(~merijn@83-160-49-249.ip.xs4all.nl)
2021-12-27 20:06:26 +0100xb0o2(~xb0o2@user/xb0o2)
2021-12-27 20:06:39 +0100fizbin(~fizbin@c-73-33-197-160.hsd1.nj.comcast.net) (Ping timeout: 250 seconds)
2021-12-27 20:06:42 +0100 <zincy> So can I do Pi (n : int) -> (if even n then A else B)
2021-12-27 20:08:04 +0100 <EvanR> more likely Pi (n : Int) -> f n where f : Int -> Type and could do that
2021-12-27 20:09:05 +0100 <EvanR> jargon for f could be "an indexed family of types"
2021-12-27 20:09:32 +0100yauhsien(~yauhsien@61-231-42-148.dynamic-ip.hinet.net)
2021-12-27 20:09:58 +0100 <zincy> Is Type just like a type parameter?
2021-12-27 20:10:04 +0100 <EvanR> no
2021-12-27 20:10:15 +0100 <EvanR> Type is the type of types
2021-12-27 20:10:23 +0100 <EvanR> like Int : Type
2021-12-27 20:10:55 +0100 <zincy> So is this because there is no instantiation to do?
2021-12-27 20:11:14 +0100 <zincy> f 1 and f 2 can return different types
2021-12-27 20:11:22 +0100 <zincy> or have I mean
2021-12-27 20:11:23 +0100 <EvanR> if you had a parameter of type Type, passing in a type is like instanciation in haskell
2021-12-27 20:12:00 +0100 <EvanR> yes
2021-12-27 20:12:52 +0100 <EvanR> in this case f always returns a Type though
2021-12-27 20:13:05 +0100 <zincy> So is it a bit like existential types in haskell but on the value level
2021-12-27 20:14:15 +0100yauhsien(~yauhsien@61-231-42-148.dynamic-ip.hinet.net) (Ping timeout: 250 seconds)
2021-12-27 20:14:19 +0100 <zincy> returning Type from a function means the consumer of the function picks a different type for every value applied to f
2021-12-27 20:14:30 +0100 <zincy> Sort of existentially maybe
2021-12-27 20:14:42 +0100eggplantade(~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net)
2021-12-27 20:14:44 +0100 <EvanR> Sigma is how you express existential types with dependent types
2021-12-27 20:14:53 +0100 <EvanR> which also involves this Type family thing
2021-12-27 20:15:42 +0100 <zincy> So with sigma values don't determine the result type
2021-12-27 20:16:03 +0100 <EvanR> they do
2021-12-27 20:16:26 +0100gioyik(~gioyik@gateway/tor-sasl/gioyik)
2021-12-27 20:16:36 +0100 <EvanR> Sigma (n : Int, if even n then Char else Bool)
2021-12-27 20:16:50 +0100 <iphy> EvanR: yes, you can go nuts, but I also want it to be readable code
2021-12-27 20:16:56 +0100 <EvanR> the type of the snd component depends on the value of n
2021-12-27 20:17:43 +0100deadmarshal(~deadmarsh@95.38.116.71) (Ping timeout: 256 seconds)
2021-12-27 20:19:06 +0100lavaman(~lavaman@98.38.249.169) (Ping timeout: 245 seconds)
2021-12-27 20:20:31 +0100 <zincy> Ok so each value is mapped to a choice of multiple types
2021-12-27 20:22:10 +0100 <EvanR> so (0,'a') (1,False) (2,'z') (3,True) are values of that sigma type
2021-12-27 20:22:54 +0100 <EvanR> when the second component is not a boring value but evidence of some property, it gets more interesting
2021-12-27 20:23:28 +0100 <EvanR> Sigma (n : Int, Even n)
2021-12-27 20:23:58 +0100 <EvanR> has values (0,<proof term>) (2,<other proof term>) ..., but not (1, <impossible>)
2021-12-27 20:24:41 +0100eggplantade(~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) (Remote host closed the connection)
2021-12-27 20:25:23 +0100 <EvanR> Even n are all different Types so you need dependent types for this
2021-12-27 20:26:11 +0100zincy(~zincy@2a00:23c8:970c:4801:bdb9:8c5f:3085:2807) (Remote host closed the connection)
2021-12-27 20:28:31 +0100fef(~thedawn@user/thedawn) (Quit: Leaving)
2021-12-27 20:30:05 +0100zincy(~zincy@host86-151-99-97.range86-151.btcentralplus.com)
2021-12-27 20:32:03 +0100eggplantade(~Eggplanta@2600:1700:bef1:5e10:b417:46a:3118:ab81)
2021-12-27 20:32:30 +0100zincy(~zincy@host86-151-99-97.range86-151.btcentralplus.com) (Remote host closed the connection)
2021-12-27 20:35:41 +0100zincy(~zincy@2a00:23c8:970c:4801:bdb9:8c5f:3085:2807)
2021-12-27 20:37:51 +0100snake(~snake@user/snake)
2021-12-27 20:39:23 +0100merijn(~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 250 seconds)
2021-12-27 20:40:29 +0100 <zincy> Oh nice
2021-12-27 20:40:41 +0100 <zincy> EvanR: What is Even n ?
2021-12-27 20:43:10 +0100 <EvanR> a type
2021-12-27 20:43:31 +0100 <EvanR> carefully designed to represent the fact that n is even
2021-12-27 20:43:48 +0100 <EvanR> (if and only if it is)
2021-12-27 20:45:18 +0100 <EvanR> types are propositions, values are the proofs
2021-12-27 20:45:25 +0100 <EvanR> if any
2021-12-27 20:46:04 +0100max22-(~maxime@2a01cb0883359800f5f346d928347cfb.ipv6.abo.wanadoo.fr)
2021-12-27 20:46:12 +0100gioyik(~gioyik@gateway/tor-sasl/gioyik) (Ping timeout: 276 seconds)
2021-12-27 20:46:55 +0100ksqsf(~user@134.209.106.31)
2021-12-27 20:49:12 +0100 <zincy> ok thanks
2021-12-27 20:49:36 +0100 <zincy> I am guessing that I wont pick this up by reading and will have to actually play around with a dependently typed language
2021-12-27 20:49:43 +0100 <EvanR> yeah
2021-12-27 20:49:59 +0100 <zincy> Then I will be able to ask well formed questions
2021-12-27 20:51:56 +0100ksqsf(~user@134.209.106.31) (Ping timeout: 252 seconds)
2021-12-27 20:53:44 +0100gioyik(~gioyik@gateway/tor-sasl/gioyik)
2021-12-27 21:05:19 +0100juhp(~juhp@128.106.188.82) (Ping timeout: 268 seconds)
2021-12-27 21:06:03 +0100[itchyjunk](~itchyjunk@user/itchyjunk/x-7353470)
2021-12-27 21:08:29 +0100juhp(~juhp@128.106.188.82)
2021-12-27 21:09:47 +0100aner(~aner@static.219.128.itcsa.net)
2021-12-27 21:09:54 +0100aner(~aner@static.219.128.itcsa.net) (Client Quit)
2021-12-27 21:10:22 +0100argento(~argento@static.219.128.itcsa.net)
2021-12-27 21:12:07 +0100Flow(~none@gentoo/developer/flow) (Ping timeout: 268 seconds)
2021-12-27 21:15:28 +0100Flow(~none@gentoo/developer/flow)
2021-12-27 21:17:47 +0100YoungFrog(~youngfrog@39.129-180-91.adsl-dyn.isp.belgacom.be) (Ping timeout: 256 seconds)
2021-12-27 21:18:57 +0100dcoutts_(~duncan@71.78.6.51.dyn.plus.net) (Ping timeout: 240 seconds)
2021-12-27 21:18:58 +0100haask(~askham@92.234.0.237) (Remote host closed the connection)
2021-12-27 21:19:47 +0100haask(~harry@143.47.228.49)
2021-12-27 21:24:41 +0100haask(~harry@143.47.228.49) (Changing host)
2021-12-27 21:24:41 +0100haask(~harry@user/haask)
2021-12-27 21:30:20 +0100qrpnxz(abc4f95c31@user/qrpnxz) (Disconnected: Replaced by new connection)
2021-12-27 21:30:41 +0100qrpnxz(abc4f95c31@user/qrpnxz)
2021-12-27 21:32:59 +0100coot_(~coot@2a02:a310:e03f:8500:5cc8:47c:8ec0:b827)
2021-12-27 21:33:38 +0100snake(~snake@user/snake) (Leaving)
2021-12-27 21:35:17 +0100neurocyte0132889(~neurocyte@user/neurocyte) (Ping timeout: 240 seconds)
2021-12-27 21:35:21 +0100argento(~argento@static.219.128.itcsa.net) (Quit: leaving)
2021-12-27 21:35:29 +0100argento(~argento@static.204.189.itcsa.net)
2021-12-27 21:36:09 +0100coot(~coot@89-64-85-93.dynamic.chello.pl) (Ping timeout: 268 seconds)
2021-12-27 21:38:32 +0100pretty_dumm_guy(trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655)
2021-12-27 21:41:06 +0100ksqsf(~user@134.209.106.31)
2021-12-27 21:45:10 +0100justsomeguy(~justsomeg@user/justsomeguy)
2021-12-27 21:46:07 +0100ksqsf(~user@134.209.106.31) (Ping timeout: 256 seconds)
2021-12-27 21:48:30 +0100pavonia(~user@user/siracusa)
2021-12-27 21:54:15 +0100bitdex(~bitdex@gateway/tor-sasl/bitdex) (Quit: = "")
2021-12-27 21:54:30 +0100hololeap(~hololeap@user/hololeap)
2021-12-27 21:54:42 +0100yauhsien(~yauhsien@61-231-42-148.dynamic-ip.hinet.net)
2021-12-27 21:56:46 +0100oldsk00l(~znc@ec2-52-57-80-8.eu-central-1.compute.amazonaws.com)
2021-12-27 22:02:44 +0100otherwise(~otherwise@2601:602:880:90f0:7490:2afa:37a4:523b) (Remote host closed the connection)
2021-12-27 22:02:58 +0100jackson99(~bc8147f2@cerf.good1.com)
2021-12-27 22:03:35 +0100argento(~argento@static.204.189.itcsa.net) (Remote host closed the connection)
2021-12-27 22:04:04 +0100yauhsien(~yauhsien@61-231-42-148.dynamic-ip.hinet.net) (Remote host closed the connection)
2021-12-27 22:04:49 +0100yauhsien(~yauhsien@61-231-42-148.dynamic-ip.hinet.net)
2021-12-27 22:07:28 +0100 <[itchyjunk]> Non haskell question, i was made aware of a "omega combinator" which is (\x.xx) (\x.xx). But googling "omega combinator" mostly gives me things about JS. does it have alternative name?
2021-12-27 22:08:49 +0100 <geekosaur> doubled y combinator. which adds little over a single y combinator
2021-12-27 22:08:59 +0100 <geekosaur> (y combinator applied to another y combinator)
2021-12-27 22:09:12 +0100 <[itchyjunk]> hmmm
2021-12-27 22:09:17 +0100yauhsien(~yauhsien@61-231-42-148.dynamic-ip.hinet.net) (Ping timeout: 240 seconds)
2021-12-27 22:10:17 +0100 <[itchyjunk]> Argh, googling anything with ycombinator seems to result the incubator website and not the ycombinator i want :D
2021-12-27 22:10:21 +0100geekosaur(~geekosaur@xmonad/geekosaur) (Remote host closed the connection)
2021-12-27 22:11:31 +0100 <hpc> try "fixed point combinator"
2021-12-27 22:11:55 +0100 <hpc> or adding "lambda calculus" to the search
2021-12-27 22:12:01 +0100geekosaur(~geekosaur@xmonad/geekosaur)
2021-12-27 22:12:11 +0100 <[itchyjunk]> ahh ty
2021-12-27 22:12:27 +0100 <[itchyjunk]> i had seed fixed point combinator wiki page actually, didn't realize that was what i wanted
2021-12-27 22:12:36 +0100 <[exa]> [itchyjunk]: I never saw anyone to refer it in a different way than just Ω = ωω; sometimes it is very informally called "infinite loop"
2021-12-27 22:12:44 +0100rito_(~rito_gh@45.112.243.219) (Quit: Leaving)
2021-12-27 22:13:09 +0100shriekingnoise(~shrieking@186.137.144.80) (Ping timeout: 268 seconds)
2021-12-27 22:13:19 +0100 <[exa]> fixpoint combinators (Y) are a tiny bit more complex because they have the `f` there. In fact Ω = YI
2021-12-27 22:14:47 +0100zer0bitz(~zer0bitz@185.112.82.230) (Read error: Connection reset by peer)
2021-12-27 22:14:57 +0100 <[exa]> geekosaur: btw you meant YY ? (/me tries that kind of recursion in head)
2021-12-27 22:15:00 +0100 <[itchyjunk]> Right. I was watching a "computerphile" video on it and he gives an exercise for fixed point combinator but he covers the (\x.xx) (\x.xx) thing on it's own
2021-12-27 22:15:02 +0100 <[exa]> (head explodes)
2021-12-27 22:16:08 +0100 <[exa]> anyway it's likely the smallest λ-term with no normal form (ie "fully reduced")
2021-12-27 22:16:33 +0100hololeap(~hololeap@user/hololeap) (Ping timeout: 276 seconds)
2021-12-27 22:23:28 +0100 <EvanR> the heck is omega combinator is js
2021-12-27 22:23:33 +0100 <EvanR> in js
2021-12-27 22:25:21 +0100 <iphy> never heard of it in js, and my google search yields nothing
2021-12-27 22:26:00 +0100 <[exa]> const Ω = () => {while(true){}};
2021-12-27 22:26:18 +0100 <[exa]> seems like I'll need to restart the browser now.
2021-12-27 22:27:18 +0100qrpnxz(abc4f95c31@user/qrpnxz) (Disconnected: Replaced by new connection)
2021-12-27 22:27:26 +0100qrpnxz(abc4f95c31@user/qrpnxz)
2021-12-27 22:27:42 +0100 <hpc> using while seems like cheating...
2021-12-27 22:27:58 +0100 <[exa]> nah I properly inlined that!
2021-12-27 22:28:20 +0100qrpnxz(abc4f95c31@user/qrpnxz) (Disconnected: closed)
2021-12-27 22:28:32 +0100qrpnxz(abc4f95c31@user/qrpnxz)
2021-12-27 22:28:43 +0100 <EvanR> i know how to do lambda calculus in js, was wondering if it was some terribly named unrelated library xD
2021-12-27 22:29:16 +0100hueso(~root@user/hueso) (Quit: hueso)
2021-12-27 22:31:17 +0100xff0x(~xff0x@2001:1a81:53c9:5600:de59:5c41:aa07:4876) (Ping timeout: 240 seconds)
2021-12-27 22:32:29 +0100xff0x(~xff0x@2001:1a81:53c9:5600:4d50:2309:32ab:9f17)
2021-12-27 22:32:36 +0100tromp(~textual@dhcp-077-249-230-040.chello.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
2021-12-27 22:32:50 +0100 <[exa]> hpc: never underestimate properly applied optimizations https://godbolt.org/z/3skK9j
2021-12-27 22:33:07 +0100steven1(~steven@74.215.200.15)
2021-12-27 22:33:40 +0100 <EvanR> what
2021-12-27 22:33:47 +0100altern(~Sergii@altern.corbina.com.ua) (Quit: Leaving)
2021-12-27 22:34:33 +0100hueso(~root@user/hueso)
2021-12-27 22:34:34 +0100 <steven1> hello, is `data Void -- empty` considered isomorphic to forall a. a ? I initially thought yes, but it seems I can go Void -> a with `absurd v = case v of { }`, but I can't go a -> Void since I obviously can't construct a value of type Void
2021-12-27 22:34:46 +0100 <steven1> I can use undefined of course, but not sure if that's allowed when I'm trying to find an isomorphism
2021-12-27 22:35:07 +0100 <EvanR> they both have no real values, and they both have undefined
2021-12-27 22:35:17 +0100ksqsf(~user@134.209.106.31)
2021-12-27 22:35:34 +0100 <EvanR> so either way they are in correspondence
2021-12-27 22:35:43 +0100merijn(~merijn@83-160-49-249.ip.xs4all.nl)
2021-12-27 22:36:27 +0100 <lyxia> steven1: a -> Void is different from (forall a. a) -> Void.
2021-12-27 22:36:37 +0100 <steven1> ah that is true
2021-12-27 22:36:58 +0100 <steven1> then again I can still write the same absurd definition for that type too I think
2021-12-27 22:37:00 +0100drewr(~drew@user/drewr)
2021-12-27 22:37:16 +0100 <steven1> oh wait that's the other way
2021-12-27 22:37:25 +0100 <lyxia> you can also just do \x -> x
2021-12-27 22:37:37 +0100 <steven1> ah that's right
2021-12-27 22:39:57 +0100ksqsf(~user@134.209.106.31) (Ping timeout: 240 seconds)
2021-12-27 22:41:57 +0100 <steven1> I was trying to derive the representation of existential types by hand. e.g. (forall r. r -> a) -> a is the same as exists r. r What I found is that exists r. r is isomorphic to (forall r. r -> Void) -> Void but this definition doesn't seem to work
2021-12-27 22:42:12 +0100tromp(~textual@dhcp-077-249-230-040.chello.nl)
2021-12-27 22:42:27 +0100 <steven1> intuitively it seems like (forall r. r -> Void) -> Void is also isomorphic to forall a. (forall r. r -> a) -> a but I can't prove it
2021-12-27 22:43:00 +0100 <steven1> and if I try to use the void version in haskell the same way it doesn't seem to work. Obviously it only returns Void so I can't possibly get any information out of it
2021-12-27 22:44:08 +0100 <EvanR> well you just picked a = Void
2021-12-27 22:44:15 +0100 <EvanR> not a problem
2021-12-27 22:44:31 +0100 <steven1> yeah but I can't seem to go the other way
2021-12-27 22:45:06 +0100 <EvanR> hmm?
2021-12-27 22:45:13 +0100 <steven1> e.g. I can see that exists r. r == (forall r. r -> Void) -> Void . But I don't see how to get from this to the forall a version
2021-12-27 22:45:14 +0100_ht(~quassel@82-169-194-8.biz.kpn.net) (Remote host closed the connection)
2021-12-27 22:45:47 +0100 <steven1> once I know that forall a . (forall r. r -> a) -> a is the answer, I know how to go backward, but I don't see how I could have gotten there from what I have
2021-12-27 22:45:52 +0100 <EvanR> one's a justified specialization of the other
2021-12-27 22:46:03 +0100 <EvanR> not sure how you'd undo that
2021-12-27 22:46:47 +0100 <EvanR> it's like saying, if I know reverse :: [Char] -> [Char], how do I prove that reverse can work for any type of list
2021-12-27 22:46:58 +0100 <EvanR> (without looking at the code)
2021-12-27 22:47:06 +0100acidjnk(~acidjnk@pd9e0bdc0.dip0.t-ipconnect.de)
2021-12-27 22:47:44 +0100 <steven1> yeah, I thought the isomorphism from Void to forall a. a might help, but it's not clear to me. Let me run through the steps a bit and see if I get somewhere
2021-12-27 22:49:14 +0100 <EvanR> the specialized fact you saw reflects that anything "false" about the hidden value... is false
2021-12-27 22:49:44 +0100 <steven1> ah that's intereseting intuition
2021-12-27 22:49:57 +0100drewr(~drew@user/drewr) (Ping timeout: 240 seconds)
2021-12-27 22:49:58 +0100 <steven1> then maybe my derivation is strictly less powerful than the other version
2021-12-27 22:53:55 +0100 <steven1> let me post my steps in a minute and maybe someone can find an error in what I've done
2021-12-27 22:56:59 +0100 <steven1> https://gist.github.com/stevenfontanella/c26bfbf79f615ae0145ae4704df8b47f here's what I did
2021-12-27 22:57:24 +0100 <steven1> I am kind of mixing predicate logic with 'type' logic which might be wrong
2021-12-27 22:58:03 +0100 <steven1> one thing I'm not sure of is line 2 actually, since tecnically it should be an exclusive disjunction I guess (one value can't have multiple types)
2021-12-27 22:58:07 +0100 <EvanR> a proof of not a = a -> Void seems funny
2021-12-27 22:58:27 +0100 <steven1> yeah not too sure of that either
2021-12-27 22:58:41 +0100 <steven1> it should be true in predicate logic but not sure if it carries over to this
2021-12-27 22:59:11 +0100 <EvanR> that's just the definition of not
2021-12-27 22:59:20 +0100DNH(~DNH@2a02:8108:1100:16d8:6043:aa58:f99b:e1b) (Quit: My MacBook has gone to sleep. ZZZzzz…)
2021-12-27 23:00:06 +0100 <monochrom> What is "\/ a" doing on its own line? Syntax error?
2021-12-27 23:00:20 +0100 <steven1> it's like a disjunction over a set
2021-12-27 23:00:43 +0100 <EvanR> the lines seem a bit incomplete, like they're not saying anything
2021-12-27 23:01:05 +0100drewr(~drew@user/drewr)
2021-12-27 23:01:18 +0100zincy(~zincy@2a00:23c8:970c:4801:bdb9:8c5f:3085:2807) (Remote host closed the connection)
2021-12-27 23:01:19 +0100 <EvanR> exists a . a doesn't seem equal to \/ a or anything
2021-12-27 23:01:31 +0100 <steven1> by \/ a I mean we're doing a disjunction over all types e.g. t1 \/ t2 \/ t3 \/ t4 and so on
2021-12-27 23:01:38 +0100 <EvanR> lol what
2021-12-27 23:01:39 +0100alekhine_(~alekhine@c-73-38-152-33.hsd1.ma.comcast.net)
2021-12-27 23:02:05 +0100 <steven1> I was thinking exists a. a means a is either t1, or t2, etc. so I represent it as a logical disjunction
2021-12-27 23:02:49 +0100 <monochrom> You don't need to "translate" exists a. a to \/a just to use de Morgan. not (forall a. not a) is just fine.
2021-12-27 23:02:54 +0100 <EvanR> it means there exists a type
2021-12-27 23:03:16 +0100 <monochrom> Hell, you don't need to "translate", period.
2021-12-27 23:03:23 +0100 <alekhine_> Hello. I'm trying to get a handle on this language, but i'm having trouble finding resources beyond the wiki and the purple book. I've written a couple very basic things but that's it. I have experience in imperative languages. If anybody could recommend some stuff for a beginner, that would be great. I appreciate any help
2021-12-27 23:03:57 +0100 <steven1> monochrom: hmm ok, my motivation was to derive the representation of existential types (forall r. r -> a) -> a from scratch
2021-12-27 23:04:05 +0100 <EvanR> if someone tells you there exists a type a, well there you have it. That is what type there is
2021-12-27 23:05:06 +0100 <EvanR> doing a set complement on the whole universe types sounds interesting and outside the usual realm of possibility xD
2021-12-27 23:05:12 +0100 <steven1> alekhine_: what's the purple book? I liked learn you a haskell when I started
2021-12-27 23:05:36 +0100drewr(~drew@user/drewr) (Client Quit)
2021-12-27 23:05:58 +0100 <steven1> EvanR: yeah, could be. My derivation is close so I'm thinking there could be some connection here
2021-12-27 23:06:03 +0100oldsk00l(~znc@ec2-52-57-80-8.eu-central-1.compute.amazonaws.com) (Remote host closed the connection)
2021-12-27 23:06:05 +0100 <monochrom> alekhine_: I don't know what's the purpose book. My http://www.vex.net/~trebla/haskell/learn-sources.html comments on some books and works I know. Maybe you find something suitable to you or not.
2021-12-27 23:06:08 +0100 <alekhine_> steven1: I was referring to Haskell Programming from First Principles, by Chris Allen and Julie Moronuki
2021-12-27 23:06:33 +0100 <alekhine_> Thanks monochrom
2021-12-27 23:06:37 +0100alx741(~alx741@157.100.93.160) (Read error: Connection reset by peer)
2021-12-27 23:08:00 +0100 <dsal> alekhine_: That book is pretty great, but if you're not understanding something, it'd be easier to offer guidance if you said what you didn't understand and gave some context as to why you didn't understand it.
2021-12-27 23:08:34 +0100 <dsal> e.g., "experience in imperative languages" hints at some handicaps that will make a few things harder to understand.
2021-12-27 23:08:37 +0100 <geekosaur> @where paste
2021-12-27 23:08:37 +0100 <lambdabot> Help us help you: please paste full code, input and/or output at e.g. https://paste.tomsmeding.com
2021-12-27 23:09:22 +0100 <monochrom> Yeah, there is diminishing return in more reading.
2021-12-27 23:09:57 +0100merijn(~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 250 seconds)
2021-12-27 23:10:41 +0100 <monochrom> And the 1000-page tome is already a lot of reading.
2021-12-27 23:11:01 +0100 <iphy> which combinator can I use to implement this function? https://github.com/iphydf/hs-cimple/blob/fix/test/Language/Cimple/ASTSpec.hs#L25
2021-12-27 23:11:38 +0100 <EvanR> steven1, so you proved (exists a . a) -> (forall r . r -> b) -> b. With \e f -> f e. And you want to prove ((forall r . r -> Void) -> Void) -> (exists a . a) ?
2021-12-27 23:12:00 +0100 <alekhine_> Fair enough dsal. I guess I'm trying to just learn everything I can do? I think I want a list of topics or features I need to know about so I can write useful programs, then move on to more advanced things later
2021-12-27 23:12:01 +0100 <EvanR> or
2021-12-27 23:12:53 +0100 <monochrom> That direction is probably unprovable in constructive logics.
2021-12-27 23:13:08 +0100 <alekhine_> And yes, my ingrained imperative experience has actually hindered my learning.
2021-12-27 23:13:17 +0100 <steven1> EvanR: I guess I proved (exists a. a) -> (forall r. r -> Void) -> Void
2021-12-27 23:13:23 +0100machinedgod(~machinedg@24.105.81.50) (Ping timeout: 256 seconds)
2021-12-27 23:13:25 +0100Henson(~kvirc@107-179-133-201.cpe.teksavvy.com)
2021-12-27 23:13:29 +0100 <dsal> alekhine_: I found the book pretty good for that. It's hard to know what's holding you up, though.
2021-12-27 23:13:32 +0100 <EvanR> turns out using some basic assumptions you can translate any imperative program into a functional program xD
2021-12-27 23:13:41 +0100 <EvanR> for what it's worth
2021-12-27 23:13:42 +0100 <dsal> I had a few programs I'd written in Haskell that I'd been using while going through that book.
2021-12-27 23:13:50 +0100 <monochrom> Indeed Kant complained about Hilbert's PhD thesis precisely because Hilbert was pulling that off.
2021-12-27 23:13:54 +0100 <steven1> and I want to go to ((forall r. r -> Void) -> Void) -> (forall a. (forall r. r -> a) -> a)
2021-12-27 23:14:11 +0100 <EvanR> yeah, doesn't seem plausible to do that
2021-12-27 23:15:08 +0100 <alekhine_> dsal: fair enough, i'll go find some problem to bash my head against then come back with a more specific question
2021-12-27 23:15:15 +0100 <monochrom> The statement to be proved was "there exists blah blah", Hilbert did "if blah blah didn't exist, something would go wrong". Kant was like "that's not math, that's theology".
2021-12-27 23:15:25 +0100 <EvanR> haha
2021-12-27 23:15:37 +0100 <steven1> yeah, that's too bad. I tried subbing Void = forall a. a but it doesn't seem to help. There's no way to require that both Voids are the same a. At least, I'm not sure whether I'm allowed to 'pull out' the forall
2021-12-27 23:15:45 +0100solidfox(~snake@user/snake)
2021-12-27 23:16:07 +0100 <EvanR> sure
2021-12-27 23:16:14 +0100 <EvanR> the forall a
2021-12-27 23:16:19 +0100 <EvanR> doesn't changing anything
2021-12-27 23:16:35 +0100 <EvanR> might make it even more clear what's going on
2021-12-27 23:17:09 +0100 <steven1> yeah, basically I can make it into (forall r. r -> (forall a. a)) -> (forall a. a) but seems like I'm stuck from here
2021-12-27 23:17:51 +0100 <EvanR> once multiple different a appear I go for a third letter
2021-12-27 23:17:56 +0100 <EvanR> just to avoid confusion
2021-12-27 23:18:10 +0100tromp(~textual@dhcp-077-249-230-040.chello.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
2021-12-27 23:18:54 +0100 <Henson> Hi everyone, I'm trying to build a project in which a Haskell function is exported to C via the FFI, but I'm getting an "undefined reference" to the exported function at link time. What can I put in the cabal file to make C find this Haskell function? Finding the C function in Haskell works just fine.
2021-12-27 23:23:15 +0100solidfoxsnake
2021-12-27 23:23:19 +0100 <Henson> hmm, it seems if I move the library in question from "exposed-modules" to "other-modules" it compiles and gets rid of the error.
2021-12-27 23:24:46 +0100 <EvanR> steven1, or... the task of proving that A implies B when A and B can be proven independently is possible but pointless
2021-12-27 23:25:08 +0100deadmarshal(~deadmarsh@95.38.112.219)
2021-12-27 23:25:18 +0100 <EvanR> i.e. f :: Int -> Char, f _ = 'c'
2021-12-27 23:25:21 +0100 <EvanR> Int implies Char
2021-12-27 23:25:36 +0100takuan(~takuan@178-116-218-225.access.telenet.be) (Remote host closed the connection)
2021-12-27 23:25:45 +0100 <steven1> Void can't be proven though
2021-12-27 23:25:55 +0100 <EvanR> no Void is happening in your theorem
2021-12-27 23:25:56 +0100snake(~snake@user/snake) (Leaving)
2021-12-27 23:26:12 +0100alx741(~alx741@157.100.93.160)
2021-12-27 23:26:35 +0100 <EvanR> unless i copy pasted wrong
2021-12-27 23:26:50 +0100 <EvanR> ((forall r. r -> Void) -> Void) -> (forall a. (forall r. r -> a) -> a)
2021-12-27 23:27:42 +0100 <steven1> yeah that's what I want
2021-12-27 23:28:02 +0100 <EvanR> \_ f = f id
2021-12-27 23:28:07 +0100 <dsal> alekhine_: Yeah, for me, having a thing I want to work on makes learning *way* easier.
2021-12-27 23:28:23 +0100 <steven1> you're saying that has that type?
2021-12-27 23:28:33 +0100 <EvanR> yeah, a = Void -> Void xD
2021-12-27 23:28:38 +0100 <EvanR> er
2021-12-27 23:28:44 +0100 <EvanR> the second r = Void -> Void
2021-12-27 23:29:21 +0100 <EvanR> they are just independent
2021-12-27 23:29:22 +0100ksqsf(~user@134.209.106.31)
2021-12-27 23:29:34 +0100deadmarshal(~deadmarsh@95.38.112.219) (Ping timeout: 260 seconds)
2021-12-27 23:29:47 +0100 <EvanR> all this leads back to the premise "someone tells you there exists a type, now what"
2021-12-27 23:29:55 +0100 <steven1> hmm let me think about your definition
2021-12-27 23:29:57 +0100dan-so(~danso@2001:1970:52e7:d000:96b8:6dff:feb3:c009) (Ping timeout: 240 seconds)
2021-12-27 23:29:59 +0100 <EvanR> rather, there is a type and it's inhabited
2021-12-27 23:33:00 +0100coot_(~coot@2a02:a310:e03f:8500:5cc8:47c:8ec0:b827) (Quit: coot_)
2021-12-27 23:33:44 +0100 <steven1> yes, I see your point, we basically ignored the first argument and then proved this: theorem :: (forall a. (forall r. r -> a) -> a)
2021-12-27 23:33:50 +0100 <steven1> theorem f = f id
2021-12-27 23:33:57 +0100 <steven1> which is like saying exists r. r
2021-12-27 23:34:02 +0100 <steven1> 'there exists a type'
2021-12-27 23:34:09 +0100 <EvanR> that is inhabited
2021-12-27 23:34:14 +0100ksqsf(~user@134.209.106.31) (Ping timeout: 260 seconds)
2021-12-27 23:34:18 +0100 <EvanR> for example, Void -> Void xD
2021-12-27 23:35:30 +0100 <EvanR> alternatively show that some type is inhabited
2021-12-27 23:35:32 +0100 <steven1> I think our formulation was wrong: theorem :: ((forall r. r -> Void) -> Void) -> (forall a. (forall r. r -> a) -> a). The r on the right is different from the r on the left
2021-12-27 23:35:45 +0100 <steven1> the left should imply that that r exists, not some other r
2021-12-27 23:36:22 +0100 <EvanR> it's "implied" by being unrelated and also "true"
2021-12-27 23:36:31 +0100 <steven1> yeah
2021-12-27 23:36:40 +0100 <steven1> that's why I'm thinking we proved the wrong thing
2021-12-27 23:37:11 +0100cosimone(~user@93-47-231-248.ip115.fastwebnet.it) (Ping timeout: 256 seconds)
2021-12-27 23:37:17 +0100 <steven1> ah, this is tough
2021-12-27 23:37:25 +0100 <EvanR> the informal thing you were saying made no real sense, so I take a win if I can get it xD
2021-12-27 23:38:17 +0100 <steven1> I can believe that, not sure where I went wrong though
2021-12-27 23:38:25 +0100 <EvanR> the Void version of church encoded(?) existential is a possibility but doesn't really have any bearing on the general version or help
2021-12-27 23:38:49 +0100 <steven1> yeah
2021-12-27 23:40:13 +0100shriekingnoise(~shrieking@186.137.144.80)
2021-12-27 23:41:51 +0100 <steven1> well, thanks for the help EvanR . Maybe I will get some inspiration another time
2021-12-27 23:42:14 +0100steven1(~steven@74.215.200.15) (Quit: WeeChat 2.8)
2021-12-27 23:44:19 +0100qrpnxz(abc4f95c31@user/qrpnxz) (Disconnected: Replaced by new connection)
2021-12-27 23:44:32 +0100qrpnxz(abc4f95c31@user/qrpnxz)
2021-12-27 23:45:36 +0100eggplantade(~Eggplanta@2600:1700:bef1:5e10:b417:46a:3118:ab81) (Remote host closed the connection)
2021-12-27 23:50:10 +0100qrpnxz(abc4f95c31@user/qrpnxz) (Disconnected: Replaced by new connection)
2021-12-27 23:50:13 +0100qrpnxz(abc4f95c31@user/qrpnxz)
2021-12-27 23:51:14 +0100acode(~acode@151.65.31.181) (Quit: Client closed)
2021-12-27 23:56:25 +0100qrpnxz(abc4f95c31@user/qrpnxz) (Disconnected: Replaced by new connection)
2021-12-27 23:56:27 +0100qrpnxz(abc4f95c31@user/qrpnxz)