[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/...