3 ms·
The problem is that math types are equivalent to dependent structural types. You can say, "let x be a set with a comutative binary operation". In languages with
by DanielRibeiro 15y ago
The problem is that math types are equivalent to dependent structural types. You can say, "let x be a set with a comutative binary operation". In languages with Hindley–Milner type inference you can do almost the same (you will miss the dependent part).
And the most famous languages with static typing (Java, C++, C#, Scala) do not have such power.
For more information, I'd urge you to see the amazing presentation[1] of Daniel Spiewak's, Uncovering the Unknown: Principles of Type Inference, and James Iry's Types à la Chart [2]
[1] http://screencasts.chariotsolutions.com/uncovering-the-unknown-principles-of-type-inference- http://screencasts.chariotsolutions.com/uncovering-the-unkno...
[2] http://james-iry.blogspot.com/2010/05/types-la-chart.html http://james-iry.blogspot.com/2010/05/types-la-chart.html
- kamechan 15y ago> In languages with Hindley Milley type inference ... Small correction, it's actually "Hindley-Milner type inference".
- DanielRibeiro 15y agoThanks. Fixxed the typo.
- wbhart 15y agoApparently it's Hindley-Milner type system or Damas-Milner type inference. I didn't know that myself until I watched the video.
- deleted 15y ago[deleted]
- fleitz 15y agoDefinitely agree with you on those points, what do you think of the type system in F#?
- DanielRibeiro 15y agoF# seems to have a Hindley-Milner type system, as described some years ago also by Daniel Spiewak[1]. Which is a vast improvement over more mainstream type systems, while not as powerful as traditional logic type systems, such as those used in First order and Higher Order Logic. However, I personally rely more on unit tests than on type systems to make sure the code is consistent. And when I do that, specially when I write the test before the code, I find the type system getting more in the way than helping me. Rich Hickey, Clojure's creator, compared[2] these to guard-rails. [1] http://www.codecommit.com/blog/scala/what-is-hindley-milner-and-why-is-it-cool http://www.codecommit.com/blog/scala/what-is-hindley-milner-... [2] http://www.infoq.com/presentations/Simple-Made-Easy http://www.infoq.com/presentations/Simple-Made-Easy
- wbhart 15y agoInteresting. In [1] he claims that languages with a nominal type system cannot have global type inference. Yet Nemerle claims to have both.