Comment by nostrademons | Hacker News Reader

Comment by nostrademons | Hacker News Reader

Parent Full thread

Type inference in the presence of OOP-style subtyping was largely considered to be impossible in 2005; there had been a lot of research results with System F:< and System Fw, along with a well-known undecidability result [1]. Attempts to introduce subtyping into research languages like Haskell and Ocaml gave us records [2] and objects [3], but neither of these were something that an ordinary mainstream programmer would want to use. Haskell's type system made it frustratingly easy to construct types that would force the typechecker into an infinite loop [4].

And now Swift not only allows these in a way that's familiar to existing mainstream programmers, it interoperates fully with Objective-C and offers additional features like polymorphic literals. And when polymorphic literals (previously allowed only by Haskell, and then not with user-defined types) makes typechecking take 12 hours [5], it's widely decried for being poorly implemented.

On the Rust end - the whole concept of the borrow checker was borrowed (sorry) from Cyclone [6][7], a research language of the early 2000s. I remember seeing it occasionally pop up on Lambda: the Ultimate [8] around 2004-2005, people seemed intrigued, but few people really took notice. Rust's big accomplishment is to generalize this to an "industrial strength" programming language, figuring out all the corner cases around mutability, traits, move-semantics, boxes, etc. that you need for this to work in real programming.

[1] http://repository.cmu.edu/cgi/viewcontent.cgi?article=3059&c...

[2] http://research.microsoft.com/en-us/um/people/simonpj/Haskel...

[3] https://realworldocaml.org/v1/en/html/objects.html

[4] https://downloads.haskell.org/~ghc/latest/docs/html/users_gu...

[5] https://www.reddit.com/r/programming/comments/4givdg/go_home...

[6] http://www.bennetyee.org/ucsd-pages/Courses/cse227.w03/hando...

[7] https://www.cs.umd.edu/~mwh/papers/ismm.pdf

[8] http://lambda-the-ultimate.org

> On the Rust end - the whole concept of the borrow checker was borrowed from Cyclone

Not really. That's the lifetime system, which is not the same thing. "Existential Types for Imperative Languages", also by Dan Grossman, explains more of the motivation, but the borrow check is a hybrid of the two solutions he presents.

Borrowing itself is something with a long history, but the whole "unique loan paths" thing makes Rust's solution distinct from a lot of the stuff you find in the research literature.

> Type inference in the presence of OOP-style subtyping was largely considered to be impossible in 2005

Type inference in a OO language is still considered, if not impossible, at least very impractical. Swift, Scala and Rust avoid most algorithmic complexity and ambiguity by mostly supporting only type propagation instead of type inference, and thus require annotations on function parameters.

The big innovation there is in realizing that's enough. When I was into language design from 2004-2007, language designers usually assumed people wanted full global type inference. It turns out that local type propagation is an effective 80/20 solution for most practical programming tasks, which opened up a lot of hybrid type systems that would've been far too complex before.

Yes. A blessing in disguise. In hindsight, global type inference seems too unstable. Too much action at a distance; it's hard to evolve a codebase when local changes cascade. Type annotations keep things grounded.

Nemerle had quite an interesting solution to this problem back then.

http://research.microsoft.com/en-us/um/people/moskal/pdf/msc...

Yes. It’s worth pointing out that this is the author’s MSc thesis, submitted in 2005.

What about Crystal? It has quite extensive type inference.

Unfortunately they also had to narrow down the scope of type inference recently. IIRC type annotations are now mandatory for class-level variables (member variables). This hindered the "Ruby-like" feeling, but they had to give up global type inference because it costed too much memory in some cases. I got an impression that global type inference is difficult (or, costly) in general.

I'm not sure I consider Rust to be object oriented.

> Haskell's type system made it frustratingly easy to construct types that would force the typechecker into an infinite loop [4].

It's more akin to C++ templates, where the type checker only has a bounded number of reductions it will do before it gives up. Aside from writing something that really is infinite and a limit of trillions of reductions - which wouldn't really be a useful program - it ends up as a type error as you'd expect. This also only happens with -XUndecidableInstances, which frankly isn't really one of the most common extensions, I'd say.

That said, in practice, most Haskell programmers seem to largely consider subtyping a misfeature anyway, and approximations of it elsewhere in the ecosystem use things like RankNTypes to give a 'feel' for subtyping where you can do things like "use any instance of a more general base type, in place of that type, right here". The infamous lens library does this to great effect.

> previously allowed only by Haskell, and then not with user-defined types

I don't know what you mean here - Haskell has, until recently, never allowed overloaded literals for certain syntactic forms, like lists. For the other cases, though, like numerics, you have always been able to have polymorphic literals, which can be instantiated to user-defined type. The most general type of `1` by itself with no defaulting is `1 :: Num a => a`, and there's certainly no problem with instantiating `a` to whatever user-defined type you have, providing it can sensibly be constructed from a base-10 decimal value (meaning, you have a function `toInteger :: Integer -> a`)

These days, lists are also syntactically overloadable by a similar convention, through value polymorphism/type classes.

Meanwhile companies like Google invest their money in languages that were already known to be possible in 1968.

http://cowlark.com/2009-11-15-go/

I like Rust, but there is nothing wrong with Go (I think their decision to not have generics does have some merit). They just took trade-offs they needed. Nothing wrong with that.

I did like Oberon a lot, and appreciate Oberon-2 influence on Go, but I think there is a lost opportunity in a company like Google sponsoring such a design, when it could have done so much more helping advancing the state of art for mainstream developers.

In that regard, Apple and Microsoft do so much more to help developers improve their skill sets, given the programming languages and tools that they have brought into the market.

However, I do advocate Go for the use cases where developers still make use of C for user space applications, without any real need for C's low level features.

Also do believe that Go can actually be used for systems programming, even if not all scenarios from systems programming like for example, 8 and 16 bit embedded processors, can be covered.

The language is similar enough to Oberon and Limbo for it to be possible, just needs someone to write a bare metal runtime.

Reply on news.ycombinator.com