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!
Replying to
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
“Singleton types here, singleton types there, singleton types everywhere” by Monnier and Haguenauer seems to be extremely close to what I've been after! Thanks for the pointer!
Quote Tweet
Replying to @brendanzab
Maybe this is relevant? iro.umontreal.ca/~monnier/comp-
1
1
5
The paper sneakily leaves the generalization to a PTS (which is close to what I have in my core language) right until the end! 😆
Quote Tweet
Replying to @brendanzab and @fancytypes
Aha! I think this is covered later on - always somewhat confusing when papers do this. Something like: “If in doubt, read backwards from the end”. 
1
1
1
This bit really confused me initially - took me _many_ readings to understand! So it seems like they are making two global definitions called `Nat` and `Ω` that will be available later in the later rules, using syntactic sugar over`Ind(k:Kind){k0..kn}`. 🥴
1
1
I was really confused as to how the constructors of the inductive definitions were suddenly appearing in the later rules. Turns out they are global definitions that can be desugared down to the core TL language - not sure if I am just really bad at reading or what! 😅
Replying to
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
Show replies