The proto-Idris-2 doesn't have high level constructs yet, but it has Elaborator Reflection now so I'll probably implement the rest of it that way...
Conversation
Ooh, what magic is this `%runElab` thingy? How does it know about those user-defined data types you made in that gist? Does it verify that they're of the right 'shape' first, or is it more of a macro-style thing?
1
1
1
2
Oh right, cool! Think I've come across that one before!
1
1
Kind of looks similar to what I've been wondering - could you consider have a language that just treated the file as some statically run monady thing, then commands like `data` and `import` would just be functions that alter the environment…
1
4
That's pretty much how it works. Reflection exposes that, so as long as the overhead is low (which it is) it seems a plausible way to implement the rest (e.g. records, interfaces, etc)
2
4
Just been starting to look at what is out there about structural dependent record types actually… there's some stuff out there by Luo and Feng. They base their stuff on LF which is a little alien after starting off with LambdaPi and Agda. So many weird ways of chopping up TT. 😬
Do most folks just forgo structural records at the moment because the subtyping is really annoying?
1