Hacker News Reader

Comment by hbex5 | Hacker News Reader

Idris is one of those languages that when I learned it felt like it was offering me a glimpse into a possible future.

I love it when that happens.

Would you mind sharing what it was about Idris that made you feel like you were offered a glimpse into a possible future?

I can't speak for op but I had a similar feeling going through the free chapters of 'Type driven development with Idris'. 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. Furthermore it showed that doing so allows the compiler to go from being a gatekeeper to being more of a virtual assistant that helps you write your code not just check it.

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

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.

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

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.

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.

Pony language's "reference capabilities" are like this--which separates the idea of type from the access to memory, and provides another level of error-class elimination and its composition of these reference capabilities and the actor model for another reduction of runtime overhead in garbage collection (being lock-free and concurrent.)

https://tutorial.ponylang.org/capabilities/reference-capabil...

https://tutorial.ponylang.org/appendices/garbage-collection....

Reply on news.ycombinator.com