For even more context: this is part of stuff I'm playing around with in my binary data description language, Fathom:
Conversation
"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?
1
2
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”. 😅
