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
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
Yeah, this is very good point that I'd forgotten about. I was intending to generate coercion-style things between these generative things, and yeah, I absolutely will be testing this stuff! I've got no idea how challenging this will be though. 😨
1
1
Linking is absolutely a frustrating issue with this approach. At the moment separate compilation of binary format descriptions is a desirable, but far off goal. Not sure how I'd handle that yet.
Thanks again for all these thoughts! They've come to me in the past, but somewhere along the line they fell out of my head.
1
Last time this happened to me, I wrote a draft paper describing my approach, as Simon PJ recommends. Maybe call it a design document?
The point of that, by convincing your audience that your approach works, you'll notice where it doesn't yet and how to fix it.
1
1
Show replies