I'm into PL(T) stuff and I've gotten tired about hearing about Jai. One thing I like is Jai adopting the SPAD X-form (Chi-form); he (mis)attributes it to Sean B

I'm into PL(T) stuff and I've gotten tired about hearing about Jai. One thing I like is Jai adopting the SPAD X-form (Chi-form); he (mis)attributes it to Sean Barret: The syntax name: type = value; specifies that a variable named name is of the type type and is to receive the value value Where the inferred/imperative-assignment form is a visual reduction: name : type = expr name := expr It has the lovely property that if you elide the type expression the variable gets an inferred type. If you keep the type expression, then the language has both a type-expression for type-checking and type of the value-expression for type-inference; then, the PL can be designed in one of a few ways: 1. If the type expression mismatches the type of the value-expression, fail; 2. If the type expression can be unified with the type of value-expression, keep the unified; or, 3. If the value expression can be coerced to the type expression, keep the type expression. SPAD used the second behavior and it was the bees-knees. This was especially true since SPAD supported refinement (quotient) types, so you could do things like this: name : int(-2 < n and n <= 10) = ... complex expression that we can't prove is in the range (-2, 10] ...; ... and this would fail to compile.