Hacker News new | ask | show | jobs
by 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.
1 comments
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