[nukifw]

In the specific case of OCaml, this is also possible using indexing and GADTs or polymorphic variants. But generally, referencing as its own type serves different purposes. From my point of view, distinguishing between sum branches often tends to result in code that is difficult to reason about and difficult to generalise due to concerns about variance and loss of type equality.

[ackfoobar]

Unless you reach an unsound part of the type system I don't see how. Could you provide an example?

[nukifw]

- You can use GADTs (https://ocaml.org/manual/5.2/gadts-tutorial.html) and indexes to give a concrete type to every constructors:

  ```ocaml
  type _ treated_as = 
   | Int : int -> int treated_as
   | Float : float -> float treated_as

  let f (Int x) = x + 1 (* val f : int treated_as -> int *)
  ```

- You can use the structurale nature of polymorphic variants (https://ocaml.org/manual/5.1/polyvariant.html)

  ```ocaml
  let f = function 
  | `Foo x -> string_of_int (x + 1) 
  | `Bar x -> x ^ "Hello"
  (* val f : [< `Foo of int | `Bar of string] -> string` *)

  let g = function
  | `Foo _ -> ()
  | _ -> () 
  (* val g : [> `Foo of 'a ] -> unit *)
  ```

(Notice the difference between `>` and `<` in the signature?)

And since OCaml has also an object model, you can also encoding sum and sealing using modules (and private type abreviation).

[ackfoobar]

Oh if you use those features to express what "sum type as subtyping" can, it sure gets confusing. But it's not those things that I want to express that are hard to reason about, the confusing part is the additions to the HM type system.

A meta point: it seems to me that a lot of commenters in my thread don't know that vanilla HM cannot express subtypes. This allows the type system to "run backwards" and you have full type inference without any type annotations. One can call it a good tradeoff but it IS a tradeoff.

[nukifw]

Yes and my point was, when you want what you present in the first comment, quoting my post, you have tools for that, available in OCaml. But there is cases, when you do not want to treat each branch of your constructors "as a type", when the encoding of visitors is just rough. This is why I think it is nice to have sum type, to complete product type. So i am not sure why we are arguing :)

[ackfoobar]

> So i am not sure why we are arguing :)

I think we agree on a lot of points. The rest is mostly preferences. Some other comments in my thread though...

[nukifw]

Ok! (BTW, thanks for the interaction!)