I don't think I've come across term-rewriting before. There's an example in their wiki page for inserting into a BST:
> nonfix nil;
> insert nil y = bin y nil nil;
> insert (bin x L R) y = bin x (insert L y) R if y<x;
> = bin x L (insert R y) otherwise;
> foldl insert nil [7,3,9,18];
bin 7 (bin 3 nil nil) (bin 9 nil (bin 18 nil nil))
Lines beginning with > are what you type; the extra line is the evaluated response.
So the language is dynamically typed and it seems you don't need to declare constructor symbols that take arguments. A constructor seems to be something that is irreduceable according to the rules already defined, whereas a function is something with reduction rules available.
I'm not sure I agree with the rationale for the dynamic typing. The designer says it means the language supports an arbitrary degree of polymorphism, but obviously it means it accepts invalid programs with undefined behavior. I think by adopting a Typescript style system you'd get huge advantages ("Typescript-style" meaning structural, adhoc and evolving towards correctness, rather than meeting the wrong design constraints upfront). But I'm still not at all sure my intuitions for this language are useful.
Anyway that's my review in five minutes. I hope someone writes something relevant here.
> but obviously it means it accepts invalid programs with undefined behavior.
Congratulations! This is the most entitled sentence in all of computing. The prize ceremony will be held at your house, tomorrow. I'll be casting a statue of gold for you, but first I have to rebuild all the software between me and the CNC machine in Coq or Typescript.
On a barely related note: When did Typescript's type system become some shining example of type systems? It's super basic and you can do almost nothing with it. It's not as basic as Go's type system, but it's really very sparse.
Not saying it’s particularly amazing, but its ad-hoc structural product types are really nice. I would really enjoy if a language had TS-style ad-hoc structural products and Ocaml-style ad-hoc structural sums. This would allow for very lightweight type-level documentation.
I can no longer edit my original comment, so I'll take the opportunity to pull back a little bit and say I don't wanna make it seem like I think TS's type system is useless, but rather it's nothing special.
That said, I guess it's much better than nothing at all (JS).
Basically every language has ad-hoc products in the form of tuples. They aren’t structurally typed in ocaml, which is the interesting part. Typescript has labeled products that have similar subtyping rules to ocaml’s anonymous sum subtyping rules. Eg {x:a, y:b} < {x:a}.
So the language is dynamically typed and it seems you don't need to declare constructor symbols that take arguments. A constructor seems to be something that is irreduceable according to the rules already defined, whereas a function is something with reduction rules available.
I'm not sure I agree with the rationale for the dynamic typing. The designer says it means the language supports an arbitrary degree of polymorphism, but obviously it means it accepts invalid programs with undefined behavior. I think by adopting a Typescript style system you'd get huge advantages ("Typescript-style" meaning structural, adhoc and evolving towards correctness, rather than meeting the wrong design constraints upfront). But I'm still not at all sure my intuitions for this language are useful.
Anyway that's my review in five minutes. I hope someone writes something relevant here.