5 ms·

I don't think type hints do Hindley/Milner/Damas justice. This type system has two parts, none of which are present in most popular languages: 1. A program tha

by quchen 11y ago

I don't think type hints do Hindley/Milner/Damas justice. This type system has two parts, none of which are present in most popular languages: 1. A program that typechecks cannot have type errors during runtime. Dynamic type (i.e. runtime tag) based functions like instanceof break this, and most (all?) OOP languages have it in some form. 2. Type inference: the types of expressions can be unified to the most general type that works for all of them. I don't know any popular language that is able to do this. Most typing I see added to languages these days are cherry-picking consequences of the HM algorithm. C++'s auto keyword for example is a very simple version of type inference, type hints in dynamic languages aren't checked (or checkable) statically, and when runtime tags are involved it's hard to speak of static type inference.

mafribe 11y ago
I don't think type hints do Hindley/Milner/Damas justice. I agree. Retro-fitting Hindley-Milner would be difficult. Rpython has type-inference for a subset of Python. But it's a special purpose language.
MrBuddyCasino 11y ago
I don't know any popular language that is able to do this. Wikipedia lists ML and Haskell - are they missing some detail?
- marvy 11y ago
  not very popular :)
- quchen 11y ago
  I wouldn't call ML popular, and in Haskell you have type classes, which have undecidable type inference. You can write `show (read str)` in Haskell for example, which parses `str` and then converts it back to `String` again. But the compiler cannot infer which type you want to parse to: is the input an Int, a Double, a JSON object, any other read/showable format? In these (rare) cases, you need explicit type annotations. (Without type classes, type inference is decidable in Haskell.)
  - mafribe 11y ago
    As an aside, Hindley–Milner is DEXPTIME-complete, and indeed you can write 5 line programs that exhibit the worst-case behaviour. That's as bad a worst-case behaviour as undecidability for all practical purposes. That said, in practise, HM type inference tends to be very fast, because the worst-case behaviour only shows up in rather artificial programs that human programmers would normally not write. If you bound the depth of let-nesting, HM is polynomial.
    - quchen 11y ago
      You're correct on the theoretical side, and writing a value whose type makes GHC crash is fairly easy. But in multiple years of Haskell, I did not encounter nor have I heard of a practical case in which type inference time was a performance issue, let alone a bottleneck or problem.

by quchen 11y ago

mafribe 11y ago

I don't think type hints do Hindley/Milner/Damas justice. I agree. Retro-fitting Hindley-Milner would be difficult. Rpython has type-inference for a subset of Python. But it's a special purpose language.

MrBuddyCasino 11y ago

I don't know any popular language that is able to do this. Wikipedia lists ML and Haskell - are they missing some detail?

marvy 11y ago
not very popular :)
quchen 11y ago
I wouldn't call ML popular, and in Haskell you have type classes, which have undecidable type inference. You can write `show (read str)` in Haskell for example, which parses `str` and then converts it back to `String` again. But the compiler cannot infer which type you want to parse to: is the input an Int, a Double, a JSON object, any other read/showable format? In these (rare) cases, you need explicit type annotations. (Without type classes, type inference is decidable in Haskell.)
- mafribe 11y ago
  As an aside, Hindley–Milner is DEXPTIME-complete, and indeed you can write 5 line programs that exhibit the worst-case behaviour. That's as bad a worst-case behaviour as undecidability for all practical purposes. That said, in practise, HM type inference tends to be very fast, because the worst-case behaviour only shows up in rather artificial programs that human programmers would normally not write. If you bound the depth of let-nesting, HM is polynomial.
  - quchen 11y ago
    You're correct on the theoretical side, and writing a value whose type makes GHC crash is fairly easy. But in multiple years of Haskell, I did not encounter nor have I heard of a practical case in which type inference time was a performance issue, let alone a bottleneck or problem.