# Sum types: sub- & super-type

**URL:** <https://discuss.ocaml.org/t/sum-types-sub-super-type/5894>\
**Category:** Community\
**Created:** [June 1, 2020, 9:19am UTC](https://discuss.ocaml.org/t/sum-types-sub-super-type/5894 "2020-06-01T09:19:53Z")\
**Posts on this page:** 1\
**Page:** 1

<div class="post-metadata">

**Author:** ![recoules](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/recoules/32/1742_2.png) [@recoules](https://discuss.ocaml.org/u/recoules)\
**Post date:** [June 1, 2020, 9:19am UTC](https://discuss.ocaml.org/t/sum-types-sub-super-type/5894/1 "2020-06-01T09:19:54Z")

</div>

Hi,

I am here to share some though about the type system of sum types in OCaml.

_Disclaimer_: I have not followed the language development for a while so, sorry if something similar have already been discussed elsewhere.

_Context_: I recently opened the Pandora’s box by playing with _polymorphic variants_ and I was stunned by their capacities and how easy it is to restrict or extend a type using them. Yet, they have some drawback and they suffer from a _bad reputation_ so for now, I can not expect to use them in my collaborative projects without annoying the other people. So, I am looking forward for some trade-off between the 3 ways for declaring sum types (ok, it is actually 2.5 since GADTs are parts of normal variants) and maybe, some cool new features.

**Motivating example**  
Here is an oversimplified example to illustrate the main features I wish to be present in OCaml.

```ocaml
module Expr : sig
  type t = Variable of string
         | Plus of t list
  val pp: Format.formatter -> t -> unit
end

module Equation : sig
  type t = Equal of Expr.t * Expr.t
         | Diff of Expr.t * Expr.t
end

module System : sig
  type t = Equation.t list

  val parse : string -> t
  val empty: t
  val add : Equation.t -> t -> t
  val solve : t -> (string * int) list
end

```

It is not rocket science, I think it is a basic usage of variants.  
Here are additional (arbitrary) constrains:

- the types should be finite to rely on exhaustive pattern matching;
- the types already exist and can not be easily modified;
- GADTs scare some people.

**Sub-typing**  
Let say that some sequences of variants make no sense or are not optimal in some context.

I want to implement some syntactic simplifications and for instance, the expression `Plus [Variable "a"; Plus [ Variable "b"; Variable "c"] ]` can be flattened: `Plus [Variable "a"; Variable "b"; Variable "c"]`.

I want to go further such as there is an invariant that enforces all the linear addition to be flattened.

```ocaml
module Var : sig
   type t = subtype of Expr.t = Variable of string
end

module NormExpr : sig
  type t = subtype of Expr.t = Variable of string | Plus of Var.t list
end

```

The definition is valid because the compiler can prove that _subtype_ always contains less variant than the type they are based on.

Now, when I will pattern match on a `NormExpr`, the compiler will warn me if I try to pattern match a non flattened addition. Still, I can _cast_ `NormExpr` to `Expr` to reuse any function defined for the latter.

_Note_: Here it is trivial but enforcing invariant in the AST of an normalized expression can be very valuable for complex types.

_Current status_:

- _standard_ variant: impossible
- polymorphic variant: possible but runtime will be slower
- GADT: I know a way to encode such invariant with _phantom_ type but it is pretty ugly for complex expressions and force to declare a lot of _universally quantified_ (unboxed) single variant types.

**Super-typing**  
For all the existing code, it makes no sense to have an additional variant, but for a very specific usage, I would like to extend the type of `Equation`.

```ocaml
module ExtEquation : sig
  type t = supertype of Equation.t
         = Equal of Expr.t * Expr.t
         | Diff of Expr.t * Expr.t
         | Interval of { lo: int; e: Expr.t; hi: int }
end

module ExtSystem : sig
  type t = ExtEquation.t list

  val add : ExtEquation.t -> t -> t
  val solve : t -> (string * int) list
end

```

Here, the point is that `ExtEquation` accept every variants of `Equation` so, `ExtSystem` is also a _supertype_ of `System`. It is then possible to solve a `System` using function from `ExtSystem` without having to _recreate_ it.

_Current status_:

- polymorphic variant: possible but runtime will be slower
- _standard_ variant & GADT: without modifying the base type, it is possible to create a new type like:

```auto
type t = Basic of Equation.t
       | Interval of { lo: int; e: Expr.t; hi: int }

```

This approach has three drawbacks:

- it is less memory efficient (especially if you want to extend the type multiple times)
- you have to make an explicit converted `val ext: Equation.t -> ExtEquation.t`
- it forces you to “recreate” every structure that contains an `Equation`. Here, it is a simple list but if `System` was a more complex structure (eg. graph) it could have a high cost.

**Mini conclusion**  
The two features are more or less already implemented by polymorphic variant. My concern about them is they are too general for what I want: I do not need arbitrary variants but just more flexibility over a set of well defined variants.

I can imagine two ways to improve this:

- add an optimization pass that will make polymorphic variants to use the same representation as standard variant if the set is finite and well know at compile time;
- add more flexibility to standard variants with a mechanism of `subtype of` and `supertype of`

Regards,  
Frédéric Recoules