News for hackers. Stuff that matters.

A comment on Try Idris. Parent comment

Re:Try Idris by thinkpad20 on Monday April 14, 2014 @12:38AM (#7584565)
I don't know that much about Idris, but from my understanding, its type system is more advanced than Haskell's, because dependent types by definition contain more information than the (independent?) types used in Haskell (can't comment on scala). Haskell as a language with all of its various extensions and bells and whistles is surely far more complicated, having been around a great deal longer and with a massive compiler and numerous features, but from my knowledge it's incorrect to say Idris is simpler than Haskell, at least in regards to its type system.
[ Parent | on HN ]
Re:Try Idris by chriswarbo on Monday April 14, 2014 @08:27AM (#7585706)
Idris's types system is both more advanced and simpler than Haskell's. For example, "vanilla" Haskell's type system implements (amongst other things) functions, records, parametric polymorphism and typeclasses. Idris implements (amongst other things) dependent functions and dependent records.

Idris doesn't need to support (non-dependent) functions or parametric polymorphism, since they're just special-cases of dependent functions. Likewise, typeclasses are just special-cases of dependent records.

When we consider Haskell extensions, many of them are designed to introduce dependently-typed idioms (eg. DataKinds). This makes Idris automatically simpler, since it supports those idioms directly and doesn't have to offer all of the non-dependent parts of Haskell.

On the other hand, typical Haskell programs may use types in a simpler way than typical Idris programs, but that's a separate point. We can focus on simple programs while learning.

[ Parent | on HN ]
Re:Try Idris by jonsterling on Monday April 14, 2014 @05:53PM (#7589178)
To be fair, Idris does not in general support parametric polymorphism, though you could extend it to do so.

Idris has a quantifier which is called Pi in type theory, and this is not the same as Forall (the quantifier present in Haskell and ML). Forall gives you guarantees about uniform behavior over the domain of quantification (this is parametricity), whereas Pi does not.

Idris does however recover parametricity anyway for types, since it lacks an eliminator for the universe (i.e. it doesn't have type-case). But it doesn't have parametric polymorphism for values.

[ Parent | on HN ]