(co-author of typedefs here): having real ADTs with sum/coproduct type constructors is indeed one of the motivations behind typedefs. re [1] the language behin

(co-author of typedefs here): having real ADTs with sum/coproduct type constructors is indeed one of the motivations behind typedefs. re [1] the language behind ATD seems really similar to typedefs (not surprising, it is the "sane" choice) I need to give it a deeper look to point out more subtle differences. Additionally since we developed in Idris we provide proofs that `serialized . deserialize = id`, which is not possible in OCaml. regarding [2], it's the same idea, except that doesn't follow any well establish type theory or other mathematical structure as the basis of it's language: Compound = Record | Sequence | Set | Dictionary This is mathematically already quite complicated.