5 ms·
Types exist in mathematics it's just that when discussing mathematics the types are usually inferred. A lot of computer science concerns itself with algorithms
by fleitz 15y ago
Types exist in mathematics it's just that when discussing mathematics the types are usually inferred. A lot of computer science concerns itself with algorithms rather than math.
eg. When multiplying integers and matrices respectively you'd use a different algorithm to compute the result of multiplying the respective types.
Types mostly disappear as well when using a language derived from the lambda calculus vs. the universal turing machine.
- DanielRibeiro 15y agoThe 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.
- chc 15y agoI'm not sure that's quite right. Haskell models the lambda calculus pretty closely, but it has one of the most complicated type systems known to man. In its modern form, the type system is Turing-complete. The type system itself is capable of universal computation. The thing is just that type systems tend to be more usable in lambda calculus languages.
- wbhart 15y agoYou mean that Haskell has one of the most complex of the practical type systems known to man. For example (correct me if I am wrong) but the Haskell type system does not allow specification of dependent types (though dependent typing can be simulated after a fashion). Haskell with extensions does have a Turing-complete type system though (I actually don't know what this means, but the internets says so -- perhaps someone can tell me the difference between Haskell and Haskell with extensions).