Finally it's worth noting that the typed tagless approach was originally developed as a way to encode partial evaluation in typed languages: the first paper was "Finally Tagless, Partially Evaluated: Tagless Staged Interpreters for Simpler Typed Languages"
Conversation
This is all fabulous, thanks mate!
1
1
Idris 1 has some interesting stuff to do with partial evaluation - I'm unsure how these experiments went though: docs.idris-lang.org/en/latest/refe
1
1
3
Thanks, this is awesome. I had completely forgotten about this
1
Yeah, it's super interesting! I really want to see something like this explored more in the future, perhaps treating 'phase' as a partial order on types. Conor Mc Bride has mentioned this quite a few times. Seems like a nicer approach to C++, D, and Rust's const expressions.
1
1
Davies and Pfenning "A modal analysis of staged computation" develops a modal type theory for partial evaluation (allowing multiple stages) that might be exactly what you want.
1
1
Oooh, cool. Will check it out. I've been following along with and 's Context Constrained computation, and and 's Granule+coeffect stuff in the hope that there's something there that could be useful for this.
1
3
Part of the challenge (afaik) is not just adding that order on types, but also then combining it with other things in a sound way, like other effects/co-effects, and dependent types. Lots of cool work out there getting closer:
- github.com/granule-projec
- bentnib.org/context-constr
1
2
4
I kind of really appreciate all the work our university friends are doing in this area. It's really cool and important! But it's hard, and takes time. I'm pretty excited about being able to get my head around it though, once the dust starts to settle on it all. 🙂
1
3
Thanks! We have a graded generalisation of Davies and Pfenning's system sketched on paper. Just need the person power to work on the implementation and work out the details!
1
4
😱 Oh, so cool! You folks are amazing! Really would like to get up to speed with this stuff, and figure out how it relates to my work!
and I are working on a paper that has more details about the overall story. Ping me an email and we can send you a preprint when we are done!
4
5
Heh, I have one or two half finished emails to you on my computer 😅 - will definitely try to summon the courage up now! Big fan of the things that you’re trying to tackle.
1