For me, dependent types are about precision and productivity, and expressing my understanding of a problem as well as possible in types.
-
-
Show 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 …
Show 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”
Show 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.
Show this thread
End of conversation
New conversation -
-
-
I’ve found indexing terms by names really valuable. And that the state machines in general gets a lot of benefit for not much effort.
-
So I’m not really sure what you’re looking for. I’m after high reward (if not perfect) for low effort…
End of conversation
New conversation -
-
-
I suppose to some extent that depends what you mean by "nice". My favourite examples are often about side effects and state, for example.
Thanks. Twitter will use this to make your timeline better. UndoUndo
-
-
-
To me this seems like trying to present a downside as a benefit (what’s good for math is not what’s good for programs). And while I’ve never seen truly useful hole filling, there’s nothing that prevents it being done with contracts as well (if it were ever proven useful).
Thanks. Twitter will use this to make your timeline better. UndoUndo
-
-
-
Dependent type theory is a foundation of math, so that's a non-trivial and nice application. Logical frameworks (not quite dependent type theory but close) are used to express and reason about formal systems, including type theory, that's another application.
Thanks. Twitter will use this to make your timeline better. UndoUndo
-
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.