4 ms·
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
by tuukkah 10y ago
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 http://blog.tweag.io/posts/2017-03-13-linear-types.html
- riffraff 10y agoAs 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 https://news.ycombinator.com/item?id=12350273
- tathougies 10y agoBut type inference takes a hit. Trade offs -- conceptually similar but potentially needing more annotation
- mietek 10y agoGood Haskell style already presupposes top-level type annotations.
- bad_user 10y agoHighly 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.
- ziman 10y agoWhile 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.
- mrkgnao 10y agoI 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.
- Kutta 10y agoI'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.