Quote from AntC on October 6, 2022, 8:04 am

To riff on Wadler's opening example in that Theorems for free! paper ... Assuming the reader has domain knowledge of TTM:

• Wadler's example is working on (the types of) Lists, and the sequence of elements.
• We know that unlike Lists, TTM tuples are unordered.
• For the sake of illustration, I'll assume the operators' names are cryptic/in some foreign language.
• We see the types of two operations on tuples take two not-necessarily-the-same-typed-tuples and produce a not-necessarily-the-same-typed-tuple result. None of the arguments/results are fixed to the empty tuple -- but we can't rule out they might produce an empty tuple for some combinations of arguments.
• We see those type specs don't mention any specific attribute names nor attribute types.
• So those operations can only be doing a few possible things: producing a result that has only the attributes specific to one operand; producing a result that has only the attributes in common -- but the values from only one. (Because if it could only have the values from both somehow if they had the same value -- but that would require the attribute-values be same type -- and the operators' types don't specify that.) Produce a result that's some combo of the above -- such as a result that has the attributes specific to one union specific to the other but none of the in-common attribs.
• If you further see that the types of P(t1, t2) === R(t1, R(t1,t2)); you can 'solve' that type-as-proposition: both operators are non-commutative; R( ) must be the operation that removes from its first operand the attributes in common with the second; P( ) must be the operation that projects its first operand on the attribs in common with the second.
• The type of our third operation requires that for E(t1, t2) we must have type P(t1, t2) === TUP{ }. And again its args are not-necessarily-same-typed-tuple; its result is not-necessarily-same-typed as either arg. We might ask the compiler the type of E(t1, TUP{ }) and be told it's t1; and ask the type with the args flipped, and be told also t1. Then we can infer what E( ) must be, purely from its type.

You're never going to make sense of invocations of PROJECT(), RENAME(), EXTEND(), if you don't know _what_ those things are.

I haven't seen any of the implementation code for those hypothesised operations.

I've assumed domain knowledge of TTM. I've assumed you know how to 'read' types and prod the compiler to do some type inference. I haven't expected any specialist knowledge about calling modes or ad-hoc syntax for arguments -- there isn't any.

(You might try evaluating some example expressions, and discover you can put undefined values in the r.h. arg to P( ), R( ) but not E( ). You might even find variants of P( ), R( ) with very similar types, but the second arg being a 'phantom' -- used only for its type, not its value -- which you can tell purely from the operations' type.)