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
What usually can't be translated in those systems (at least the first): large eliminations (intuitively, computing a type from a value by pattern matching).
Translating that might require fake dependent types with GADTs and "singleton types" (mirror valued at the type level).
1
1
I was thinking something like this:
f : (b : Bool) -> if b then String else I32
f True = "hi"
f False = 42
Could be compiled to this:
3
Interesting, never seen it! _But_ the source language lets you combine that with `if b2 then I32 else String` (if b = !b2) or `if b then File else I32` (do you create another sum type?).
1
Replying to
I guess for booleans I could parameterise the tagged union, but I think this might be more challenging, say, for integers, where you have lots of different cases. I'd probably be fine doing things naively first, seeing as it's not intended as a general purpose language.
