Logs: liberachat/#haskell
| 2021-05-29 18:25:08 | <siraben> | with tagless-final* |
| 2021-05-29 18:25:16 | <Bartosz> | You either need a parameterized data type or a GADT to handle Int and Bool expressions |
| 2021-05-29 18:25:23 | <siraben> | and new code can freely combine it with MulSYM |
| 2021-05-29 18:25:35 | <siraben> | Right, another alternative is to use parametrization over a functor, say |
| 2021-05-29 18:25:52 | <siraben> | data Exp f a where Add :: Exp (f Int) → Exp (f Int) |
| 2021-05-29 18:25:55 | → | beka joins (~beka@104.193.170-254.PUBLIC.monkeybrains.net) |
| 2021-05-29 18:26:00 | <siraben> | Add :: Exp (f Int) → Exp (f Int) → Exp (f Int) |
| 2021-05-29 18:26:07 | <siraben> | no idea if it will work, just a thought |
| 2021-05-29 18:26:50 | <siraben> | Bartosz: the paper also talks about disadvantages of tagless-final, including things like deforestation and fusion are not so well studied (and I believe GHC is not going to do such things, so you'll incur quite a bit of penalty if you finally encode everything) |
| 2021-05-29 18:27:25 | <Bartosz> | I think the idea is that you can have an "extensible GADT" if you define a parameterized data type and separately a bunch of smart constructors. If you combine these smart constructors into a GADT, you lose extensibility. |
| 2021-05-29 18:27:44 | <siraben> | here's a blog post I wrote that uses tagless final to express an AST for a language that can be re-interpreted under different contexts (models) https://siraben.github.io/2020/02/26/translating_cl.html |
| 2021-05-29 18:28:07 | <siraben> | Bartosz: right, another one is allowing reinterpretation of an AST just by type hints |
| 2021-05-29 18:28:11 | × | kus quits (~ku@2601:280:c780:7ea0:4047:2728:61af:6d22) (Quit: Leaving) |
| 2021-05-29 18:28:21 | <siraben> | if you have instance ExpSYM Int, then eval just becomes id @Int |
| 2021-05-29 18:28:29 | → | ku joins (~ku@2601:280:c780:7ea0:4047:2728:61af:6d22) |
| 2021-05-29 18:29:19 | → | pavonia joins (~user@user/siracusa) |
| 2021-05-29 18:30:17 | <Bartosz> | Another question: what's the meaning of initial and final for these EDSLs? What is it that's initial or final? |
| 2021-05-29 18:30:18 | × | myShoggoth quits (~myShoggot@97-120-89-117.ptld.qwest.net) (Ping timeout: 264 seconds) |
| 2021-05-29 18:30:53 | <dminuoso> | http://okmij.org/ftp/tagless-final/course/lecture.pdf covers these terms right in the introduction |
| 2021-05-29 18:31:14 | <siraben> | Yep, that's the paper |
| 2021-05-29 18:31:21 | <siraben> | Bartosz: I highly suggest that pdf link, it's very readable |
| 2021-05-29 18:31:32 | × | holy_ quits (~h01y_b4z0@2400:adc1:178:c800:9e45:76a9:57f2:1665) (Ping timeout: 245 seconds) |
| 2021-05-29 18:31:57 | × | LukeHoersten quits (~LukeHoers@user/lukehoersten) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 2021-05-29 18:32:01 | <Bartosz> | Thanks. I think I've seen it before, but already forgot. |
| 2021-05-29 18:32:27 | → | bfrk joins (~Thunderbi@200116b8456a1f00d8d08c49fac857df.dip.versatel-1u1.de) |
| 2021-05-29 18:32:32 | <dminuoso> | Bartosz: Also "Finally tagless, partially evaluated: Tagless staged interpreters for simpler typed language" by Carette, Kiselyov and Shan. |
| 2021-05-29 18:32:55 | <dminuoso> | Which is the original paper I think |
| 2021-05-29 18:33:01 | <Bartosz> | Yes, I've seen it. |
| 2021-05-29 18:33:26 | → | ddellacosta joins (~ddellacos@86.106.121.74) |
| 2021-05-29 18:33:28 | <Bartosz> | Unfortunatley it's in ML |
| 2021-05-29 18:35:15 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 2021-05-29 18:35:33 | <Bartosz> | I guess the key is that a data constructor is a function, but a function is not necessarily a data constructor. |
| 2021-05-29 18:35:37 | <dminuoso> | Bartosz: Reading some other parts, I think the word "final" is very informal and carries no exact notion. A relationship to "initial" from category theory is possible. |
| 2021-05-29 18:36:01 | <dminuoso> | But Oleg seems to not elaborate on it very much |
| 2021-05-29 18:37:07 | → | jco joins (~jco@c83-248-173-38.bredband.tele2.se) |
| 2021-05-29 18:37:36 | <Bartosz> | It could be that initial means the language you're embedding; and final, the language you're embedding it into (like Haskell, in this case, or ML). |
| 2021-05-29 18:37:56 | <dminuoso> | Well in the original paper Oleg says: |
| 2021-05-29 18:38:01 | × | ddellacosta quits (~ddellacos@86.106.121.74) (Ping timeout: 268 seconds) |
| 2021-05-29 18:38:04 | <dminuoso> | (Or presumably Oleg does) |
| 2021-05-29 18:38:24 | → | boxscape joins (~boxscape@user/boxscape) |
| 2021-05-29 18:38:32 | <dminuoso> | "We call this approach final (in contrast to initial), because we represent each object term not by its abstract syntax but by its denotation in a semantic algebra." |
| 2021-05-29 18:40:59 | × | wallymathieu quits (~wallymath@81-234-151-21-no94.tbcn.telia.com) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 2021-05-29 18:44:50 | × | tromp quits (~textual@dhcp-077-249-230-040.chello.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2021-05-29 18:45:28 | × | ixlun quits (~user@109.249.184.235) (Ping timeout: 244 seconds) |
| 2021-05-29 18:45:44 | → | Gjestefest joins (~Gjestefes@81.191.174.68) |
| 2021-05-29 18:46:22 | ← | Gjestefest parts (~Gjestefes@81.191.174.68) () |
| 2021-05-29 18:47:53 | × | favonia quits (~favonia@user/favonia) (Ping timeout: 268 seconds) |
| 2021-05-29 18:50:17 | × | lu quits (~lu@user/lu) (Ping timeout: 245 seconds) |
| 2021-05-29 18:51:04 | <Bartosz> | I think I see it. It's like defining a list: you can define it as a recursive data type, or you can say it's a higher order function (fold) that maps an algebra to a value. |
| 2021-05-29 18:51:23 | <dminuoso> | I guess |
| 2021-05-29 18:52:02 | → | ddellacosta joins (~ddellacos@86.106.121.30) |
| 2021-05-29 18:52:08 | ski | . o O ( `mu r. ..r.. = forall r. (..r.. -> r) -> r' ) |
| 2021-05-29 18:52:21 | → | tehStickMan joins (~tehStickM@37.98.248.234) |
| 2021-05-29 18:52:25 | × | tehStickMan quits (~tehStickM@37.98.248.234) (K-Lined) |
| 2021-05-29 18:52:41 | <Bartosz> | He even compares interpreting to folding |
| 2021-05-29 18:53:04 | <Bartosz> | Yes, exactly |
| 2021-05-29 18:54:23 | <Bartosz> | Something called Bohm Baraducci representation? |
| 2021-05-29 18:55:24 | <shachaf> | You can define data types as their folds, or codata types (I guess people would say) as their unfolds. |
| 2021-05-29 18:56:19 | × | ddellacosta quits (~ddellacos@86.106.121.30) (Ping timeout: 244 seconds) |
| 2021-05-29 18:56:26 | × | taeaad quits (~taeaad@user/taeaad) (Quit: ZNC 1.7.5+deb4 - https://znc.in) |
| 2021-05-29 18:57:04 | ski | . o O ( `nu s. ..s.. = exists s. (s,s -> ..s..)' ) |
| 2021-05-29 18:57:24 | → | favonia joins (~favonia@user/favonia) |
| 2021-05-29 18:57:29 | → | Guest31_ joins (~textual@cpc146410-hari22-2-0-cust124.20-2.cable.virginm.net) |
| 2021-05-29 18:57:36 | → | taeaad joins (~taeaad@user/taeaad) |
| 2021-05-29 18:58:40 | <Rembane> | The eager pattern matching parts of my brain wants to talk about recursion schemes and mtl, do they fit into these final tagless encodings in some way? |
| 2021-05-29 18:59:10 | <Bartosz> | data Mu f = Mu (forall a. Algebra f a -> a) |
| 2021-05-29 18:59:10 | <dminuoso> | Rembane: mtl-style is tagless final encoding. :) |
| 2021-05-29 19:00:03 | <Rembane> | dminuoso: Sweet! :) |
| 2021-05-29 19:00:08 | <monochrom> | Classes like MonadState are examples. |
| 2021-05-29 19:03:10 | <Bartosz> | @ski : data Nu f = forall a. Nu (a -> f a, a) |
| 2021-05-29 19:03:10 | <lambdabot> | Maybe you meant: wiki src ask |
| 2021-05-29 19:05:22 | → | jneira joins (~jneira@166.red-81-39-172.dynamicip.rima-tde.net) |
| 2021-05-29 19:05:42 | × | pbrisbin quits (~patrick@pool-72-92-38-164.phlapa.fios.verizon.net) (Ping timeout: 245 seconds) |
| 2021-05-29 19:05:45 | → | werneta joins (~werneta@mobile-166-176-56-255.mycingular.net) |
| 2021-05-29 19:06:16 | <Bartosz> | It's called Church/B ̈ohm/Berarducci encoding |
| 2021-05-29 19:08:07 | <Bartosz> | Oleg says: the non-extensible final encoding is equivalent to the Church/B ̈ohm/Berarducci encoding of the data type representing the embedded language |
| 2021-05-29 19:09:14 | <Bartosz> | But tagless final is more general, because it holds for higher-order typed languages. |
| 2021-05-29 19:10:24 | → | ddellacosta joins (~ddellacos@86.106.121.117) |
| 2021-05-29 19:11:07 | × | werneta quits (~werneta@mobile-166-176-56-255.mycingular.net) (Ping timeout: 245 seconds) |
| 2021-05-29 19:14:30 | × | pretty_dumm_guy quits (trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655) (Quit: WeeChat 3.2-dev) |
| 2021-05-29 19:14:52 | × | ddellacosta quits (~ddellacos@86.106.121.117) (Ping timeout: 245 seconds) |
| 2021-05-29 19:17:58 | → | Las[m] joins (~lasmatrix@2001:470:69fc:105::74e) |
| 2021-05-29 19:18:32 | → | pbrisbin joins (~patrick@pool-72-92-38-164.phlapa.fios.verizon.net) |
| 2021-05-29 19:19:36 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 2021-05-29 19:20:15 | × | river quits (~river@tilde.team/user/river) (Quit: Leaving) |
| 2021-05-29 19:23:44 | → | ixlun joins (~user@109.249.184.235) |
| 2021-05-29 19:23:55 | <dminuoso> | glguy: By the way, you asked about any rough edges with config-schema. One thing that has been bothering me slightly, is that I have much less ability to attach information for documentation purposes similarly to how I can mappend into an option in optparse-applicative |
| 2021-05-29 19:26:13 | <dminuoso> | For example, I'd like to do something like `describe "Launch a nuclear missile, stopping the peace" (atomSpec "launchMissile" $> CmdLaunchMissile) <!> describe "Go to sleep" (atomSpec "sleep" $> CmdSleep)` to describe what values of an enum could do |
| 2021-05-29 19:27:45 | <shiraeeshi> | "We call this approach final (in contrast to initial), because we represent each object term not by its abstract syntax but by its denotation in a semantic algebra." |
| 2021-05-29 19:27:51 | <shiraeeshi> | what's final about that? |
| 2021-05-29 19:27:52 | → | raehik joins (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) |
| 2021-05-29 19:28:07 | → | ddellacosta joins (~ddellacos@89.46.62.44) |
| 2021-05-29 19:28:12 | × | rahguzar quits (~rahguzar@dynamic-adsl-84-220-228-254.clienti.tiscali.it) (Ping timeout: 266 seconds) |
| 2021-05-29 19:28:12 | × | Erutuon quits (~Erutuon@71-34-10-193.mpls.qwest.net) (Ping timeout: 245 seconds) |
| 2021-05-29 19:28:34 | → | danso joins (~danso@23-233-111-52.cpe.pppoe.ca) |
| 2021-05-29 19:28:48 | <shiraeeshi> | I think I get it: it's just a silly wordplay |
| 2021-05-29 19:31:19 | × | Bartosz quits (~textual@24.35.90.211) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 2021-05-29 19:31:32 | → | lavaman joins (~lavaman@98.38.249.169) |
| 2021-05-29 19:32:29 | × | curiousgay quits (~AdminUser@178.217.208.8) (Ping timeout: 244 seconds) |
| 2021-05-29 19:32:58 | → | Bartosz joins (~textual@24.35.90.211) |
All times are in UTC.