Hacker News Reader

Comment by tuukkah | Hacker News Reader

Your example (and more) can be achieved by linear types which are coming to Haskell: "The patch is currently under 1000 lines long. We are targeting a merge by the time of the 8.4 release of GHC." http://blog.tweag.io/posts/2017-03-13-linear-types.html

View on HN

As I understand it, one selling point of Idris' type system is that it's actually simpler than haskell as it's based on a single very generic concept that covers a wide range of applications, rather than a sum of specialized things.

There was some discussion previously on HN about this https://news.ycombinator.com/item?id=12350273

But type inference takes a hit. Trade offs -- conceptually similar but potentially needing more annotation

Good Haskell style already presupposes top-level type annotations.

Highly generic code yields complicated signatures, so even if it's good style to add those signatures for top level declarations, it's really good to have the compiler help you figure out what that signature is.

While dependent type inference is more difficult, you get program inference in exchange. That's not a bad tradeoff because I'd rather write the spec (type) and have the computer fill in the boring bits, rather than the other way around.

I remember seeing an Edwin Brady talk (it featured a now-possibly-famous Brexit joke) in which the compiler almost inferred ... I think it was either zip or a fold.

I've seen this over and over but it's false. Adding dependent types do not negatively affect type inference for the non-dependent fragment in any shape or form. On the contrary, Agda/Coq type inference is far more powerful than in Haskell. While Agda/Coq do not have let generalization, that is by purely a design decision and not some kind of limitation.

Reply on news.ycombinator.com