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
“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”. 
Replying to
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! 😅