[MichaelBurge]

Many of these you can work around with language extensions or a custom Prelude, but then you need to have been bitten by them to know that you need to work around them.

I hear "dependent types" and I think "theorem prover", but it seems like Idris is a cleaned up Haskell with some light proving features built in?

Haskell is good for compilers and parsers. What's a good excuse to try Idris?

[neel_k]

> I hear "dependent types" and I think "theorem prover", but it seems like Idris is a cleaned up Haskell with some light proving features built in?

It's a full-strength dependent type theory, but is intended primarily for use as a programming language. So the design focus is on using full dependent types to make ordinary programming easier.

> What's a good excuse to try Idris?

The best excuse of all: it is super fun.

[johncolanduoni]

Dependent types can help a lot when writing both of those actually. Idris' documentation contains an example interpreter that uses dependent typing (outside of theorem proving) heavily[1]. Compilers are a place where formal verification is likely worth it in some parts, particularly when writing optimization passes.

I think one of the biggest advantages of dependent typing is that it lets you implement a lot of things that other languages need to add as ad-hoc language features. A good example (if you're familiar with Haskell) is typeclasses. These can be done entirely at the value level in Idris, and IIRC interfaces are just syntactic sugar over this implementation. Other examples are generics that depend on values instead of types (without resorting to tedious things like type-level integers) and cleaner replacements for a lot of macro functionality.

[1]: http://docs.idris-lang.org/en/latest/tutorial/interp.html

[HelloNurse]

Many of the points touched in the article are simply the difference between designing a programming language for giving the authors a feeling of bleeding-edge cleverness and designing it for the benefit of programmers using it. It's quite more than an "excuse" to prefer Idris.

[pjmlp]

> Haskell is good for compilers and parsers.

While true, the same applies to any other language in the ML family.