Home liberachat/#haskell: Logs Calendar

Logs: liberachat/#haskell

←Prev  Next→
Page 1 .. 171 172 173 174 175 176 177 178 179 180 181 .. 17906
— 1,790,544 events total
2021-05-29 17:35:46 ← ecm parts (~user@103.88.87.15) ()
2021-05-29 17:36:12 × buggy quits (~buggy@user/smorgasbord) (Quit: Lost terminal)
2021-05-29 17:36:32 → Bartosz joins (~textual@24.35.90.211)
2021-05-29 17:36:51 → haskman joins (~haskman@223.190.19.0)
2021-05-29 17:37:04 → holy_ joins (~h01y_b4z0@2400:adc1:178:c800:9e45:76a9:57f2:1665)
2021-05-29 17:37:27 → sondre joins (~sondrelun@cm-84.212.100.140.getinternet.no)
2021-05-29 17:37:35 → v01d4lph4 joins (~v01d4lph4@user/v01d4lph4)
2021-05-29 17:37:59 → Erutuon joins (~Erutuon@71-34-10-193.mpls.qwest.net)
2021-05-29 17:41:07 → Kaiepi joins (~Kaiepi@nwcsnbsc03w-47-54-173-93.dhcp-dynamic.fibreop.nb.bellaliant.net)
2021-05-29 17:41:42 → niko joins (~niko@libera/staff/niko)
2021-05-29 17:42:36 → ddellacosta joins (~ddellacos@89.46.62.116)
2021-05-29 17:44:57 → sbmsr joins (~pi@2600:1700:63d0:4830::26)
2021-05-29 17:45:00 → monadlight joins (~chris@bras-vprn-nwmkon8540w-lp130-19-184-147-249-234.dsl.bell.ca)
2021-05-29 17:45:19 → lavaman joins (~lavaman@98.38.249.169)
2021-05-29 17:47:11 × ddellacosta quits (~ddellacos@89.46.62.116) (Ping timeout: 265 seconds)
2021-05-29 17:47:19 → favonia joins (~favonia@user/favonia)
2021-05-29 17:47:58 → lieven joins (~mal@ns2.wyrd.be)
2021-05-29 17:49:27 × lavaman quits (~lavaman@98.38.249.169) (Ping timeout: 245 seconds)
2021-05-29 17:49:48 → maralorn[m] joins (~maralorn@2001:470:69fc:105::251)
2021-05-29 17:51:16 → srid[m] joins (~sridmatri@2001:470:69fc:105::1c2)
2021-05-29 17:51:36 × fizbin quits (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net) (Remote host closed the connection)
2021-05-29 17:52:26 → LukeHoersten joins (~LukeHoers@user/lukehoersten)
2021-05-29 17:55:38 × Arsen quits (~arsen@fosshost/volunteer/ArsenArsen) (Quit: Quit.)
2021-05-29 17:55:55 → Arsen joins (~arsen@fosshost/volunteer/ArsenArsen)
2021-05-29 17:58:34 → ddellacosta joins (~ddellacos@86.106.121.86)
2021-05-29 17:59:15 × HarveyPwca quits (~HarveyPwc@2601:246:c180:a570:29df:3b00:ad0e:3a06) (Quit: Leaving)
2021-05-29 17:59:54 → fendor joins (~fendor@178.165.129.15.wireless.dyn.drei.com)
2021-05-29 18:00:53 <Bartosz> I'm trying to understand the idea of tagless final encoding. They always say that tagless can be done without GADTs. So I assume that using GADTs solves the problem too. The functions they define are just GADT constructors, aren't they?
2021-05-29 18:00:54 <shiraeeshi> ecm: "The book of monads" by Alejandro Serrano Mena
2021-05-29 18:01:05 → HarveyPwca joins (~HarveyPwc@2601:246:c180:a570:29df:3b00:ad0e:3a06)
2021-05-29 18:01:24 <geekosaur> ecm left
2021-05-29 18:01:38 <shiraeeshi> oh, ok
2021-05-29 18:02:39 → vgtw joins (~vgtw@c-9164205c.07-348-756d651.bbcust.telenor.se)
2021-05-29 18:03:17 <shiraeeshi> Bartosz: "The functions they define are just GADT constructors, aren't they?" - who are "they"?
2021-05-29 18:03:18 × ddellacosta quits (~ddellacos@86.106.121.86) (Ping timeout: 264 seconds)
2021-05-29 18:03:36 <Bartosz> Kiselyov et al
2021-05-29 18:03:59 → wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net)
2021-05-29 18:04:06 × monadlight quits (~chris@bras-vprn-nwmkon8540w-lp130-19-184-147-249-234.dsl.bell.ca) (Ping timeout: 268 seconds)
2021-05-29 18:04:30 × HarveyPwca quits (~HarveyPwc@2601:246:c180:a570:29df:3b00:ad0e:3a06) (Client Quit)
2021-05-29 18:04:59 → HarveyPwca joins (~HarveyPwc@2601:246:c180:a570:29df:3b00:ad0e:3a06)
2021-05-29 18:05:20 × favonia quits (~favonia@user/favonia) (Ping timeout: 268 seconds)
2021-05-29 18:05:49 × blurgy quits (~blurgy@blurgy.xyz) (Quit: Quit: Aliens invaded Earth)
2021-05-29 18:06:25 <Bartosz> edwardk : is that right?
2021-05-29 18:06:42 × tromp quits (~textual@dhcp-077-249-230-040.chello.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
2021-05-29 18:07:19 <siraben> Bartosz: tagless final encoding has better compositional properties
2021-05-29 18:07:37 <siraben> in the paper there's an example of MulSYM and ExpSYM
2021-05-29 18:07:46 <siraben> you can combine them to something like, x = add (lit 3) (mul (lit 3) (lit 5))
2021-05-29 18:08:02 <siraben> then the typeclass constraint on x would be, (ExpSYM a, MulSYM a) => a
2021-05-29 18:08:13 <siraben> notice that this would not typecheck with GADTs
2021-05-29 18:08:16 → blurgy joins (~blurgy@blurgy.xyz)
2021-05-29 18:08:16 <Bartosz> But can you do the same with GADT?
2021-05-29 18:08:21 ← blurgy parts (~blurgy@blurgy.xyz) ()
2021-05-29 18:08:24 → blurgy joins (~blurgy@blurgy.xyz)
2021-05-29 18:08:32 ← blurgy parts (~blurgy@blurgy.xyz) ()
2021-05-29 18:09:03 <siraben> Let's say you did, data ExpSYM a where Add :: ExpSYM Int → ExpSYM Int → ExpSYM Int
2021-05-29 18:09:08 <Bartosz> Aren't these just smart constructors?
2021-05-29 18:09:14 <siraben> and Lit :: Int → ExpSYM Int
2021-05-29 18:09:34 <siraben> data MulSYM a where Mul :: MulSYM Int → MulSYM Int → MulSYM Int
2021-05-29 18:09:40 <siraben> Add (Lit 3) (Mul (Lit 3) (Lit 5)) would not typecheck
2021-05-29 18:10:27 <siraben> So, while it's basically equivalent with GADTs for a single typeclass, the ability to freely combine things in tagless-final encoding is one of the advantages
2021-05-29 18:11:25 → xfc83e joins (~xfc83e@178.44.133.16)
2021-05-29 18:11:37 × xfc83e quits (~xfc83e@178.44.133.16) (K-Lined)
2021-05-29 18:11:56 <Bartosz> I was just reading this blog post, where the guy points out that tagless final has nothing to do with typeclasses. https://www.foxhound.systems/blog/final-tagless/
2021-05-29 18:12:39 <Bartosz> Ben Levy wrote it
2021-05-29 18:13:15 × Kaiepi quits (~Kaiepi@nwcsnbsc03w-47-54-173-93.dhcp-dynamic.fibreop.nb.bellaliant.net) (Remote host closed the connection)
2021-05-29 18:13:20 <siraben> Kiselyov expresses it through typeclasses, I'm only familiar with his presentation of GADTs
2021-05-29 18:13:24 <siraben> Oops I mean, presentation of tagless-final
2021-05-29 18:13:26 → smitop joins (uid328768@user/smitop)
2021-05-29 18:13:58 <cdsmith> So basically we're just saying that you're using the type class (or equivalent mechanism) to postpone the choice of model, meaning you can define your x = add (lit 3) (mul (lit 3) (lit 5)) in one place, and maybe instantiate the type with a GADT in one place, or a different model somewhere else?
2021-05-29 18:14:12 <siraben> Bartosz: I only see a single sort going on in that blog post; SqlExpr
2021-05-29 18:15:02 <siraben> In the little example I gave, there's two different kinds of expressions
2021-05-29 18:15:53 <cdsmith> Sure, but eventually, a has to be SOMETHING!
2021-05-29 18:16:31 → ddellacosta joins (~ddellacos@89.46.62.108)
2021-05-29 18:16:39 <cdsmith> Sorry, I think I was jumping in and confusing things.
2021-05-29 18:16:44 <siraben> Chris Smith: exactly, "choice of model" is a more mathematical way to put it
2021-05-29 18:16:49 → lu joins (~lu@user/lu)
2021-05-29 18:16:53 × henrylaxen quits (~user@177.239.36.179) (Remote host closed the connection)
2021-05-29 18:17:09 × Guest962 quits (~Guest9@103.240.169.6) (Ping timeout: 265 seconds)
2021-05-29 18:17:20 → favonia joins (~favonia@user/favonia)
2021-05-29 18:18:05 <Bartosz> It seems to me that "tagless" and "final" are specific terms. It so happens that tagless final allows the use of typeclasses to postpone the interpretation.
2021-05-29 18:18:36 × werneta quits (~werneta@mobile-166-176-59-138.mycingular.net) (Ping timeout: 244 seconds)
2021-05-29 18:18:41 <siraben> it's like in mathematical logic, you can add more and more terms and equations for your logical theory, which possibly constrains the number of models that satisfy that theory
2021-05-29 18:19:28 → Guest997 joins (~Guest9@103.240.169.6)
2021-05-29 18:19:37 → tromp joins (~textual@dhcp-077-249-230-040.chello.nl)
2021-05-29 18:20:08 → ku joins (~ku@2601:280:c780:7ea0:a9c5:d391:6107:54ae)
2021-05-29 18:20:37 → kus joins (~ku@2601:280:c780:7ea0:4047:2728:61af:6d22)
2021-05-29 18:21:16 <Bartosz> I'm just wondering if the use of GADTs is considered "tagging" the result. My understanding is that GADT tags are only used by the typechecker.
2021-05-29 18:21:18 × ddellacosta quits (~ddellacos@89.46.62.108) (Ping timeout: 264 seconds)
2021-05-29 18:22:32 × dyeplexer quits (~dyeplexer@user/dyeplexer) (Remote host closed the connection)
2021-05-29 18:23:13 × talismanick quits (~user@2601:644:8502:d700::94c9) (Ping timeout: 272 seconds)
2021-05-29 18:23:37 × wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 245 seconds)
2021-05-29 18:23:52 <shiraeeshi> siraben: why did you create GADTs like that? How about something like this (it's not even a GADT, just a regular data):
2021-05-29 18:23:55 <shiraeeshi> data Exp where Add {a :: Exp, b :: Exp}; Mult {a :: Exp, b :: Exp}
2021-05-29 18:24:02 × Guest997 quits (~Guest9@103.240.169.6) (Ping timeout: 245 seconds)
2021-05-29 18:24:08 <siraben> the point is that you can extend it post-hoc
2021-05-29 18:24:12 <siraben> without recompiling old code
2021-05-29 18:24:18 <siraben> the tagless-final paper talks about this
2021-05-29 18:24:27 × ku quits (~ku@2601:280:c780:7ea0:a9c5:d391:6107:54ae) (Ping timeout: 245 seconds)
2021-05-29 18:24:46 <siraben> if you added a new case to Exp, then you'd have to go along everywhere you destructed an Exp and handle the new case
2021-05-29 18:25:02 <siraben> with this, the old code that uses values of type (ExpSYM a) => a stay as such
←Prev  Next→
Page 1 .. 171 172 173 174 175 176 177 178 179 180 181 .. 17906

All times are in UTC.