Hacker News new | ask | show | jobs
by tel 3219 days ago
Not true. You can model sums with inheritance along with an exclusivity constraint, but it's a weird model and subtyping is more general. Further, the idea of each variant being its own type is inherently a subtyping sort of idea. Sums don't give names to their conponents, only distinctions.
1 comments
rbehrends 3219 days ago
> You can model sums with inheritance along with an exclusivity constraint, but it's a weird model and subtyping is more general.

You don't need an exclusivity constraint. Exclusivity is purely a modularity concern; you will still have a finite number of variants in any given software system; traditional ADTs and exclusivity just limit the declaration of variants to a single module. See also "open sum types" vs. "closed sum types", because it can be beneficial to have extensible sum types [1]. Not all sum types are closed; see polymorphic variants and extensible variants in OCaml.

Also, do not confuse the language mechanism used to specify a type with the type itself.

I do agree that inheritance is a generalization of algebraic data types.

> Further, the idea of each variant being its own type is inherently a subtyping sort of idea. Sums don't give names to their conponents, only distinctions.

Try polymorphic variants in OCaml (mentioned above); or GADTs:

  # type _ t = Int: int -> int t | String: string -> string t;;
  type _ t = Int : int -> int t | String : string -> string t
  # Int 0;;
  - : int t = Int 0
  # String "";;
  - : string t = String ""
There's nothing inherent about summands not having a distinct declared type in ML and Haskell, only convention. Obviously, they do have distinct actual types.

Edit: A practical use case is the representation of nodes for an abstract syntax tree. An `Ast` type can benefit from having abstract `Expr`, `Statement`, `Declaration`, `Type`, etc. subtypes that group the respective variants together in order to get proper exhaustiveness checks, for example.

[1] See the question of how to type exceptions in Standard ML; in OCaml, this led to the generalization of exception types to extensible variants.

link
tel 3216 days ago
I'm aware of polymorphic variants and row types and the like. My concern is one of modularity in that I consider a running system pretty dead, extensions during coding are where language features and their logics are interesting. Closing your sums is valuable to consumers: they have complete induction principles, e.g.

Open sums and row types are a little different in that they represent a fixed/closed type but retain enough information to extend it more conveniently and to see it as structurally related to other (open) sums/products. This is no doubt super useful, but I see it more as an application sitting atop polymorphism rather than a fundamental concept.

Finally, I am exactly confusing the language mechanism with the type it intends to model because exactly now we have to think about things as a mechanism and model. This is where breakdowns occur.

Anyway, I doubt there's a real difference of opinion here. I'm very familiar with the concepts you're discussing, but perhaps argue that they are not as fundamental as regular, closed sums/products and language support for those simplest building blocks is important.

link