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
Replying to
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:
I guess you could also do this, which is more like the singleton approach? 🤔
1
1
2
The process to getting to either one of these is rather intimidating though, and would involve a bunch of stuff that I still need to learn, like uncurrying etc. Hence why I'm fine with not solving it for all possible input programs (it's ok if I have errors during extraction).
1
Replying to
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
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.
1
Replying to
Even with `if b then String else I32`, you're translating to a generative construction `FOutput`. Do you merge all definitions of FOutput? Does that mean you can't link 2 programs using `if b then String else I32`?
1
1
Or do you add partial conversions that throw "must not happen" errors when failing?
The last is probably a good idea with your constraints, at least as a first try. It will need (more) serious testing of the output, but you should test it anyway so :-).
1
1
Show replies