Question for PL/TT Twitter:
Does anyone know of any prior art in terms of extracting something like Martin-Löf Type Theory (non-cumulative, with one universe, kind of like in The Little Typer) to something like System Fω with lifted terms and types?
Conversation
This is part of a compilation process where I want to preserve most of the types in my target language, and it's ok if not everything can be translated initially. I'll be converting things like type level case expressions to tagged unions for example.
1
2
For even more context: this is part of stuff I'm playing around with in my binary data description language, Fathom:
1
3
"ok if not everything can be translated initially" – that is to say, we're ok if the elaboration process results in errors if the target language cannot match the expressiveness of the source language.
1
Papers recommended to me on #dependent:
• “Extracting Fω's Programs from Proofs in the Calculus of Constructions” by Paulin-Mohring
• “Foundations of Dependent Interoperability” by Dagand et al.
• “Type-Theory In Color” by Bernardy and Moulin
More suggestions welcome though!
2
6
I guess part of the challenge is that my target language, Rust, might be able to express some of the dependent stuff, and sometimes this is important for performance - eg. if we know the exact length of a list, we could translate it to a fixed length array. 🤔
3
2
I assume not for lists tho, they have different asymptotics, but you can provide a different API.
Sorry for the tangent, but the actual question is much harder... but the size of fixed length arrays must be a constant, right? That would avoid pi-types in Rust.
1
Replying to
Yeah, I'd have to require the length to be known statically to perform that optimization.