"Totally" I see what you did there
-
-
Indeed. Although, I haven’t implemented a totality checker yet :).
2 replies 0 retweets 1 like -
Replying to @edwinbrady @plragde
Is this the land where you'll experiment with other effects systems?
1 reply 0 retweets 0 likes -
I'm hoping to experiment with lots of things, but first I want a core that works properly. DTs are really helping so far...
2 replies 0 retweets 3 likes -
Idris about to be self hosting?
1 reply 0 retweets 2 likes -
I am making no promises :). But wherever this ends up, I hope it will fix some of the mistakes in the design/implementation of Idris…
1 reply 0 retweets 5 likes -
Replying to @edwinbrady @milessabin and
Mostly I’m doing this because I want to write a big(ish) thing in Idris, and type checkers are the only things I know how to write.
2 replies 0 retweets 12 likes -
Replying to @edwinbrady @milessabin and
So, what is the theory your type checker implements?
1 reply 0 retweets 0 likes -
-
Replying to @edwinbrady @milessabin and
Do you think
@pigworker's linear dependent types/quantitative type theory is mature enough to be used a the core of a dependent language?1 reply 0 retweets 2 likes
Trying it would be one way to find out :). I did a toy implementation a while back, and it’s very promising.
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.