They do! e.g. there seem to be quite a few Scheme partial evaluators (I'm no expert)
Conversation
Partial evaluators for typed languages seem rarer. Duncan Coutts mentions citeseerx.ist.psu.edu/viewdoc/downlo (pdf) issues with reencoding types. The cogen approach offers a viable alternative.
1
1
But see also Scala's Lightweight Modular Staging.
1
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"
2
1
5
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
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
Show replies