[runeks]

> 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]

The 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]

I'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/...

[dynamic]

Checking the head of an empty list is a simple example. (Although see 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.

[pyrale]

head [] 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.