Hacker News Reader

Comment by seanmcdirmid | Hacker News Reader

> all of which are functional, in part also because OO/subtyping is hard to reason about formally

OO subtyping is hard to reason about formally in formal systems designed for FP...news at 11! I jest.

The reason FP does so well academically is that no one knows how to rigorously evaluate something that isn't theoretical (since FP is close to math anyways) or performance-based (most other PL work).

The Haskell crowd is also very creative so they do a lot of cool stuff. However, many of their ideas are transferrable to other languages without the FP ideology.

The OO people have something to offer also, but we've been kind of muted lately.

View on HN

>> OO subtyping is hard to reason about formally in formal systems designed for FP...news at 11!

Well. Even systems like L2 (which are not functional) find subtyping difficult. It becomes difficult in the presence of overloading and overriding.

I believe there's a nice book called Foundations of Object Oriented Languages which dissects the problem in depth.

Pierce's TAPL, also, and Harper's Practical Foundations. There's also some things i've seen about how scala does it, but I'll have to dig for them

http://www.cs.cmu.edu/~rwh/plbook/book.pdf

See also the DOT calculus[1] (Dependent Object Types) being the basis for a new foundation for scala's type system

[1] - https://github.com/namin/dot

OO subtyping is hard to reason about formally in formal systems _in general_.

And yet, is-a and has-a relationships predominate natural language. Well, it makes sense: natural language is hard to reason about formally also.

The problem isn't that `is-a` is hard, it's the divergence of `is-subtype-of` and `is-subclass-of`. Take a look here, I think it explains it rather well. http://okmij.org/ftp/Computation/Subtyping/

I would argue that nominative subtyping is natural (basically sub-classing), since it matches our ability to assign arbitrary meaning and relationships to words, which is incredibly useful when having a conversation. Ya, maybe a set isn't exactly a bag, but close enough. Birds mostly fly, but penguins don't, we can deal with that.

But the main problem with subtyping, nominative or structural, is how it messes up Hindley-Damas-Milner style type inference. But that shouldn't be surprising that an FP theory for type inference wouldn't work well for OOP.

Reply on news.ycombinator.com