|
|
|
|
|
by wires
2050 days ago
|
|
(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. |
|