[rbehrends]

> Inheritance is not a way to express sum types, it's a form of subtyping.

A distinction without a difference. This is probably most visible in languages like Scala and Kotlin, which implement algebraic data types by way of inheritance.

That inheritance creates a subtyping relationship is irrelevant; there's a similar subtyping relationship between variants (or groups of variants) and the overarching type using a traditional sum type notation as in Haskell or ML. This is most clearly visible in OCaml's polymorphic variants [1, 2].

[1] http://caml.inria.fr/pub/docs/manual-ocaml-400/manual006.htm...

[2] https://stackoverflow.com/questions/16773384/why-does-ocaml-...

[mcguire]

Pony (https://ponylang.org) uses sum types, perhaps excessively. Just yesterday, I wrote:

    (None | (In, USize))

I.e., None (the null valued type) or a pair made of a type variable (In) and a USize.

The thing is, the values that satisfy this type are not subtypes of None and a pair. (That would be silly, given None.) Such a value is either None, or a pair.

[rbehrends]

> The thing is, the values that satisfy this type are not subtypes of None and a pair. (That would be silly, given None.) Such a value is either None, or a pair.

Unless I'm misreading you, this seems to be a misunderstanding of what sum types are. A sum type `T = A | B` represents the (disjoint) union of all possible values of `A` and of all possible values of `B`, simply put, not the intersection (as you seem to indicate by the phrasing of "not subtypes of None and pair"; correct me if you meant something else).

Recall what subtyping means (I'm going with Wikipedia's definition here for sake of accessibility):

> [S]ubtyping (also subtype polymorphism or inclusion polymorphism) is a form of type polymorphism in which a subtype is a datatype that is related to another datatype (the supertype) by some notion of substitutability, meaning that program elements, typically subroutines or functions, written to operate on elements of the supertype can also operate on elements of the subtype.

This holds in the case of sum types. Operations that work on the sum type will generally also work on the variants that constitute the sum type.

The same goes for inheritance. If an abstract class T has two concrete subclasses `A` and `B`, then a value of type `T` belongs to the union of values of type `A` and of type `B`.

[tel]

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.

[rbehrends]

> 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.

[tel]

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.