3 ms·

I don't think I understand the reasoning behind the ADT. Isn't a 'type' just a set of predicates applied to arguments at compile time and/or at runtime? Why not

I don't think I understand the reasoning behind the ADT. Isn't a 'type' just a set of predicates applied to arguments at compile time and/or at runtime? Why not just define a Caramel convention where you specify typed functions using a fancy argument list, in this case, a list of lists of predicate functions? Untyped functions would take a different shape of argument.

deleted 11y ago
[deleted]
LightMachine 11y ago
The point of ADT syntax is to allow deriving many functions on different data structures automatically. For example, lists and some functions can be defined as: cons = (x list cons nil -> (cons x (list cons nil))) nil = (cons nil -> (id nil)) map = (f list cons -> (list (comp cons f))) head = (list -> (list (a b -> a) nil)) tail = (list cons nil -> (list (h t g -> (g h (t cons))) (const nil) (h t -> t))) zip_with = (f a b -> ((left a) (right f b))) left = (foldr (x xs cont -> (cont x xs)) (const [])) right = (f -> (foldr (y ys x cont -> (cons (f x y) (cont ys))) (const (const [])))) length = (flip comp const) The very same definitions could be written more tersely as just: List = #{Cons Type * | Nil} cons = (Ctor 0 List) nil = (Ctor 1 List) head = (Getter 0 0 List) tail = (Getter 0 1 List) zip_with = (ZipWith List) length = (Size List) Where Ctor/Getter/ZipWith/Size are proper derivers. It is possible because all the information you need is there, but it is very hard to come up with those derivers and I currently only have some very bloated derivers for Scott encoded structures, and none for Church encoded structures yet.
- tikhonj 11y ago
  Coincidentally, if you're thinking of adding pattern matching to the underlying calculus (not just as syntactic sugar), the book I mentioned in another comment (Pattern Calculus) is worth a look. The author explores what a language could look like of patterns were first-class and used to express arbitrary computations. At the very least, it could be fun to have an extended version of the system (or a plugin of some sort, perhaps) using his ideas about pattern matching.
- javajosh 11y ago
  Cool, thanks for the explanation. I guess I'm a little confused by the desire to "derive many functions on different data-structures automatically". What's the independant variable in this meta-function? It makes little sense to "automatically" define a type when one could argue that programming is the act of defining types! I guess my claim is that I want to express type as a named list of predicates that fold into a single predicate over 'and'.

deleted 11y ago

[deleted]

LightMachine 11y ago

The point of ADT syntax is to allow deriving many functions on different data structures automatically. For example, lists and some functions can be defined as: cons = (x list cons nil -> (cons x (list cons nil))) nil = (cons nil -> (id nil)) map = (f list cons -> (list (comp cons f))) head = (list -> (list (a b -> a) nil)) tail = (list cons nil -> (list (h t g -> (g h (t cons))) (const nil) (h t -> t))) zip_with = (f a b -> ((left a) (right f b))) left = (foldr (x xs cont -> (cont x xs)) (const [])) right = (f -> (foldr (y ys x cont -> (cons (f x y) (cont ys))) (const (const [])))) length = (flip comp const) The very same definitions could be written more tersely as just: List = #{Cons Type * | Nil} cons = (Ctor 0 List) nil = (Ctor 1 List) head = (Getter 0 0 List) tail = (Getter 0 1 List) zip_with = (ZipWith List) length = (Size List) Where Ctor/Getter/ZipWith/Size are proper derivers. It is possible because all the information you need is there, but it is very hard to come up with those derivers and I currently only have some very bloated derivers for Scott encoded structures, and none for Church encoded structures yet.

tikhonj 11y ago
Coincidentally, if you're thinking of adding pattern matching to the underlying calculus (not just as syntactic sugar), the book I mentioned in another comment (Pattern Calculus) is worth a look. The author explores what a language could look like of patterns were first-class and used to express arbitrary computations. At the very least, it could be fun to have an extended version of the system (or a plugin of some sort, perhaps) using his ideas about pattern matching.
javajosh 11y ago
Cool, thanks for the explanation. I guess I'm a little confused by the desire to "derive many functions on different data-structures automatically". What's the independant variable in this meta-function? It makes little sense to "automatically" define a type when one could argue that programming is the act of defining types! I guess my claim is that I want to express type as a named list of predicates that fold into a single predicate over 'and'.