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
Maybe this is relevant? iro.umontreal.ca/~monnier/comp-
1
1
3
Sounds like singleton types is what you are looking for. Haskell uses GADTs for them today but they can be encoded in F-omega.
1
1
Awesome! I'll check out that paper! One option I had was this: twitter.com/brendanzab/sta - which is more singleton-like I think?
Quote Tweet
Replying to @brendanzab and @Blaisorblade
I guess you could also do this, which is more like the singleton approach? 
1
Wow, from an initial pass the singleton types paper by Monnier and Haguenauer is looking really close to what I've been attempting to do right now! I need to read it more closely to be sure, but thanks so much, I really appreciate it! 🤩
1
2
I guess an added complication might be that I'm starting out with a core language more like MLTT, where I mix terms, types, and universes together. I'm guessing I'll need to have another pass to get it to look like the CC source language used in this paper?
I guess I'm a little confused in the paper with how it jumps from a Pure Type System to the layered CC source language in section 2.2. Is that assumed knowledge - ie. covered elsewhere? Or left as an exercise for the reader? 😅
1
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