5 ms·

> Typedefs is similar to protocol-buffers, thrift and many more ... however, it is based on a theory of algebraic data types and aims to be a more natural fit f

> Typedefs is similar to protocol-buffers, thrift and many more ... however, it is based on a theory of algebraic data types and aims to be a more natural fit for users of proof assistants and purely functional, strongly typed programming languages I think an IDL with strong support for ADTs is a great idea. Reminds me of ATD for OCaml [1]. Someone posted here this other project that seems to share similar goals [2]. A long shot, but I wonder if anyone here may be familiar with any two pairs of these projects to compare and contrast. 1: https://github.com/ahrefs/atd https://github.com/ahrefs/atd 2: https://preserves.gitlab.io/preserves/preserves.html https://preserves.gitlab.io/preserves/preserves.html

wires 6y 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.
- chrischen 6y ago
  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?
- tonyg 6y ago
  Preserves has an equational theory. It's untyped, though, like S-expressions, JSON and XML.

wires 6y 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.

chrischen 6y ago
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?
tonyg 6y ago
Preserves has an equational theory. It's untyped, though, like S-expressions, JSON and XML.