6 ms·
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 cla
by bbatha 9y ago
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 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/...