Hacker News new | ask | show | jobs
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.
2 comments

Preserves has an equational theory. It's untyped, though, like S-expressions, JSON and XML.
Are better examples on the TODO list? I read through the basic examples but felt like it skipped over some things (like the specialized types, and why the examples don't work when compiling to ReasonML). Will I be able to make JSON decoders/serializers of primitive types just like with ATD gen?