3 ms·
> What blew me away was once you have such a strong type system it eliminates whole classes or errors at compile time I previously considered only checkable at
by runeks 9y ago
> What blew me away was once you have such a strong type system it eliminates whole classes or errors at compile time I previously considered only checkable at runtime.
Can Idris turn Haskell runtime errors into compile-time errors and, if so, which ones?
- bbatha 9y agoThe classic one is the `head` function in idris can only be called on `Vec`s of length 1 or more. More pressingly, you can actually prove lawfulness of type classes.
- aaron-santos 9y agoI'm curious how does this compare to something like Cats' NonEmptyList[1] in Scala? [1] - https://github.com/typelevel/cats/blob/master/core/src/main/scala/cats/data/NonEmptyList.scala https://github.com/typelevel/cats/blob/master/core/src/main/...
- dynamic 9y agoChecking the head of an empty list is a simple example. (Although see https://wiki.haskell.org/Non-empty_list https://wiki.haskell.org/Non-empty_list for an approach to avoiding these runtime errors in Haskell). Here's a more advanced example: https://news.ycombinator.com/item?id=14569605 https://news.ycombinator.com/item?id=14569605.
- pyrale 9y agohead [] in haskell will crash and burn, because you cannot carry vector size information in the type (at least not easily). In idris, you can lift the non-empty list check at type level, making such operation a compilation error.