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...https://gist.github.com/edwinb/18638589f9de62a6419c9c32e22a9edd …
-
-
Replying to @edwinbrady
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 reply 0 retweets 1 like -
Replying to @brendanzab
The magic is more or less what you see in https://eb.host.cs.st-andrews.ac.uk/drafts/elab-reflection.pdf … by
@d_christiansen and me1 reply 0 retweets 2 likes -
Replying to @edwinbrady @d_christiansen
Oh right, cool! Think I've come across that one before!
1 reply 0 retweets 1 like -
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 reply 0 retweets 4 likes -
Replying to @brendanzab @d_christiansen
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 replies 0 retweets 4 likes -
Replying to @edwinbrady @brendanzab
The Lean folks made their similar feature really fast, it might be worth stealing some implementation techniques
1 reply 0 retweets 4 likes -
Replying to @d_christiansen @brendanzab
My hunch is that the overhead will be quite small for what I have in mind (I'm only reflecting high level things for now) but once it gets to developing proof scripts I should certainly do that.
1 reply 0 retweets 0 likes -
Replying to @edwinbrady @brendanzab
I think a big improvement to make on the current Idris elab refl is to bake-in quotations a la Eli Barzilay's thesis, rather than representing them as just another datatype. Something like data TT = ... | Quote Nat TT where the quote level 0 is an antiquotation
2 replies 0 retweets 3 likes -
Can we also have IO side effects in Elab? (as mentioned in the conclusion section of
@d_christiansen's dissertation) For example, it would allow us to call an SMT solver inside Elab.1 reply 0 retweets 1 like
It's technically possible. But right now the main goal is (not joking here...) to be able to implement the rest of Blodwen in itself.
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.