undefined | Better HN

0 pointslmm10y ago0 comments

It means there's a diversity of Scala styles; one person's Scala won't necessarily look like someone else's. More concretely it causes a lot of problems for type inference (particularly when ADTs in Scala are modeled as traits with implementing classes, so e.g. the type of Some(x) ends up as Some rather than Option). Other ML family languages that don't have traditional OO inheritance generally have perfect type inference (at least in the absence of higher kinds) via Hindley-Milner.

0 comments

1 comments · 1 top-level

mafribe10y ago

Practical type inference for Hindley-Milner-style languages with higher kinds is not a problem, see e.g. [1]. The problem is adding sub-typing.

I'm also not 100% sure it's correct to say that ML-style languages have no problem with type-inference. I'm sure Robin Milner would have preferred having full, unrestricted parametric polymorphism (i.e. System F) in ML. Alas System F has undecidable type inference [2]. Hindley-Milner is a restriction of full parametric polymorphism that enjoys type inference, and is expressive enough to type many programs. BC Pierce says that the Hindley-Milner "has hit a sweetspot". I concur.

[1] M. P. Jones, A system of constructor classes: overloading and implicit higher-order polymorphism. http://www.cs.tufts.edu/comp/150GIT/archive/mark-jones/fpca9...

[2] J. B. Wells, Typability and type checking in System F are equivalent and undecidable. http://www.macs.hw.ac.uk/~jbw/papers/f-undecidable-APAL.ps.g...

j / k navigate · click thread line to collapse