3 ms·

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

• seanmcdirmid 13y ago
  And yet, is-a and has-a relationships predominate natural language. Well, it makes sense: natural language is hard to reason about formally also.
  • deleted 13y ago
    [deleted]
  • Tyr42 13y ago
    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/ http://okmij.org/ftp/Computation/Subtyping/
    • seanmcdirmid 13y ago
      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.