Home liberachat/#haskell: Logs Calendar

Logs on 2024-04-02 (liberachat/#haskell)

00:00:20 → destituion joins (~destituio@2a02:2121:655:c95b:9402:ea22:1848:e3db)
00:05:49 → pavonia joins (~user@user/siracusa)
00:10:02 × caconym quits (~caconym@user/caconym) (Read error: Connection reset by peer)
00:10:17 → caconym joins (~caconym@user/caconym)
00:20:55 geekopurr is now known as geekosaur
00:38:13 × fererrorocher quits (fererroroc@gateway/vpn/protonvpn/fererrorocher) (Quit: WeeChat 4.2.1)
01:08:07 × dbaoty quits (~dbaoty@tptn-04-0838.dsl.iowatelecom.net) (Quit: Leaving.)
01:25:51 × machinedgod quits (~machinedg@d173-183-246-216.abhsia.telus.net) (Ping timeout: 256 seconds)
01:32:07 × tertek quits (~tertek@user/tertek) (Quit: %quit%)
01:32:28 → tertek joins (~tertek@user/tertek)
01:33:10 → Achylles joins (~Achylles@45.182.57.3)
01:33:23 → falafel_ joins (~falafel@162.83.249.190)
01:37:17 → FragByte_ joins (~christian@user/fragbyte)
01:37:35 × FragByte quits (~christian@user/fragbyte) (Ping timeout: 260 seconds)
01:37:35 FragByte_ is now known as FragByte
01:37:46 → Achylles_ joins (~Achylles@45.182.57.3)
01:41:03 → Achylles__ joins (~Achylles@45.182.57.3)
01:41:09 × xff0x quits (~xff0x@2405:6580:b080:900:2b2b:eb19:37de:d4bd) (Ping timeout: 256 seconds)
01:41:40 × Achylles quits (~Achylles@45.182.57.3) (Quit: Leaving)
01:41:43 × Achylles__ quits (~Achylles@45.182.57.3) (Read error: Connection reset by peer)
01:41:43 × Achylles_ quits (~Achylles@45.182.57.3) (Read error: Connection reset by peer)
01:45:59 × waleee quits (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) (Ping timeout: 272 seconds)
01:50:07 × otto_s quits (~user@p4ff2714c.dip0.t-ipconnect.de) (Ping timeout: 268 seconds)
01:50:13 → Guest23 joins (~Guest23@static.126144025125.cidr.jtidc.jp)
01:51:31 → otto_s joins (~user@p4ff27c9e.dip0.t-ipconnect.de)
01:53:43 <Guest23> I have a question.
01:53:43 <Guest23> Is there any way to show `definition of self defined data type`?
01:53:44 <Guest23> Like this
01:53:44 <Guest23> ```
01:53:45 <Guest23> data Mydata = Foo | Bar
01:53:45 <Guest23> main = print Mydata
01:53:46 <Guest23>        -- > "Mydata = Foo | Bar"
01:53:46 <Guest23> ```
01:54:24 × mei quits (~mei@user/mei) (Remote host closed the connection)
01:56:31 <geekosaur> it might be possible via Genetics
01:56:49 <geekosaur> er, Generics
01:56:49 → mei joins (~mei@user/mei)
01:57:58 <geekosaur> types are otherwise erased at runtime, so that information isn't available
02:03:39 → iteratee_ joins (~kyle@162.218.222.207)
02:03:47 × iteratee quits (~kyle@162.218.222.207) (Read error: Connection reset by peer)
02:10:57 × ski quits (~ski@ext-1-033.eduroam.chalmers.se) (Ping timeout: 255 seconds)
02:14:27 → infinity0_ joins (~infinity0@pwned.gg)
02:14:27 infinity0 is now known as Guest4479
02:14:27 × Guest4479 quits (~infinity0@pwned.gg) (Killed (zinc.libera.chat (Nickname regained by services)))
02:14:27 infinity0_ is now known as infinity0
02:23:22 → ski joins (~ski@ext-1-033.eduroam.chalmers.se)
02:25:54 → xff0x joins (~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp)
02:30:27 × bitdex quits (~bitdex@gateway/tor-sasl/bitdex) (Remote host closed the connection)
02:31:20 → rosco joins (~rosco@121.120.71.44)
02:31:31 → bitdex joins (~bitdex@gateway/tor-sasl/bitdex)
02:32:52 × bitdex quits (~bitdex@gateway/tor-sasl/bitdex) (Remote host closed the connection)
02:33:59 → bitdex joins (~bitdex@gateway/tor-sasl/bitdex)
02:39:29 × rosco quits (~rosco@121.120.71.44) (Quit: Lost terminal)
02:40:46 × falafel_ quits (~falafel@162.83.249.190) (Ping timeout: 264 seconds)
02:48:23 × califax quits (~califax@user/califx) (Remote host closed the connection)
02:48:47 → califax joins (~califax@user/califx)
02:49:40 × califax quits (~califax@user/califx) (Remote host closed the connection)
02:50:04 → califax joins (~califax@user/califx)
02:51:45 → machinedgod joins (~machinedg@d173-183-246-216.abhsia.telus.net)
02:54:21 × califax quits (~califax@user/califx) (Remote host closed the connection)
02:54:41 → califax joins (~califax@user/califx)
02:55:43 × Guest23 quits (~Guest23@static.126144025125.cidr.jtidc.jp) (Quit: Client closed)
03:00:53 × td_ quits (~td@i53870937.versanet.de) (Ping timeout: 252 seconds)
03:02:35 → td_ joins (~td@i53870933.versanet.de)
03:04:02 × califax quits (~califax@user/califx) (Remote host closed the connection)
03:04:21 → califax joins (~califax@user/califx)
03:15:13 → Square2 joins (~Square@user/square)
03:29:26 × aforemny quits (~aforemny@2001:9e8:6cd9:500:d9a4:1707:4c79:474) (Ping timeout: 256 seconds)
03:29:37 → aforemny_ joins (~aforemny@2001:9e8:6cfb:ec00:7756:c37a:675d:87ba)
03:29:49 → ezzieyguywuf joins (~Unknown@user/ezzieyguywuf)
03:33:33 → igemnace joins (~ian@user/igemnace)
03:35:11 × erisco quits (~erisco@d24-141-66-165.home.cgocable.net) (Ping timeout: 260 seconds)
03:35:17 <Inst> just curious, but how much vomit do existential types provoke?
03:35:31 → erisco joins (~erisco@d24-141-66-165.home.cgocable.net)
03:36:17 <Inst> it looks very useful, but it seems as though it's potentially a deathtrap
03:39:03 <Inst> yup, seems to make the type checker go haywire
03:48:28 × dsrt^ quits (~cd@c-98-242-74-66.hsd1.ga.comcast.net) (Remote host closed the connection)
03:52:18 → Square joins (~Square4@user/square)
03:55:18 × Square2 quits (~Square@user/square) (Ping timeout: 268 seconds)
03:59:35 × ezzieyguywuf quits (~Unknown@user/ezzieyguywuf) (Remote host closed the connection)
04:00:32 → ezzieyguywuf joins (~Unknown@user/ezzieyguywuf)
04:01:38 <ski> haywire, how ?
04:04:42 × ec_ quits (~ec@gateway/tor-sasl/ec) (Ping timeout: 260 seconds)
04:06:41 → ec_ joins (~ec@gateway/tor-sasl/ec)
04:46:47 × adanwan quits (~adanwan@gateway/tor-sasl/adanwan) (Remote host closed the connection)
04:47:08 → adanwan joins (~adanwan@gateway/tor-sasl/adanwan)
04:52:17 × adanwan quits (~adanwan@gateway/tor-sasl/adanwan) (Remote host closed the connection)
04:52:33 → adanwan joins (~adanwan@gateway/tor-sasl/adanwan)
05:05:45 → _ht joins (~Thunderbi@28-52-174-82.ftth.glasoperator.nl)
05:23:20 × machinedgod quits (~machinedg@d173-183-246-216.abhsia.telus.net) (Ping timeout: 252 seconds)
05:24:59 × xal quits (~xal@mx1.xal.systems) ()
05:31:28 → euphores joins (~SASL_euph@user/euphores)
05:53:41 × euphores quits (~SASL_euph@user/euphores) (Ping timeout: 240 seconds)
06:00:04 × Sgeo quits (~Sgeo@user/sgeo) (Read error: Connection reset by peer)
06:14:53 → xal joins (~xal@mx1.xal.systems)
06:21:38 → peterbecich joins (~Thunderbi@047-229-123-186.res.spectrum.com)
06:21:53 → michalz joins (~michalz@185.246.207.200)
06:26:51 × peterbecich quits (~Thunderbi@047-229-123-186.res.spectrum.com) (Remote host closed the connection)
06:28:08 → gmg joins (~user@user/gehmehgeh)
06:28:15 → peterbecich joins (~Thunderbi@047-229-123-186.res.spectrum.com)
06:33:03 × stiell_ quits (~stiell@gateway/tor-sasl/stiell) (Remote host closed the connection)
06:34:08 → stiell_ joins (~stiell@gateway/tor-sasl/stiell)
06:46:51 → lortabac joins (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4)
06:47:23 → acidjnk_new joins (~acidjnk@p200300d6e714dc8721a8bc0199a4b6df.dip0.t-ipconnect.de)
06:49:36 → danza joins (~francesco@151.57.164.121)
06:55:59 × peterbecich quits (~Thunderbi@047-229-123-186.res.spectrum.com) (Ping timeout: 268 seconds)
06:57:34 → tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
07:00:22 × CrunchyFlakes quits (~CrunchyFl@ip92348280.dynamic.kabel-deutschland.de) (Quit: ZNC 1.8.2 - https://znc.in)
07:04:21 → CrunchyFlakes joins (~CrunchyFl@ip92348280.dynamic.kabel-deutschland.de)
07:12:10 × bitdex quits (~bitdex@gateway/tor-sasl/bitdex) (Remote host closed the connection)
07:13:11 → bitdex joins (~bitdex@gateway/tor-sasl/bitdex)
07:17:31 → zetef joins (~quassel@5.2.182.99)
07:26:10 → SurfBlueCrab joins (~SurfBlueC@nyc.nanobit.org)
07:43:31 → oo_miguel joins (~Thunderbi@78-11-181-16.static.ip.netia.com.pl)
07:44:11 × tzh quits (~tzh@c-73-164-206-160.hsd1.or.comcast.net) (Quit: zzz)
07:49:12 × econo_ quits (uid147250@id-147250.tinside.irccloud.com) (Quit: Connection closed for inactivity)
07:51:17 × danza quits (~francesco@151.57.164.121) (Ping timeout: 240 seconds)
07:53:20 × zetef quits (~quassel@5.2.182.99) (Ping timeout: 268 seconds)
07:53:30 → CiaoSen joins (~Jura@2a05:5800:2b2:5300:e6b9:7aff:fe80:3d03)
07:57:11 → machinedgod joins (~machinedg@d173-183-246-216.abhsia.telus.net)
08:04:41 → zetef joins (~quassel@5.2.182.99)
08:07:47 × remmie quits (ianremsen@tilde.team) (Ping timeout: 264 seconds)
08:08:17 × igemnace quits (~ian@user/igemnace) (Read error: Connection reset by peer)
08:09:49 <tomsmeding> Inst: you unpack existentials by pattern matching on the constructor containing them
08:10:23 <tomsmeding> (which you can read as compatible with the CPS encoding by reading "pattern matching" and "constructor" as "application" and "function", respectively)
08:10:44 <tomsmeding> you should not expect to be able to "return" an existentially quantified type from a function directly
08:11:13 <tomsmeding> apart from that, they work fine, but this need to wrap things in a constructor makes things kind of verbose sometimes
08:13:17 → danse-nr3 joins (~danse-nr3@151.57.164.121)
08:18:01 × zetef quits (~quassel@5.2.182.99) (Ping timeout: 272 seconds)
08:19:31 → remmie joins (ianremsen@tilde.team)
08:25:21 → igemnace joins (~ian@user/igemnace)
08:29:23 → zetef joins (~quassel@5.2.182.99)
08:34:52 × FragByte quits (~christian@user/fragbyte) (Ping timeout: 256 seconds)
08:35:16 × remmie quits (ianremsen@tilde.team) (Ping timeout: 268 seconds)
08:35:26 → FragByte joins (~christian@user/fragbyte)
08:41:58 × chiselfuse quits (~chiselfus@user/chiselfuse) (Remote host closed the connection)
08:42:47 → chiselfuse joins (~chiselfus@user/chiselfuse)
08:43:09 × chiselfuse quits (~chiselfus@user/chiselfuse) (Remote host closed the connection)
08:44:50 → tushar2 joins (~tushar@103.176.64.116)
08:45:04 × CiaoSen quits (~Jura@2a05:5800:2b2:5300:e6b9:7aff:fe80:3d03) (Ping timeout: 256 seconds)
08:45:24 → lisbeths joins (uid135845@id-135845.lymington.irccloud.com)
08:47:18 → Inst_ joins (~Inst@120.244.192.126)
08:47:49 → chiselfuse joins (~chiselfus@user/chiselfuse)
08:48:19 × danse-nr3 quits (~danse-nr3@151.57.164.121) (Ping timeout: 255 seconds)
08:50:11 × Inst quits (~Inst@120.244.192.126) (Ping timeout: 260 seconds)
08:51:37 × chiselfuse quits (~chiselfus@user/chiselfuse) (Remote host closed the connection)
08:52:25 × stiell_ quits (~stiell@gateway/tor-sasl/stiell) (Remote host closed the connection)
08:52:49 → stiell_ joins (~stiell@gateway/tor-sasl/stiell)
08:52:51 → chiselfuse joins (~chiselfus@user/chiselfuse)
08:54:42 × chiselfuse quits (~chiselfus@user/chiselfuse) (Remote host closed the connection)
08:55:37 → danse-nr3 joins (~danse-nr3@151.57.164.121)
08:55:41 <carbolymer> what's the good list alternative which will store its length in the type?
08:56:36 <carbolymer> this https://hackage.haskell.org/package/vec-0.5/docs/Data-Vec-Lazy.html#t:Vec ? Idk what's the best option out there
08:57:59 → chiselfuse joins (~chiselfus@user/chiselfuse)
08:59:09 × stiell_ quits (~stiell@gateway/tor-sasl/stiell) (Remote host closed the connection)
08:59:33 → stiell_ joins (~stiell@gateway/tor-sasl/stiell)
09:02:26 × danse-nr3 quits (~danse-nr3@151.57.164.121) (Read error: Connection reset by peer)
09:02:50 → danse-nr3 joins (~danse-nr3@151.57.164.121)
09:03:06 → ubert joins (~Thunderbi@2a02:8109:ab8a:5a00:5d4b:5ac:c6db:5974)
09:04:24 × Rodney_ quits (~Rodney@176.254.244.83) (Ping timeout: 260 seconds)
09:10:25 × chiselfuse quits (~chiselfus@user/chiselfuse) (Remote host closed the connection)
09:11:19 → chiselfuse joins (~chiselfus@user/chiselfuse)
09:11:59 → CiaoSen joins (~Jura@2a05:5800:2b2:5300:e6b9:7aff:fe80:3d03)
09:13:32 → Rodney_ joins (~Rodney@92.40.181.27.threembb.co.uk)
09:14:08 → remmie joins (ianremsen@tilde.team)
09:14:49 × chiselfuse quits (~chiselfus@user/chiselfuse) (Remote host closed the connection)
09:16:24 → chiselfuse joins (~chiselfus@user/chiselfuse)
09:16:48 × CiaoSen quits (~Jura@2a05:5800:2b2:5300:e6b9:7aff:fe80:3d03) (Ping timeout: 256 seconds)
09:22:11 <danse-nr3> not sure carbolymer, did not get beyond NonEmpty yet...
09:22:22 <carbolymer> :)
09:25:37 <danse-nr3> might be a debated topic where people tend to roll out their own solution
09:29:28 × Rodney_ quits (~Rodney@92.40.181.27.threembb.co.uk) (Read error: Connection reset by peer)
09:32:21 × stiell_ quits (~stiell@gateway/tor-sasl/stiell) (Remote host closed the connection)
09:32:48 → stiell_ joins (~stiell@gateway/tor-sasl/stiell)
09:34:05 × lortabac quits (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Ping timeout: 240 seconds)
09:35:01 → Rodney_ joins (~Rodney@176.254.244.83)
09:35:55 × todi quits (~todi@p57803331.dip0.t-ipconnect.de) (Ping timeout: 272 seconds)
09:36:41 × jespada quits (~jespada@cpc121308-nmal25-2-0-cust15.19-2.cable.virginm.net) (Quit: Textual IRC Client: www.textualapp.com)
09:40:42 → mmhat joins (~mmh@p200300f1c74dcfc3ee086bfffe095315.dip0.t-ipconnect.de)
09:43:33 → jespada joins (~jespada@cpc121308-nmal25-2-0-cust15.19-2.cable.virginm.net)
09:44:16 → lortabac joins (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4)
09:45:15 × tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
09:48:35 → cfricke joins (~cfricke@user/cfricke)
09:52:15 → tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
09:53:18 × chiselfuse quits (~chiselfus@user/chiselfuse) (Ping timeout: 260 seconds)
09:54:23 → todi joins (~todi@p57803331.dip0.t-ipconnect.de)
09:55:07 → chiselfuse joins (~chiselfus@user/chiselfuse)
09:56:03 × zetef quits (~quassel@5.2.182.99) (Ping timeout: 268 seconds)
09:58:20 <carbolymer> yeah, but writing my own feels like kicking an already open doors
10:01:57 → siw5ohs0 joins (~aiw5ohs0@user/aiw5ohs0)
10:02:06 ← siw5ohs0 parts (~aiw5ohs0@user/aiw5ohs0) (Leaving)
10:05:59 × todi quits (~todi@p57803331.dip0.t-ipconnect.de) (Ping timeout: 264 seconds)
10:13:34 × qqq quits (~qqq@92.43.167.61) (Read error: Connection reset by peer)
10:15:49 × xff0x quits (~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp) (Ping timeout: 272 seconds)
10:18:09 → qqq joins (~qqq@92.43.167.61)
10:21:58 × robobub quits (uid248673@id-248673.uxbridge.irccloud.com) (Quit: Connection closed for inactivity)
10:23:11 × lortabac quits (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Ping timeout: 268 seconds)
10:30:00 × Lord_of_Life quits (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 255 seconds)
10:30:51 → Lord_of_Life joins (~Lord@user/lord-of-life/x-2819915)
10:35:47 → zetef joins (~quassel@5.2.182.99)
10:38:15 × tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
10:39:53 <tomsmeding> one might also think of reducing dependencies, in light of the recent xz shenanigans :)
10:46:38 → todi joins (~todi@p57803331.dip0.t-ipconnect.de)
10:50:16 → danse-nr3_ joins (~danse-nr3@151.57.194.26)
10:51:01 → dbaoty joins (~dbaoty@tptn-04-0838.dsl.iowatelecom.net)
10:53:11 × danse-nr3 quits (~danse-nr3@151.57.164.121) (Ping timeout: 272 seconds)
10:53:25 → lortabac joins (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4)
10:56:02 → tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
10:56:43 × zetef quits (~quassel@5.2.182.99) (Remote host closed the connection)
11:04:47 × todi quits (~todi@p57803331.dip0.t-ipconnect.de) (Ping timeout: 264 seconds)
11:06:49 → zetef joins (~quassel@5.2.182.99)
11:15:46 → lvdv joins (~lvdv@203.221.237.91)
11:16:18 → xff0x joins (~xff0x@2405:6580:b080:900:ee6c:a70f:8c18:8e14)
11:30:07 → todi joins (~todi@p57803331.dip0.t-ipconnect.de)
11:33:31 × lvdv quits (~lvdv@203.221.237.91) (Ping timeout: 260 seconds)
11:35:18 → lvdv joins (~lvdv@211.30.149.12)
11:35:22 × danse-nr3_ quits (~danse-nr3@151.57.194.26) (Read error: Connection reset by peer)
11:36:37 × zetef quits (~quassel@5.2.182.99) (Ping timeout: 255 seconds)
11:38:09 → meritamen joins (~meritamen@user/meritamen)
11:41:58 × lvdv quits (~lvdv@211.30.149.12) (Ping timeout: 264 seconds)
11:43:38 → lvdv joins (~lvdv@203.221.237.91)
11:46:28 → zetef joins (~quassel@5.2.182.99)
11:49:41 × rvalue quits (~rvalue@user/rvalue) (Read error: Connection reset by peer)
11:50:11 → rvalue joins (~rvalue@user/rvalue)
11:52:54 × tushar2 quits (~tushar@103.176.64.116) (Quit: WeeChat 4.2.1)
12:05:56 × zetef quits (~quassel@5.2.182.99) (Ping timeout: 252 seconds)
12:07:43 × lvdv quits (~lvdv@203.221.237.91) (Ping timeout: 268 seconds)
12:08:13 <Inst_> tomsmeding: but I can't actually pattern match on the contained data within my existential type, or rather, I have to treat it as generic
12:08:45 <Inst_> data Foo where Whee :: forall a. Show a => a -> Foo
12:08:48 Inst_ is now known as Inst
12:08:56 <Inst> what :: Foo -> Int
12:09:05 <Inst> what (Whee "Hello") = 3
12:09:09 <Inst> doesn't typecheck
12:09:19 <tomsmeding> I mean, well, yes
12:09:23 <tomsmeding> that's what an existential is
12:09:28 <tomsmeding> you don't know what the original type was :p
12:09:51 <tomsmeding> the point of an existential is to allow this
12:10:19 → lvdv joins (~lvdv@203.221.237.91)
12:11:11 <tomsmeding> er wait
12:11:14 <Inst> realistically I can only interact it with
12:11:15 × lvdv quits (~lvdv@203.221.237.91) (Client Quit)
12:11:17 <tomsmeding> yes
12:11:21 <Inst> what (Whee a) = show a
12:11:23 <tomsmeding> yes
12:11:26 <Inst> or what (Whee ) = foo
12:11:26 <tomsmeding> that's the point
12:11:50 <tomsmeding> you can't pattern match on _types_ in haskell
12:11:57 → danse-nr3 joins (~danse-nr3@151.43.191.28)
12:12:02 <tomsmeding> you can only pattern match on _constructors_ of a known data type
12:12:15 <Inst> but the thing is basically coupled with typeclasses
12:12:21 <tomsmeding> not necessarily
12:12:28 <tomsmeding> data Foo where Whee :: a -> (a -> String) -> Foo
12:12:35 <tomsmeding> no reason a type class needs to get involved
12:12:40 <tomsmeding> it's just a natural match in some ways
12:12:48 <Inst> I was thinking something like forall a. ToHTML a, or Widget a
12:13:26 <tomsmeding> a value of type 'forall a. ToHTML a => a', where that 'forall' indicates an existential, is the same as 'HTML'
12:14:27 <tomsmeding> i.e. if you're wanting to write 'data Thing = forall a. ToHTML a => Thing a' then instead just write 'newtype Thing = Thing HTML'
12:14:46 <tomsmeding> nothing you can do with the former that you can't do with the latter
12:14:53 <tomsmeding> and the code is simpler to boot
12:15:28 <tomsmeding> in fact the former is very inflexible, you can do very little with it
12:16:04 <tomsmeding> you can't do more with "a collection of things of which you know only that they can be converted to HTML" than with "a collection of HTML documents"
12:23:45 × Maxdamantus quits (~Maxdamant@user/maxdamantus) (Ping timeout: 256 seconds)
12:24:49 × lisbeths quits (uid135845@id-135845.lymington.irccloud.com) (Quit: Connection closed for inactivity)
12:25:03 <Inst> i'm not sure if this is a plus or a minus, but this is really a problem Lisps don't have, and Haskell does, ideally, what I want is the ability to toHTML template objects
12:25:17 <Inst> but have the objects compose
12:26:12 <Inst> the interface would be Page {head = foo, body = bar}
12:26:37 <Inst> then foo you'd be able to use nested record types etc to construct / decosntruct
12:26:54 <Inst> more importantly, do it with body, then do script / style bs to inject CSS and so on
12:32:32 → Maxdamantus joins (~Maxdamant@user/maxdamantus)
12:33:16 <Inst> The idea is that you'd eventually end up with a widget ecosystem built around such a library, allowing users to just steal preexisting HTML presets etc
12:33:22 <Inst> and it'd be a user language for the platform I want to use
12:36:13 → pera_ joins (~pera@8.29.109.183)
12:36:37 → kuribas joins (~user@ip-188-118-57-242.reverse.destiny.be)
12:37:25 <Inst> beating py in terms of scripting ergonomics is hard
12:37:41 <Inst> but, say, JS / golden trio (html / css / js)? easy peasy
12:37:46 × foul_owl quits (~kerry@185.216.231.179) (Read error: Connection reset by peer)
12:40:04 <pera_> I have a general FP nomenclature question: is it correct to say "returned value" in the context of function application?
12:42:22 <ski> perhaps it would be slightly better to say "result((ing) value)" (note that there is no `return' command to specify a computation yielding a designated value as result of a function application/call)
12:43:13 <haskellbridge> <e​ldritchcookie> say how could i learn delimited continuations and more specifically control0# i think i understand callCC but control0 eludes me
12:43:14 <pera_> ski: ah resulting sound much better, thanks
12:43:34 <ski> but generally people are going to understand what you mean, probably (although newbies might still have confusions, due to the lack of such a `return'. there is no "if this happens, return this value, aborting the current computation that was doing something more")
12:43:49 <tomsmeding> Inst: isn't the thing there "dictionaries first-class in the language"?
12:43:59 <tomsmeding> "untyped objects" ~= "dictionaries"
12:44:19 × michalz quits (~michalz@185.246.207.200) (Quit: ZNC 1.8.2 - https://znc.in)
12:44:35 → michalz joins (~michalz@185.246.207.197)
12:44:43 <pera_> ski: yeah I agree
12:44:56 <ski> eldritchcookie : do you understand the CPS transform (at least the call-by-value version) ?
12:46:22 <ski> pera_ : still .. i think it is helpful to be more pedantic with word choice, pertinent distinctions, with learners and newbies. one can afford to be more sloppy with language, with people who've already grasped the basics, the important concepts and categories that are relied on in a fundamental level
12:46:40 × AlexZenon quits (~alzenon@94.233.240.255) (Quit: ;-)
12:47:29 <haskellbridge> <e​ldritchcookie> i guess so for instace some time ago i made template haskell to generate functions that turned (a1 ->... -> an -> m ()) -> m () into Cont m () (a1,..,an)
12:47:57 × AlexNoo quits (~AlexNoo@94.233.240.255) (Quit: Leaving)
12:48:09 <tomsmeding> the idea of cps is simply "turn a1 -> ... -> an -> b into a1 -> ... -> an -> forall r. (b -> r) -> r"
12:48:39 <tomsmeding> so `add (mul 2 3) 4` becomes `\k -> mul 2 3 (\prod -> add prod 4 k)`
12:49:10 <tomsmeding> the typical idea being that calls to these continuations are tail calls
12:49:46 <shapr> @quote
12:49:46 <lambdabot> gFunk says: [the main advantage of functional programs are that they're] incorrect the first 1000 times you try to compile it!
12:49:56 <haskellbridge> <e​ldritchcookie> yep and then you give it id to get the final result
12:50:01 <tomsmeding> yes
12:50:09 × meritamen quits (~meritamen@user/meritamen) (Quit: Client closed)
12:50:51 <haskellbridge> <e​ldritchcookie> before trying to understand delimited continuations i thought i understood continuations
12:51:23 <pera_> ski: absolutely, specially with a word like return that has quite a few meanings depending the context (call stack, statement, monad return, etc)
12:53:44 <ski> Inst : "but I can't actually pattern match on the contained data within my existential type, or rather, I have to treat it as generic" -- yes. exactly like a polymorphic function (e.g. `mystery :: forall a. Int -> [a] -> [a]') can't pattern-match on the values of the type variable `a', having to treat them as "black boxen". that type is, to `mystery' (and other operations (being polymorphic, or) *producing*
12:53:50 <ski> polymorphic values (values of type `forall a. ..a..') as output), abstract/forgotten/hidden/unknown/opaque/skolem
12:53:53 <ski> Inst : the same holds for operations *consuming* "abstracted" values as input (values of type `exists a. ..a..'. any values of the abstract/forgotten/hidden/unknown/opaque/skolem type `a' here act like black boxen, can only be interrogated via relevant callbacks (including type class methods, if available), just like in the polymorphic case)
12:54:44 → foul_owl joins (~kerry@185.219.141.164)
12:55:44 <ski> tomsmeding : s/forall a. ToHTML a => a/exists a. ToHTML a *> a/
12:58:26 <ski> Inst : "this is really a problem Lisps don't have, and Haskell does, ideally, what I want is the ability to toHTML template objects" -- meaning ?
12:59:05 <ski> pera_ : i don't think it's wrong to use the term "return", just saying that one should be a bit careful that one doesn't accidentally lean into or cause (or be afflicted by) misconceptions
12:59:16 <tomsmeding> ski: yes
13:00:19 <ski> @get-shapr
13:00:19 <lambdabot> shapr!!
13:00:57 <shapr> you called?
13:01:09 <ski> just saying hi :)
13:01:17 <shapr> hi ski! long time no see in person
13:01:47 <tomsmeding> (of course that's a builtin in lambdabot)
13:01:53 ski grins
13:02:19 <ski> you're back in the U.S., iirc. hope you're doing well
13:02:21 <shapr> I hosted lambdabot for the first seven years
13:02:34 <shapr> ski: yes, I've been back in the US since 2007
13:02:51 <ski> (mm, that's what i thought, but i haven't really been attempting to keep track)
13:02:56 <shapr> yeah, no worries
13:03:21 <ski> eldritchcookie : if you'd like, i could link you to two papers about CPS transformation
13:03:40 <haskellbridge> <e​ldritchcookie> please do
13:04:38 × bitdex quits (~bitdex@gateway/tor-sasl/bitdex) (Ping timeout: 260 seconds)
13:04:40 <ski> now, maybe they'd be somewhat dense for you .. i dunno how used you are to reading research papers. but hopefully you'll at least be able to get something out of them, specifically in this case the basics of the CPS transformation
13:05:02 <ski> (iirc the papers include some theorems and proofs which you can probably skip more or less)
13:05:30 → byorgey joins (~byorgey@155.138.238.211)
13:08:08 → meritamen joins (~meritamen@user/meritamen)
13:08:52 <ski> eldritchcookie : "Abstracting Control" in 1990-06, and "Representing Control: A Study of the CPS Transformation" in 1992-12, both by Andrzej Filinski,Olivier Danvy, at <http://hjemmesider.diku.dk/~andrzej/papers/>
13:09:15 → nickiminjaj joins (~nickiminj@user/laxhh)
13:09:46 × Maxdamantus quits (~Maxdamant@user/maxdamantus) (Ping timeout: 255 seconds)
13:10:00 <ski> btw, if you haven't seen the paper before, and you're not used to reading papers with type system stuff (although i can't recall offhand how much of that is in the above two papers), i can also suggest
13:10:25 <ski> @where polymorphic-type-inference
13:10:25 <lambdabot> "Polymorphic Type Inference" by Michael I. Schwartzbach in 1995-03 at <https://cs.au.dk/~mis/typeinf.p(s|df)>,<http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.57.1493>
13:11:12 <ski> simply because it goes over some basics that's usually not spelled out, and also because it does bring up a bunch of interesting things
13:15:22 <ski> also, the links at e.g. <https://web.archive.org/web/20180726144531/http://library.readscheme.org/> (in this case the continuations section) may also be interesting (<https://github.com/scheme-and-computer-science/library.readscheme.org/blob/master/page6.md> appears to be a separate archive of the papers on the site)
13:15:44 → zetef joins (~quassel@5.2.182.99)
13:16:08 → Maxdamantus joins (~Maxdamant@user/maxdamantus)
13:18:04 <ski> in any case, the Filinski & Danvy papers above do mention `shift' and `reset', as well as `call/cc'
13:19:04 <ski> eldritchcookie : you may also want to check out Oleg's site, specifically <https://okmij.org/ftp/continuations/>
13:22:13 <ski> eldritchcookie : from one POV, continuations are supposed to be an abstraction that represents a point of control, that you can *jump* to (with parameters/arguments), but there's no such thing as a return. from that perspective, they're like `jmp' in assembler languages. whereas functions are *called* (with some parameters), and *returns* a result back to the caller (the discovery/invention of the
13:22:19 <ski> subroutine, with explicit support for stacks, makes this correspond to `jsr'/`bsr'/`call' or similar, in assembler language)
13:24:57 <ski> eldritchcookie : from a typeful perspective, continuations are about negation, logically speaking. a continuation accepting an `Int' is like an "anti-`Int'" (kinda think of particle and anti-particle). in practice, in an expression-oriented language, such a continuation could be specified as the (dynamic/computational) *context* surrounding some particular (subexpression yielding an) `Int' value, e.g. the
13:25:03 <ski> dots context surrounding `6*7' in `..(6*7)'. that continuation could be assigned the type `Not Int'
13:25:10 × Maxdamantus quits (~Maxdamant@user/maxdamantus) (Remote host closed the connection)
13:26:13 <haskellbridge> <e​ldritchcookie> would it be better to say we have an Int in negative position so we can act as if we had an int?
13:26:38 <ski> from this perspective, a function of type `a -> b' can be seen as expressing a continuation of type `Not (a,Not b)' (a continuation accepting two parameters, one being of type `a', and the other being a "return address" (a continuation) that will (presumably) be called with a `b')
13:27:10 <ski> (note that, logically speaking (in classical logic), `A => B' (`A' implies `B'), is equivalent to `not (A and not B)'. this is not a coindicence)
13:29:31 <ski> .. and, at the assembler, or machine code, level, this is the basics of how subroutines, and functions, work. you pass some parameter(s) in some registers (or perhaps on a stack), and you also pass a *return address* (commonly on stack, but could be in a register as well). this closely adheres to the `Not (a,Not b)' picture of `a -> b'. this still ignores various issues about lifetime/extent (such as stack
13:29:37 <ski> allocation), and closing over the static/lexical environment (accessing non-local variables, "closures") ..
13:29:38 × nickiminjaj quits (~nickiminj@user/laxhh) (Quit: My MacBook has gone to sleep. ZZZzzz…)
13:30:00 <ski> "would it be better to say we have an Int in negative position" -- in which situation ?
13:30:40 <ski> .. anyway, from the above POV, continuations are a *more* fundamental concept than functions, functions being a derived concept, defined in terms of continuations
13:30:46 <ski> @where Io
13:30:46 <lambdabot> Raphael L. Levien's language with continuations as fundamental structure, described in his paper "Io: a new programming notation" (1989-09-10) at <http://dl.acm.org/citation.cfm?id=70931.70934> and
13:30:46 <lambdabot> in chapter 2 of Raphael A. Finkel's book `APLD', implementations `Amalthea',`Ganymede' - (perhaps you were looking for `@wiki Introduction to IO' ?)
13:31:01 <ski> is a language that is based on continuations as the basic primitive
13:32:09 <ski> (APLD is "Advanced Programming Language Design" by Raphael Finkel in 1996 at <https://web.archive.org/web/20150522052725if_/http://www.nondot.org/sabre/Mirrored/AdvProgLangDesign/>)
13:33:20 <shapr> Does anyone know if servant is both http 1.1 and http 2 ?
13:33:26 <ski> anyway .. denotational semantics tries to explain meaning of programming languages, by mapping phrases of programs into (traditional) mathematical structures .. and continuations are not a common structure that people consider in mathematics, whereas functions most definitely are
13:34:01 <dmj`> shapr: warp is http2
13:34:03 × koz quits (~koz@121.99.240.58) (Quit: ZNC 1.8.2 - https://znc.in)
13:34:10 <shapr> ah, and servant runs on top of warp
13:34:15 <shapr> dmj`: thanks!
13:35:32 × tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
13:35:48 <ski> eldritchcookie : this leads to the other POV here, namely *representing*/*encoding*/*simulating* continuations, via *functions*. instead of having `square :: Not (Int,Not Int)', you have `squareTupledCPS :: (Int,Int -> o) -> o' or `squareCurriedCPS :: Int -> (Int -> o) -> o', where we replace the continuations by functions returning a value of an (*arbitrary*, hence type variable) "answer" type, `o' (often
13:35:50 → Maxdamantus joins (~Maxdamant@user/maxdamantus)
13:35:54 <ski> `omega' in papers)
13:36:12 → koz joins (~koz@121.99.240.58)
13:38:32 <ski> (in terms of logic, this corresponds to embedding classical logic in what's called "minimal logic". if we replace `o' by a specific answer type like `Void' (having no defined value), then it becomes an embedding/translation into intuitionistic logic. the difference is that there's a polymorphic function `void :: Void -> a' allowing us to pretend a `Void' can give us a result of any type. in logical terms,
13:38:38 <ski> this corresponds to saying "this case is therefore impossible, and so we don't need to consider it further")
13:38:54 <ski> eldritchcookie : .. is this making any sense ?
13:38:54 × gorignak quits (~gorignak@user/gorignak) (Quit: quit)
13:39:53 <haskellbridge> <e​ldritchcookie> no, but i liked https://www.youtube.com/watch?v=TE48LsgVlIU&t=1s
13:40:14 <ski> what about my request for clarification above, then ?
13:42:21 → AlexZenon joins (~alzenon@94.233.240.255)
13:42:32 → AlexNoo joins (~AlexNoo@94.233.240.255)
13:42:32 <ski> (i guess i was focused for a while on attempting to give a "from the bottom up / first principles" general overview of what continuations and CPS are about, above. but people do learn best in different ways. perhaps you'd prefer starting from specific applications)
13:43:22 <haskellbridge> <e​ldritchcookie> o you mean the Int in negative position thing? well normally we have covariant types in positive position but when it gets under the arrow it becomes contravariant and it is in negative postion so in way we Gain a Int similar to how a function Char -> Char -> Int gives and Int
13:44:16 <haskellbridge> <e​ldritchcookie> negative means somewhere somehow we gain a value, positive mean somewhere somehow we consume a value
13:44:21 <ski> being in positive position means the same as being covariant in that position, yes. and ditto for negative & contravariant. just different ways to express the same thing
13:44:39 → fererrorocher joins (fererroroc@gateway/vpn/protonvpn/fererrorocher)
13:45:02 <haskellbridge> <e​ldritchcookie> yep
13:45:04 <kuribas> Does wreq support concurrency (green threads)?
13:46:22 <kuribas> I am doing REST call within a spock request, will they block between requests?
13:46:41 <ski> but it's important to understand that a type like `Char -> Chat -> Int' can be viewed from two directions. namely (a) from the direction of a producer/callee/implementor/"constructor", that therefore will get two `Char's, and will have to build an `Int' from them; resp. (b) from the direction of a consumer/caller/user/"de(con)structor", that will have to provide two `Char's to it, getting an `Int' back
13:46:54 <haskellbridge> <e​ldritchcookie> probably? it seems to me that the default API is synchronous
13:47:18 <ski> often when considering a type, we primarily have the producer perspective in mind, but the consumer perspective is just as important
13:48:07 <ski> (again, you could reduce this to whether you're considering the type in a positive or negative context .. although that kinda assumes that the "toplevel" context that you're considering is positive by definition)
13:48:21 <haskellbridge> <e​ldritchcookie> makes sense
13:49:09 <haskellbridge> <e​ldritchcookie> not necessarily it is positive from the caller's perspective which is the one that makes most sense to use if you are the caller
13:49:41 <ski> (when i'm e.g. talking about existentials, i try to directly make use of this duality, to spell out parallels between how `forall' is consumed and `exists' is produced, and similarly between how `forall' is produced and `exists' is consumed)
13:50:14 <ski> yea .. but we shift perspective between caller and callee, all the time, when programming subsystems
13:51:05 <ski> so .. i still don't really understand what you meant to ask, by "uld it be better to say we have an Int in negative position so we can act as if we had an int?"
13:52:20 × gawen quits (~gawen@user/gawen) (Quit: cya)
13:53:43 → gawen joins (~gawen@user/gawen)
13:56:08 <ski> .. so go back to delimited/composable/sub -continuations, for a moment, those are what happens when in `foo :: T -> (U -> o) -> o', you change `o' from being abstract, a type variable (quantified by the implicit `forall' at the top of the type signature), replacing it with some concrete type, say `Bool', or `IO ()' or `[a]' (say `forall'ing this `a'). what this allows you to do is to *not* call the
13:56:14 <ski> "continuation" (callback) *last*. iow, to *deviate* from "every call is a tail/last call", which otherwise is what CPS enforces. for this reason, this is also called nqCPS
13:56:39 <haskellbridge> <e​ldritchcookie> no idea but i think i get it now i was so confused because i didn't know what was delimited, prompt delimits the monadic action which is given as argument
13:57:12 <haskellbridge> <e​ldritchcookie> so control0 reifies from up to prompt
13:57:49 <ski> an example would be to write a `product' function in CPS, but allow it to abort what it's doing, whenever it sees a zero in its input. instead of `product :: [Integer] -> (Integer -> o) -> o', you get `product :: [Integer] -> (Integer -> Integer) -> Integer', with the important case forcing `o' to be `Integer' being `product (0:_) k = 0', ignoring the continuation `k'
13:59:20 <ski> this can also be used to incrementally generate partial results from the computation (like an "iterator"/"generator", more or less), or to send a request up to a surrounding handler, which may service that request and send back a response restarting the suspended computation. or doing other kinds of effects and stuff
14:02:04 <ski> eldritchcookie : yes. with `1 + reset (10 + shift (\c -> c (c 100)))', `c' will be bound to `\x -> reset (10 + x)' (with a `reset' in the body of the captured delimited continuation !, and `1 + reset (10 + shift (\c -> c (c 100)))' will reduce to `1 + reset (c (c 10))' (with the dynamically nearest `reset' surrounding the `shift' *surviving* the extraction of the delimited context around the `shift' call !)
14:03:02 <ski> the `control' & `prompt', and the `control0' versions, allow you to avoiding having these extra `reset's/`prompt's around
14:04:05 <ski> but doing that, afaik, requires some kind of "stack marking", and can't just be done through a simple CPS transform, which will instead just give you the `shift' & `reset' behavior
14:04:35 <ski> [| reset E |] = \k -> k ([| E |] (\x -> x))
14:06:11 <ski> [| shift (\k -> E) |] = \k -> ([| E |] (\x -> x))
14:08:39 <ski> is the CPS transform rules for those two constructs. we can clearly see that `shift' only passes a trivial continuation to `E' (corresponding to the `reset' lingering above); and that `reset' also passes the trivial continuation to `E', meaning that when we reach a `shift', it's as if the continuation `k' that it captures has a `reset' around it (can't access anything in the context outside that `reset')
14:11:48 <ski> (then one can introduce additional complexity, by having multiple levels of continuations, and even dynamically generating new such ones .. but the basics above only consider one level of continuations)
14:12:23 <ski> ("nqCPS" being short for "not-quite CPS")
14:13:34 × meritamen quits (~meritamen@user/meritamen) (Quit: Client closed)
14:18:30 × adanwan quits (~adanwan@gateway/tor-sasl/adanwan) (Quit: _)
14:18:47 → adanwan joins (~adanwan@gateway/tor-sasl/adanwan)
14:19:17 → tzh joins (~tzh@c-73-164-206-160.hsd1.or.comcast.net)
14:20:17 × rvalue quits (~rvalue@user/rvalue) (Read error: Connection reset by peer)
14:20:46 → rvalue joins (~rvalue@user/rvalue)
14:21:05 × kuribas quits (~user@ip-188-118-57-242.reverse.destiny.be) (Remote host closed the connection)
14:21:29 → kuribas joins (~user@ip-188-118-57-242.reverse.destiny.be)
14:26:36 <kuribas> How does concurrency works for something like sqlite? I suppose without threading it's use green threads, which means all calls are blocked?
14:27:20 <kuribas> Which is ok I suppose, since disk reads/writes are fast.
14:27:53 → meritamen joins (~meritamen@user/meritamen)
14:30:39 <tomsmeding> kuribas: be sure that you set SQLITE_CONFIG_SERIALIZED https://sqlite.org/c3ref/c_config_covering_index_scan.html
14:30:55 <tomsmeding> assuming you don't have perfect information about the compile-time config of your sqlite binary
14:34:36 <kuribas> tomsmeding: but I only need that if I use multiple OS threads, right?
14:34:50 <kuribas> Not with green threads?
14:36:01 × zetef quits (~quassel@5.2.182.99) (Ping timeout: 268 seconds)
14:41:25 × danse-nr3 quits (~danse-nr3@151.43.191.28) (Ping timeout: 246 seconds)
14:41:59 phma_ is now known as phma
14:42:43 <kuribas> More importantly, the http client (wrapped by Wreq) is non-blocking, right?
14:44:10 <kuribas> Otherwise a 4 second call to another api will block the server.
14:46:33 → nickiminjaj joins (~nickiminj@user/laxhh)
14:49:40 → zetef joins (~quassel@5.2.182.99)
14:50:41 → danse-nr3 joins (~danse-nr3@151.43.191.28)
14:52:58 × kuribas quits (~user@ip-188-118-57-242.reverse.destiny.be) (Remote host closed the connection)
14:53:28 → kuribas joins (~user@ip-188-118-57-242.reverse.destiny.be)
14:53:56 × nickiminjaj quits (~nickiminj@user/laxhh) (Quit: My MacBook has gone to sleep. ZZZzzz…)
15:07:14 × meritamen quits (~meritamen@user/meritamen) (Quit: Client closed)
15:08:05 × causal quits (~eric@50.35.88.207) (Quit: WeeChat 4.1.1)
15:13:10 → tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
15:17:56 → caconym4 joins (~caconym@user/caconym)
15:18:12 → random-jellyfish joins (~developer@2a02:2f04:11e:c600:2606:957e:b4af:5f60)
15:18:12 × random-jellyfish quits (~developer@2a02:2f04:11e:c600:2606:957e:b4af:5f60) (Changing host)
15:18:12 → random-jellyfish joins (~developer@user/random-jellyfish)
15:18:55 × caconym quits (~caconym@user/caconym) (Ping timeout: 260 seconds)
15:18:55 caconym4 is now known as caconym
15:19:09 → Guest10 joins (~Guest10@78.243.8.244)
15:21:48 × Guest10 quits (~Guest10@78.243.8.244) (Client Quit)
15:22:56 → Guest10 joins (~Guest10@78.243.8.244)
15:23:22 × Guest10 quits (~Guest10@78.243.8.244) (Client Quit)
15:27:49 <Inst> ski: lisps can codewalk into generated code and substitute wildly, doing this via FP is much harder
15:27:49 × lortabac quits (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Ping timeout: 268 seconds)
15:28:06 → nickiminjaj joins (~nickiminj@188.146.120.15)
15:28:06 × nickiminjaj quits (~nickiminj@188.146.120.15) (Changing host)
15:28:06 → nickiminjaj joins (~nickiminj@user/laxhh)
15:28:23 <Inst> the idea is that i want custom widget data types encapsulated by other widgets (probably of a differing type)
15:29:45 × cfricke quits (~cfricke@user/cfricke) (Quit: WeeChat 4.1.2)
15:30:28 × nickiminjaj quits (~nickiminj@user/laxhh) (Client Quit)
15:42:38 → nickiminjaj joins (~nickiminj@188.146.120.15)
15:42:38 × nickiminjaj quits (~nickiminj@188.146.120.15) (Changing host)
15:42:38 → nickiminjaj joins (~nickiminj@user/laxhh)
15:46:46 × nickiminjaj quits (~nickiminj@user/laxhh) (Client Quit)
15:49:58 → Square2 joins (~Square@user/square)
15:50:08 × jamesmartinez quits (uid6451@id-6451.helmsley.irccloud.com) (Quit: Connection closed for inactivity)
15:52:28 × kuribas quits (~user@ip-188-118-57-242.reverse.destiny.be) (Remote host closed the connection)
15:52:43 → kuribas joins (~user@ip-188-118-57-242.reverse.destiny.be)
15:53:08 × nschoe quits (~nschoe@2a01:e0a:8e:a190:8ccb:4735:e31a:8adf) (Quit: ZNC 1.8.2 - https://znc.in)
15:53:25 → nschoe joins (~nschoe@2a01:e0a:8e:a190:9eab:1f62:ace9:e44f)
15:53:31 × Square quits (~Square4@user/square) (Ping timeout: 246 seconds)
16:06:23 → nickiminjaj joins (~nickiminj@user/laxhh)
16:08:16 × nickiminjaj quits (~nickiminj@user/laxhh) (Client Quit)
16:10:56 × danse-nr3 quits (~danse-nr3@151.43.191.28) (Read error: Connection reset by peer)
16:11:12 → danse-nr3 joins (~danse-nr3@151.43.194.61)
16:12:34 × Square2 quits (~Square@user/square) (Ping timeout: 264 seconds)
16:12:44 → nickiminjaj joins (~nickiminj@user/laxhh)
16:13:17 × zetef quits (~quassel@5.2.182.99) (Ping timeout: 240 seconds)
16:16:12 × kuribas quits (~user@ip-188-118-57-242.reverse.destiny.be) (Quit: ERC (IRC client for Emacs 27.1))
16:30:03 <tomsmeding> @tell kuribas sure, you only need serialized sqlite if you have multiple OS threads, but who knows whether the GHC RTS will use multiple OS threads? Some user might pass +RTS -N2 to your program
16:30:03 <lambdabot> Consider it noted.
16:31:48 × danse-nr3 quits (~danse-nr3@151.43.194.61) (Ping timeout: 255 seconds)
16:40:05 <ski> Inst : "codewalk into generated code and substitute wildly" -- well, that's meta-programming (traversing and generating code sexps, quasi-quotation, and `eval' ior macros). if you want that in Haskell, seems you should look at Template Haskell ? .. or, use a shallow or deep embedding of a DSL, perhaps
16:40:41 <ski> Inst : "i want custom widget data types encapsulated by other widgets (probably of a differing type)" -- elaborate ?
16:40:51 × nickiminjaj quits (~nickiminj@user/laxhh) (Quit: My MacBook has gone to sleep. ZZZzzz…)
16:45:47 → nickiminjaj joins (~nickiminj@188.146.120.15)
16:45:47 × nickiminjaj quits (~nickiminj@188.146.120.15) (Changing host)
16:45:47 → nickiminjaj joins (~nickiminj@user/laxhh)
16:48:56 × nickiminjaj quits (~nickiminj@user/laxhh) (Client Quit)
16:49:34 <Inst> i want to have a widget value that can take another widget value within its data structure, but widget is a typeclass, not a single type
16:49:55 → sammelweis joins (~quassel@c-73-190-44-79.hsd1.mi.comcast.net)
16:50:21 <ski> so use `exists a. Widget a *> a' ?
16:52:33 <Inst> where did exists come from?
16:52:51 <ski> "can take another widget value within its data structure, but widget is a typeclass, not a single type"
16:53:26 → nickiminjaj joins (~nickiminj@188.146.120.15)
16:53:26 × nickiminjaj quits (~nickiminj@188.146.120.15) (Changing host)
16:53:26 → nickiminjaj joins (~nickiminj@user/laxhh)
16:53:33 <ski> you want to be able to store another widget inside your outer widget, regardless of what type the inner/former one has, as long as that type is an instance of the `Widget' type class, no ?
16:53:51 <geekosaur> you really do need to write actual Haskell at some point…
16:54:47 <ski> (when you do, you'll start to notice some drawbacks with this approach. which is fine, it's a trade off. but you can do this, if you want to)
16:55:09 <Inst> https://ghc.gitlab.haskell.org/ghc/doc/users_guide/exts/existential_quantification.html
16:55:13 → g00gler joins (uid125351@id-125351.uxbridge.irccloud.com)
16:55:18 <ski> yes ?
16:55:28 <Inst> geekosaur: ?
16:55:50 <geekosaur> "exists" and "*>" are syntax that ski wishes existed
16:56:02 <Inst> yeah that was what confused me :(
16:56:02 <ski> (fwiw, i consider the language extension `ExistentialQuantification' to be a misnomer. something like `ExistentialConstructors' would be more accurate, imho)
16:57:22 <ski> yes, i'm using pseudo-Haskell to communicate the idea, because, imho, it is clearer to communicate and discuss it, in that way, than to immediately jump to how to express/encode it in current Haskell (there's also two main ways in which one can do this, not just one. `ExistentialQuantification' is one. CPS using `Rank2Types' is the other)
16:57:43 <ski> if you're unclear about what i mean by `exists' and `*>', i'd be happy to elaborate
16:59:08 <ski> (or, i guess, possibly using `PolymorphicComponents' in place of `Rank2Types' .. nitpicking myself. but i'd think that's seldom useful, in practice)
16:59:58 <ncf> what's PolymorphicComponents?
17:00:20 <Inst> *> is more confusing
17:00:31 <ski> it's `data Foo = MkFoo (forall a. Bar a Int)', stuffing polymorphic things as components of data constructors
17:00:33 <EvanR> you heard of caleskell? will this is haski
17:00:33 <Inst> other than in the form >>
17:01:00 <EvanR> if => is like a function, *> is like a pair
17:01:12 <ski> (both `Rank2Types' and `PolymorphicComponents' are subsumed by `RankNTypes'. iirc, both implicitly enable the latter, nowadays. i'm just using these names, for extra precision)
17:01:44 <EvanR> => is waiting for a typeclass dictionary, *> is holding a typeclass dictionary already, on the left
17:01:49 <ncf> are you sure that's still a thing
17:02:06 <Inst> ah
17:02:10 → econo_ joins (uid147250@id-147250.tinside.irccloud.com)
17:02:34 <ncf> no PolymorphicComponents in https://downloads.haskell.org/ghc/latest/docs/users_guide/exts/table.html
17:02:36 <EvanR> and yeah it's not actual haskell
17:02:43 <EvanR> unfortunately
17:03:14 <ski> Inst : a value of type `Cxt => T' is a value such that, if there happens to be an instance `Cxt' in scope, then that can be (implicitly) provided to this value, so that you can use this value as having type `T'. to construct a value of type `Cxt => T', you're free to assume that the user/caller/consumer/de(con)structor of your value will (implicitly) provide an instance of `Cxt', so that you can refer to its
17:03:20 <ski> methods when computing your value of type `T'
17:05:23 <ski> Inst : correspondingly (dually), a value of type `Cxt *> T' is a value that encapsulates *both* a value of type `T', and also (implicitly) encapuslates (provides) an instance of `Cxt' to the user/caller/consumer/de(con)structor of the whole value. an implementor/callee/producer/constructor of a value of type `Cxt *> T' has to both (implicitly) provide an instance of `Cxt', and a value of type `T'
17:05:56 <Inst> ah i think that's what i'm missing
17:07:11 <ncf> (in one sentence, Cxt *> - is the left adjoint to Cxt => -)
17:07:54 <ski> Inst : in the dictionary-passing translation/implementation of type classes, type class constraints/contexts `Cxt' gets translated to corresponding data types, say `CxtDict' (e.g. `Eq a' would become `EqDict a', where `data EqDict a = MkEqDict { (==),(/=) :: a -> a -> Bool }'). then `Cxt => T' becomes `CxtDict -> T' (a function type, taking the dictionary for the constraint as input, returning the value of
17:08:00 <ski> type `T' as output), and `Cxt *> T' becomes `(CxtDict,T)' (a pair type, bundling the constraint dictionary with the value)
17:08:19 × dbaoty quits (~dbaoty@tptn-04-0838.dsl.iowatelecom.net) (Quit: Leaving.)
17:08:23 <ski> in short, yes, "`*>' is to `(,)', as `=>' is to `->'"
17:09:11 × ubert quits (~Thunderbi@2a02:8109:ab8a:5a00:5d4b:5ac:c6db:5974) (Remote host closed the connection)
17:09:38 <Inst> actually, i understand what you mean by that, i was just thinking 'why can't i find a good frontend edsl written in haskell', then i realize that just means DOM, and Reflex already exists
17:10:07 <EvanR> if you're playing (a,) then you can draw from the a pile to get an a, if you're playing a ->, you can discard an a
17:10:32 <ski> and to be complete, i guess i should say that a value of type `forall a. ..a..' (a polymorphic value) is a value such that the caller/consumer/user/de(con)structor gets to pick whichever type they want to use for `a', and the callee/producer/implementor/producer must be prepared to handle any actual type being used for `a', and so can't assume anything about it (can't even inquire about which type was chosen)
17:10:40 → euphores joins (~SASL_euph@user/euphores)
17:12:56 <ski> while, for a value of type `exists a. ..a..' (an "abstracted" value) is a value such that the callee/producer/implementor/constructor gets to pick whichever type they want to use for `a', and the caller/consumer/user/de(con)structor must be prepared to handle any actual type being used for `a', and so can't assume anything about it (can't even inquire about which type was chosen)
17:15:56 <ski> a function `foo :: Int -> exists a. Ord a *> (Map String a,Map a [a])' will pick some type `a', which may depend on the `Int' argument, such that the caller is guaranteed that the type is in `Ord', but otherwise knows nothing about it. all the `a's in the maps are of the same (unknown) type here, so can be compared to each other
17:17:36 <ski> if you instead used `bar :: String -> IO (Map String (exists a. Widget a *> a))', then not only can the type `a' chosen depend on both the `String' argument, and on the I/O interaction leading up to the monadic result; the `a's can be different for different `String' keys in the map (because the `exists' is inside `Map', rather than outside it)
17:17:45 <Inst> thanks for all the effort, i understand what you mean and how it's relevant to my concerns now
17:19:17 <ski> with `baz :: forall a. C a => T a -> exists b. D a b *> U a b', `b' can depend both on the type `a' (chosen by the caller), and the input of type `T a'. and the chosen/provided instance of `D a b' can depend on the given (by the caller) instance `C a'
17:21:06 <ski> if we want to express say `exists a. Ord a *> Map String a', then imagine if we could write
17:21:59 <ski> data SomeMap = MkSomeMap (exists a. Ord a *> Map String a)
17:22:14 <ski> this would mean that the data constructor has the following type signature
17:22:25 <ski> MkSomeMap :: (exists a. Ord a *> Map String a) -> SomeMap
17:22:59 → Kamuela joins (sid111576@id-111576.tinside.irccloud.com)
17:23:47 <ski> however, generally, `(exists a. ..a..) -> ...' is equivalent to `forall a. (..a.. -> ...)', and `(... *> ...) -> ...' is equivalent to `... => (... -> ...)' (compare with currying, how `(...,...) -> ...' is equivalent to `... -> ... -> ...')
17:23:53 <ski> therefore, this amounts to
17:24:06 <ski> MkSomeMap :: forall a. ((Ord a *> Map String a) -> SomeMap)
17:24:08 <ski> iow
17:24:20 <ski> MkSomeMap :: forall a. (Ord a => (Map String a -> SomeMap))
17:24:24 <ski> or just
17:24:28 <ski> MkSomeMap :: forall a. Ord a => Map String a -> SomeMap
17:24:34 <ski> without redundant brackets. or just
17:24:39 <ski> MkSomeMap :: Ord a => Map String a -> SomeMap
17:24:55 <ski> using implicit universal quantification of type variables at toplevel of type signatures
17:24:56 <Inst> Mhm :)
17:25:48 <ski> so, `MkSomeMap' is *polymorphic* (because it has a type `forall a. ..a..'), it's accept a `Map String a', for *any* type `a' the caller wants to use (as long as it's in the type class `Ord')
17:26:36 <ski> however, `a' here does not appear in the result type. that is what makes this data constructor "existential" (which is a figure of speech here, not an exact statement. it's the argument type, namely `exists a. Ord a *> Map String a', that's existential, if anything)
17:26:56 <ski> the *actual* syntax that the `ExistentialQuantification' extension (misnomer) gives you for this is
17:27:15 <ski> data SomeMap = forall a. Ord a => MkSomeMap (Map String a))
17:27:46 <ski> indicating that the `MkSomeMap' data constructor is polymorphic (the `forall'), specifically constrained polymorphic (the `=>')
17:28:04 <ski> if you use `GADTs', you can alternatively declare the same thing instead as
17:28:07 <ski> data SomeMap
17:28:09 <ski> where
17:28:14 <ski> MkSomeMap :: Ord a => Map String a -> SomeMap
17:28:17 <ski> if you prefer
17:29:16 <ski> to access the "existential", you must pattern-match on the `MkSomeMap' data constructor. your final result type can't depend on the hidden type `a' (and the associated `Ord a' constraint) that this pattern-matching brings into scope
17:29:43 <ski> and to return such a value (or store it in a data structure), you must wrap with with the data constructor `MkSomeMap'
17:30:03 <ski> so, whenever you intended `exists a. Ord a *> Map String a' in your original design, you will now instead write `MkSomeMap' in its place
17:30:34 <ski> this is the first approach to express/encode existentials
17:30:44 <Inst> ah, I see
17:30:47 → arjun joins (~arjun@user/arjun)
17:30:49 <ski> the second is, if you're trying to return `exists a. Ord a *> Map String a', like in
17:31:03 <ski> foobar :: Map String Fribble -> exists a. Ord a *> Map String a
17:31:31 × fererrorocher quits (fererroroc@gateway/vpn/protonvpn/fererrorocher) (Quit: WeeChat 4.2.1)
17:32:19 <ski> what you do is you exploit that any type `...' is equivalent to `forall o. (... -> o) -> o' (this is CPS, Continuation-Passing Style) (it also happens to be equivalent to `exists s. (s,s -> ...)', but i'll not use that logical equivalence atm)
17:32:26 <ski> so, we arrive at
17:32:46 <ski> foobarWith :: Map String Fribble -> forall o. ((exists a. Ord a *> Map String a) -> o) -> o
17:33:14 <ski> but, using the two equivalences that i mentioned first, above, this is amounts to
17:33:32 <ski> foobarWith :: Map String Fribble -> forall o. (forall a. Ord a => Map String a -> o) -> o
17:34:00 <ski> and, using that `... -> (forall a. ..a..)' is equivalent to `forall a. (... -> ..a..)', this becomes
17:34:08 <ski> foobarWith :: forall o. Map String Fribble -> (forall a. Ord a => Map String a -> o) -> o
17:34:11 <ski> or just
17:34:14 <ski> foobarWith :: Map String Fribble -> (forall a. Ord a => Map String a -> o) -> o
17:34:17 <ski> for short
17:35:32 <ski> so, what has happened is that, instead of directly returning the result of type `Map String a', for *some* (unknown/hidden/forgotten/abstract/opaque/skolem) type `a' (such that `Ord a'), we take an extra callback parameter (the continuation), and instead of returning the result, we pass it to the continuation (whose eventual result of type `o' we'll just return)
17:35:56 × igemnace quits (~ian@user/igemnace) (Quit: WeeChat 4.2.1)
17:36:39 <ski> this approach to encoding existentials tend to be more useful, when the caller wants to unpack the existential directly after the call. while the "existential constructor" approach is better when the caller does not want to unpack directly, or when you want to store the abstracted value, of existential type, in some data structure
17:36:47 <ski> Inst : and that's all
17:39:41 <Inst> I see.
17:41:54 <ski> (in practice, you'll of course jump directly to one or the other encoding, without going through the derivation steps, step by step. i only did that here, to help explain *why/how* these two encodings work, thinking of them as refactorings of the original pseudo-Haskell)
17:43:19 <ncf> so what problem were we solving using existential types today
17:43:40 <Inst> I don't remember either :)
17:43:49 <ncf> ah, polymorphic widgets
17:44:00 <ski> well, you were talking about widgets containing arbitrary widgets
17:44:16 <ski> (not polymorphic. abstracted)
17:44:48 <ncf> ...not not polymorphic? :)
17:44:58 <ski> ("there exists a widget of some type here")
17:45:19 ski passes ncf through DNS (Double-Negation Shift)
17:45:35 <Inst> what should I read to understand (more) of the basic Haskell type system, anyways?
17:45:59 <ski> well .. maybe the report ?
17:46:24 <ski> although .. i'd expect that a lot will make much more sense, if you practice what you're reading about, and experiment, play around, with it
17:46:49 <ncf> some lecture notes about system F, maybe
17:46:53 × machinedgod quits (~machinedg@d173-183-246-216.abhsia.telus.net) (Ping timeout: 268 seconds)
17:47:22 <ski> any intro textbook should explain higher-order functions, polymorphism, parameterized data types, type classes and instances
17:47:58 <ski> if you want to try to read a text about type systems, you could try
17:48:03 <ski> @where polymorphic-type-inference
17:48:04 <lambdabot> "Polymorphic Type Inference" by Michael I. Schwartzbach in 1995-03 at <https://cs.au.dk/~mis/typeinf.p(s|df)>,<http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.57.1493>
17:48:28 <Inst> tbh all my knowledge of Haskell's type system has been based on trial and error and finding out what blows up in my face
17:48:50 <ski> (the concrete syntax that is uses reminds more of Lisp (although not being sexpy), bu that's only a minor difference)
17:49:03 <ski> different people learn best in different ways
17:50:00 <Inst> wait, curious, technically
17:50:08 <Inst> lisp is s-expressions, algol is m-expressions
17:50:09 <Inst> haskell?
17:50:53 × mesaoptimizer quits (~mesaoptim@user/PapuaHardyNet) (Ping timeout: 268 seconds)
17:51:04 <EvanR> h expressions
17:51:33 <geekosaur> once you desugar layout, haskell is closer to algol than to lisp
17:53:10 <ski> (fwiw, DNS expresses that `forall n : Nat. not (not (P n))' entails `not not (forall n : Nat. P n)')
17:53:25 <ski> @where liskell
17:53:25 <lambdabot> a SExp syntax for Haskell, by therp : <http://clemens.endorphin.org/liskell> (broken),<https://web.archive.org/web/20081105133119/http://clemens.endorphin.org/liskell>,<http://clemens.endorphin.org/
17:53:25 <lambdabot> ILC07-Liskell-draft.pdf>,<https://web.archive.org/web/20120609122549/http://www.liskell.org/>
17:53:37 <Inst> yeah, i'm aware of it, as well as hackett
17:53:43 ski nods
17:55:04 <ski> Haskell's syntax is rather close to Miranda™'s. and not too different from ISWIM's (which used `where' in a similar fashion, iirc)
17:56:08 <ski> ISWIM was the imagined language used by Peter Landin in his seminal paper "The Next 700 Programming Language", if i'm not mistaken
17:57:18 × dcoutts quits (~duncan@cpc69402-oxfd27-2-0-cust903.4-3.cable.virginm.net) (Ping timeout: 255 seconds)
17:57:55 <ski> (and recursive defining equations (or go back further to recurrence relations), e.g. as used by Skolem or Gödel, and not too dissimilar to defining a function by multiple equations, pattern-matching, in Haskell)
18:02:54 <EvanR> n + k patterns get a lot of hate, but what more general idea was that driving toward
18:03:50 <EvanR> n+k isn't a data construction form, but does it have to be
18:04:21 <ski> pattern synonyms (more general than the current batch), which amounts to more or less the same as reverse modes for function (as in Mercury)
18:04:23 <EvanR> some languages let you put a string concatenation pattern
18:04:44 <ski> in Mercury, the function type declaration
18:05:01 <ski> :- func list(A) ++ list(A) = list(A).
18:05:16 <ski> has one (out of multiple) associated mode(s)
18:05:32 <ski> :- mode in ++ out = in is semidet.
18:06:04 <ski> expressing that if `Xs' is known and `Xs ++ Ys' is known, then that determines at most one value for `Ys', and therefore you can use that in pattern-matching like
18:06:20 <ski> foo([2,3,5,7] ++ Rest) = ..Rest..
18:06:37 <EvanR> reading that as "has one associated mode"
18:06:49 <ski> yea, the "usual" (forward) mode is
18:06:51 <Inst> EvanR: IIRC, ViewPatterns was descirbed as "N+K patterns are back!"
18:06:56 <ski> :- mode in ++ in = out is det.
18:07:21 <ski> (`det' means exactly one solution. `semidet' is at most one. `multi' is at least one. `nondet' is any number of solutions)
18:07:42 <ski> unfortunately, `ViewPatterns' can't take inputs
18:07:52 <ski> i'd like to be able to declare something like
18:08:24 <ski> pattern Append :: Eq a => [a] -> () => [a] -> [a]
18:09:19 <ski> pattern Append [ ] ys = ys
18:09:20 <ski> pattern Append (x:xs) ys = ((x ==) -> True) : Append xs ys
18:10:08 <ski> er, sorry, i meant of course `PatternSynonyms', not `ViewPatterns'
18:10:43 × pavonia quits (~user@user/siracusa) (Quit: Bye!)
18:11:01 <ski> where the general format of the type signature is `pattern PatSyn :: InCxt => InParm -> ... -> OutCxt => OutParm -> ... -> Scrut'
18:11:50 <ski> (and you can pattern-match as usual on the input parameters, with multiple defining equations, and guards if you want to)
18:21:11 → nickiminjaj_ joins (~nickiminj@user/laxhh)
18:25:07 × nickiminjaj quits (~nickiminj@user/laxhh) (Ping timeout: 260 seconds)
18:34:58 → dcoutts joins (~duncan@cpc69402-oxfd27-2-0-cust903.4-3.cable.virginm.net)
18:50:29 → waleee joins (~waleee@h-176-10-144-38.NA.cust.bahnhof.se)
18:53:24 × xal quits (~xal@mx1.xal.systems) ()
18:53:41 → xal joins (~xal@mx1.xal.systems)
19:01:13 <Inst> so, identity, maybe, nonempty, and list?
19:03:14 × euphores quits (~SASL_euph@user/euphores) (Quit: Leaving.)
19:04:04 × gmg quits (~user@user/gehmehgeh) (Remote host closed the connection)
19:04:46 × xal quits (~xal@mx1.xal.systems) ()
19:04:50 × g00gler quits (uid125351@id-125351.uxbridge.irccloud.com) (Quit: Connection closed for inactivity)
19:04:59 → gmg joins (~user@user/gehmehgeh)
19:05:15 × gmg quits (~user@user/gehmehgeh) (Remote host closed the connection)
19:05:50 → xal joins (~xal@mx1.xal.systems)
19:06:09 → gmg joins (~user@user/gehmehgeh)
19:07:05 × xal quits (~xal@mx1.xal.systems) (Client Quit)
19:10:37 → euphores joins (~SASL_euph@user/euphores)
19:11:40 → target_i joins (~target_i@user/target-i/x-6023099)
19:15:11 × gentauro quits (~gentauro@user/gentauro) (Read error: Connection reset by peer)
19:17:32 × nickiminjaj_ quits (~nickiminj@user/laxhh) (Read error: Connection reset by peer)
19:18:17 → nickiminjaj joins (~nickiminj@188.146.120.15)
19:18:17 × nickiminjaj quits (~nickiminj@188.146.120.15) (Changing host)
19:18:17 → nickiminjaj joins (~nickiminj@user/laxhh)
19:21:03 → gentauro joins (~gentauro@user/gentauro)
19:22:50 → xal joins (~xal@mx1.xal.systems)
19:24:36 → lortabac joins (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4)
19:24:54 × pera_ quits (~pera@8.29.109.183) (Quit: leaving)
19:35:06 × AlexZenon quits (~alzenon@94.233.240.255) (Ping timeout: 268 seconds)
19:37:03 <ski> Inst : you could think of them list that, sure
19:39:35 × tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
19:40:19 → fererrorocher joins (fererroroc@gateway/vpn/protonvpn/fererrorocher)
19:41:55 → AlexZenon joins (~alzenon@94.233.240.255)
19:51:11 → tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
19:52:04 × random-jellyfish quits (~developer@user/random-jellyfish) (Ping timeout: 255 seconds)
19:56:17 × nickiminjaj quits (~nickiminj@user/laxhh) (Quit: My MacBook has gone to sleep. ZZZzzz…)
19:57:28 × euphores quits (~SASL_euph@user/euphores) (Ping timeout: 246 seconds)
20:00:32 × fererrorocher quits (fererroroc@gateway/vpn/protonvpn/fererrorocher) (Quit: WeeChat 4.2.1)
20:07:19 → fererrorocher joins (fererroroc@gateway/vpn/protonvpn/fererrorocher)
20:08:03 → random-jellyfish joins (~developer@user/random-jellyfish)
20:08:50 → mima joins (~mmh@87-99-53-133.internetia.net.pl)
20:09:09 × mima quits (~mmh@87-99-53-133.internetia.net.pl) (Client Quit)
20:10:25 × mei quits (~mei@user/mei) (Remote host closed the connection)
20:10:38 × phma quits (~phma@host-67-44-208-169.hnremote.net) (Read error: Connection reset by peer)
20:10:55 → mei joins (~mei@user/mei)
20:11:34 → phma joins (phma@2001:5b0:211c:a48:b538:9e99:373e:ab2f)
20:12:42 × _ht quits (~Thunderbi@28-52-174-82.ftth.glasoperator.nl) (Quit: _ht)
20:13:37 → nickiminjaj joins (~nickiminj@user/laxhh)
20:19:13 × nickiminjaj quits (~nickiminj@user/laxhh) (Quit: My MacBook has gone to sleep. ZZZzzz…)
20:28:04 × tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
20:30:16 → nickiminjaj joins (~nickiminj@user/laxhh)
20:31:34 × xal quits (~xal@mx1.xal.systems) ()
20:33:46 × sammelweis quits (~quassel@c-73-190-44-79.hsd1.mi.comcast.net) (Quit: https://quassel-irc.org - Chat comfortably. Anywhere.)
20:42:07 × mmhat quits (~mmh@p200300f1c74dcfc3ee086bfffe095315.dip0.t-ipconnect.de) (Quit: WeeChat 4.2.1)
20:43:33 × lortabac quits (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Ping timeout: 268 seconds)
20:43:50 × nickiminjaj quits (~nickiminj@user/laxhh) (Quit: My MacBook has gone to sleep. ZZZzzz…)
20:44:12 → xal joins (~xal@mx1.xal.systems)
20:47:34 × xal quits (~xal@mx1.xal.systems) (Client Quit)
20:47:47 → nickiminjaj joins (~nickiminj@188.146.120.15)
20:47:47 × nickiminjaj quits (~nickiminj@188.146.120.15) (Changing host)
20:47:47 → nickiminjaj joins (~nickiminj@user/laxhh)
20:49:11 → tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
20:49:35 × nickiminjaj quits (~nickiminj@user/laxhh) (Client Quit)
20:52:54 → xal joins (~xal@mx1.xal.systems)
20:53:04 → mesaoptimizer joins (~mesaoptim@user/PapuaHardyNet)
20:55:59 → nickiminjaj joins (~nickiminj@user/laxhh)
20:59:29 × tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
20:59:55 × nickiminjaj quits (~nickiminj@user/laxhh) (Client Quit)
21:00:46 → nickiminjaj joins (~nickiminj@user/laxhh)
21:07:27 → machinedgod joins (~machinedg@d173-183-246-216.abhsia.telus.net)
21:08:21 → sprout_ joins (~quassel@84-80-106-227.fixed.kpn.net)
21:10:19 × sprout quits (~quassel@2a02-a448-3a80-0-7de0-65dd-3177-b6a5.fixed6.kpn.net) (Ping timeout: 260 seconds)
21:10:28 sprout_ is now known as sprout
21:12:10 × mei quits (~mei@user/mei) (Remote host closed the connection)
21:14:47 → mei joins (~mei@user/mei)
21:16:29 × machinedgod quits (~machinedg@d173-183-246-216.abhsia.telus.net) (Ping timeout: 252 seconds)
21:17:10 × michalz quits (~michalz@185.246.207.197) (Quit: ZNC 1.8.2 - https://znc.in)
21:17:28 → tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
21:21:55 → adanwan_ joins (~adanwan@gateway/tor-sasl/adanwan)
21:22:18 × adanwan_ quits (~adanwan@gateway/tor-sasl/adanwan) (Remote host closed the connection)
21:22:42 → adanwan_ joins (~adanwan@gateway/tor-sasl/adanwan)
21:23:02 × adanwan quits (~adanwan@gateway/tor-sasl/adanwan) (Ping timeout: 260 seconds)
21:26:03 → sawilagar joins (~sawilagar@user/sawilagar)
21:26:48 × gmg quits (~user@user/gehmehgeh) (Quit: Leaving)
21:40:42 × arjun quits (~arjun@user/arjun) (Quit: Quit!)
21:42:31 × tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
21:51:12 × myxos quits (~myxos@065-028-251-121.inf.spectrum.com) (Remote host closed the connection)
21:57:30 → tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
21:57:56 × target_i quits (~target_i@user/target-i/x-6023099) (Quit: leaving)
21:58:11 → Midjak joins (~MarciZ@82.66.147.146)
21:59:31 × dolio quits (~dolio@130.44.134.54) (Quit: ZNC 1.8.2 - https://znc.in)
22:01:03 → dolio joins (~dolio@130.44.134.54)
22:03:07 × dolio quits (~dolio@130.44.134.54) (Client Quit)
22:04:17 → dolio joins (~dolio@130.44.134.54)
22:07:31 × tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
22:08:12 → thegeekinside joins (~thegeekin@189.217.89.27)
22:08:32 × thegeekinside quits (~thegeekin@189.217.89.27) (Remote host closed the connection)
22:08:37 → kaskal joins (~kaskal@089144252117.atnat0061.highway.webapn.at)
22:08:51 × kaskal- quits (~kaskal@089144220117.atnat0029.highway.webapn.at) (Ping timeout: 255 seconds)
22:19:10 × kaskal quits (~kaskal@089144252117.atnat0061.highway.webapn.at) (Ping timeout: 264 seconds)
22:21:38 → yin joins (~yin@user/zero)
22:23:19 <lyxia> what's the option for GHC to print implicit arguments when printing types?
22:24:06 → kaskal joins (~kaskal@2001:4bb8:2d2:1257:60b1:1057:17df:5755)
22:24:28 <geekosaur> -fprint-explicit-foralls ?
22:25:10 <geekosaur> I think they bodged it in there, at least
22:26:59 <lyxia> found it, -fprint-explicit-kinds
22:27:45 × ystael quits (~ystael@user/ystael) (Ping timeout: 255 seconds)
22:28:02 <geekosaur> oh
22:29:46 <geekosaur> (the ghci run at https://downloads.haskell.org/ghc/9.8.1/docs/users_guide/exts/type_applications.html#inferred-vs-specified-type-variables seems to think -fprint-explicit-foralls is enough)
22:32:23 → Sgeo joins (~Sgeo@user/sgeo)
22:32:43 × random-jellyfish quits (~developer@user/random-jellyfish) (Ping timeout: 255 seconds)
22:32:47 → ddellacosta joins (~ddellacos@modemcable123.17-177-173.mc.videotron.ca)
22:35:02 mewjay is now known as cjay
22:35:29 → sadie_ joins (~sadie@c-76-155-235-153.hsd1.co.comcast.net)
22:35:47 × travgm quits (~travgm@fsf/member/travgm) (Ping timeout: 268 seconds)
22:37:08 <lyxia> ah, I meant implicit argument of applied type families. Like if I want to see the Nat in Proxy 0.
22:41:41 × sawilagar quits (~sawilagar@user/sawilagar) (Ping timeout: 240 seconds)
22:42:32 × Luj quits (~Luj@2a01:e0a:5f9:9681:114f:c45b:717e:86b) (Quit: Ping timeout (120 seconds))
22:42:50 → Luj joins (~Luj@2a01:e0a:5f9:9681:ae04:a455:8cc3:9377)
22:50:05 × mei quits (~mei@user/mei) (Remote host closed the connection)
22:52:30 → mei joins (~mei@user/mei)
22:53:55 × acidjnk_new quits (~acidjnk@p200300d6e714dc8721a8bc0199a4b6df.dip0.t-ipconnect.de) (Ping timeout: 272 seconds)
22:56:33 × germtoo quits (~quassel@user/mipsel3) (Ping timeout: 255 seconds)
23:02:27 × petrichor quits (~znc-user@user/petrichor) (Quit: ZNC 1.8.2 - https://znc.in)
23:03:08 × nickiminjaj quits (~nickiminj@user/laxhh) (Quit: Textual IRC Client: www.textualapp.com)
23:03:12 → petrichor joins (~znc-user@user/petrichor)
23:15:09 → jmdaemon joins (~jmdaemon@user/jmdaemon)
23:25:32 → jorj joins (~jorj@user/jorj)
23:37:43 → Tuplanolla joins (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi)
23:37:46 × xsarnik quits (xsarnik@lounge.fi.muni.cz) (Ping timeout: 268 seconds)
23:41:05 → xsarnik joins (xsarnik@lounge.fi.muni.cz)
23:55:30 × sadie_ quits (~sadie@c-76-155-235-153.hsd1.co.comcast.net) (Remote host closed the connection)
23:56:55 × ezzieyguywuf quits (~Unknown@user/ezzieyguywuf) (Ping timeout: 260 seconds)
23:58:15 → peterbecich joins (~Thunderbi@047-229-123-186.res.spectrum.com)
23:58:22 × Midjak quits (~MarciZ@82.66.147.146) (Quit: Leaving)
23:58:46 → ezzieyguywuf joins (~Unknown@user/ezzieyguywuf)
23:59:20 × peterbecich quits (~Thunderbi@047-229-123-186.res.spectrum.com) (Remote host closed the connection)

All times are in UTC on 2024-04-02.