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 -
Sometimes this involves proving things. Perhaps as complicated as: “if x is in the list xs, it's also in the list xs ++ ys”
1 reply 0 retweets 14 likesShow this thread -
As understanding of a problem develops, types get refined to better explain what's going on. Not necessarily bigger, just better. We're going to need much better editing and refactoring tools than we currently have, though, to do this well.
3 replies 5 retweets 38 likesShow this thread -
Replying to @edwinbrady
I may have brought this to your attention wi last 2yr (or maybe david
@d_Christiansen) http://www.lamdu.org/ https://vimeo.com/977134391 reply 0 retweets 3 likes
Yes, I know of Lamdu, @EyalL gave me a demo a few years ago. It’s very promising. This is the sort of thing we’ll need.
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.