reminder to decipher what this means in practice (or just look at the impl of @rob_rix's lang)https://twitter.com/rob_rix/status/1069311822623371264 …
-
-
Replying to @evertedsphere @mrkgrnao
So the term language of a lambda calculus is just abstraction, application, variables. It’s dependently typed so let’s throw in pi types & * too. But real languages have modules and imports and declarations and datatypes and all these other things which aren’t lambda terms.
1 reply 0 retweets 2 likes -
I’m thinking those things should be the language for the elaborator. `module` would be a command to start a namespace, declarations would extend the env & context, datatype declarations can be elaborated into lambda encodings, etc.
2 replies 0 retweets 0 likes -
-
Replying to @evertedsphere @mrkgrnao
Yeah, like, I think it’s not a really very novel (and maybe even interesting!) idea, but it’s always interesting to me how much research ends sharply at lambda terms.
1 reply 0 retweets 0 likes -
I’m also thinking about the Elaborator Reflection paper: https://dl.acm.org/citation.cfm?doid=2951913.2951932 … tho I’m not sure I understand it yet.
2 replies 0 retweets 1 like -
What you describe sounds very much in the spirit of elaborator reflection, yes.
1 reply 0 retweets 2 likes -
i havent been following blodwen, but is it true that a goal is to have a smaller core and do more implementation with with elab reflection?
2 replies 0 retweets 0 likes
I seriously considered that, and I think it's a good way to go, but in the end I decided there was enough to worry about already!
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.