Discussions of dependent types often assume they're all about specification and proof. That's part of it, but not the most interesting bit.
-
Show this thread
-
For me, dependent types are about precision and productivity, and expressing my understanding of a problem as well as possible in types.
1 reply 37 retweets 92 likesShow this thread -
e.g. so far in Blodwen (a mini-Idris in Idris), I've got huge value just out of this one dependent type:https://github.com/edwinb/Blodwen/blob/master/src/Core/TT.idr#L114 …
2 replies 2 retweets 31 likesShow this thread -
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.