"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.
Conversation
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.
1
1
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
Replying to
Yes, I like this idea! I have been wanting to make documentation for the language anyway (including internal docs), and this might be a good chance to start. I've also been sketching things out in Makam, but I feel like I might need an even lighter weight option here?
Replying to
I guess there's an implicit hierarchy of prototypes — I'm not that organized, but idealizing, my actual scratchpad is made with OneNote & C. + Apple Pencil (or anything good enough for math), what sounds good gets typeset and explained, and what's still good gets implemented.
1
1
Yeah lots of my time on this project has been consumed by:
1. been getting to grips with the subject matter
2. figuring out ways to efficiently prototype
Been rather challenging - I've gone down _so_ many paths for both. Fun, but exhausting! And still got lots to learn!
1
1
Show replies