8/30/21
Some reminders of what is well-formed in our Mini-M, and what our typing algorithm will likely do:
- variables, e.g. a, b, c, x, y, aVariable, etc. are well-formed, but they do not have types on their own. Each one needs a value in the environment (i.e. in the assumptions). But we starting from an empty environment. So the typing algorithm will reject them
- constants of known type e.g. 1,2,3 ... True, False etc. are well-formed and have a type
- constants of unknown type e.g. A,B, C, K, AConstant are well formed, but they do not have types on their own. Each one needs a value in the environment (i.e. in the assumptions). But we starting from an empty environment. So the typing algorithm will reject them
- applications e.g. (λa.a True), (True False), (7 True), etc. may be well-formed, and may have a type (depending on the types of their sub-expressions). But there is something to watch out for here. Applications are marked or identified by having parentheses around the function and the argument e.g. (λa.a True). This means that extra-parentheses cannot be used for style or attempted disambiguation. For example, (λa.(a) True) or ((λa.a )True) will be rejecting as ill-formed. Once the parser sees the brackets it is expecting an application. But these sub-expressions are not applications (they lack either a function expression or an argument expression).
- unannotated lambdas e.g. λa.a, λx.(x y) etc. are well-formed and may have have a type (depending on the types of their sub-expressions).
- annotated lambdas e.g. λa:I.a, λx:I->B.(x y) etc. are well-formed and may have have a type (depending on the types of their sub-expressions). But there is something to watch out for here. The typing sub-expression associates to the right so
λx:I->B->I->I->I.(x y) means λx:I->B->(I->(I->I))).(x y)Well, you may ask, what happens if I would like
λx:((I->B)->I)->(I->I).(x y) )The answer is: you can used parentheses as you wish in typing subexpression e.g. λx:((I->B)->I)->(I->I).(x y) ), λx:((((B)))).x are all fine. When the parser is parsing types, it accepts (perhaps disambiguating) brackets. There is no possibility of confusion with an application. The context is reading a type, not reading a full lambda calculus expression.
- annotated lambdas, more. Lambdas can be annotated with well-constructed type expressions, even containing type variables. But they cannot be annotated with a universally quantified genuine type scheme i.e. one starting with ∀. The parser will reject these as not being well-formed.
- you can use the backslash \ for λ (as Haskell does). The parser here will parse either of them.
- unannotated let expressions i.e. of form let <term variable>= <expression1> in <expression2> are fine.
- annotated let expressions i.e. of form let <term variable>:<type scheme>= <expression1> in <expression2> are also fine. <type scheme here is any type scheme including genuine type schemes with a universally quantified type with type variables (i.e. not just plain types).
No expression has a type that is a genuine type scheme with a universally quantified type with type variables
There is only one place that a full blown type scheme might appear, and that is within a let construction e.g.
let identity:∀a(a->a)=λx.x in (identity 7)
Now, the type-scheme ∀a(a->a) is not the type of the let expression, it is the type of subexpression 'identity' (or λx.x). The type of the let expression is actually, in this case, Int (which is the type of (identity 7) i.e. the second expression in the let form. Ah, you may say, what about this:
let identity:∀a(a->a)=λx.x in identity ?
Well, that has type a->a for some type variable a. But notice, there is no universal quantifier ∀. [You can try it for yourself below.]
Solving the constraints
In the earlier Junior Hindley Milner case, where all the constraints were equalities. The constraint list was confluent and the constraints could be solved in any order (in particular, from first to last). Unfortunately, when explicit and implicit constraints are introduced, the list loses its confluence and order matters. However, the algorithm in use here can look at the types in use (with every type being new) and it can convert instance constraints into equality constraints (roughly, if t1 is to be an instance of ∀<vars>t2 then t1 needs to unify with a suitably instantiated t2). At this point the constraint list again becomes confluent and can be solved first to last. The solution software below will show this in action.
A note on the type variables you might see.
There are two different algorithms that might be used here, and also the expressions might be annotated or not. If they are annotated, you, the User, might use pretty well any identifier you wish (starting with a lower-case letter) as a type variable in annotation of a let expression. So, there are plenty of possibilities for appearance either as the final type or among the constraints. However, the algorithms themselves are using certain conventions. The algorithm solving constraints one-by-one will use t0, t1, t2... etc. as the type variables with t0 as the type of the original expression. However, some of the components of a constraint may be genuine type schemas with some universally quantified variables in the type. When these are processed, the universally quantified variables (indicating polytypes) will be instantiated to ordinary type variables (monotypes) and the algorithm will use i0, i1, i, .. as instances of those type variables. So you might see as a constraint solution substitution, for example, t0:i3 ; this just means that the original expression is a monotype, of any type, and the algorithm has called that type i3.
The other algorithm uses a0, a1, a2, ... as its type variables, but it will not display its instantiations or workings for you. So, for example, it might tell you that the type of a provided expression is a1->a3 ; this means that the type is a function any type to another, where, whatever those types are, they retain their values through the entire scope they apply to.
Onward ...
Select a well-formed lambda expression. The constraint button will calculate the constraints; then it will convert the constraint list one-by-one into substitutions (if that can be done!); the value for the algebraic variable t0 will be the type of the original expression. What you want to keep your eye on is the first constraint of a line and the first substitution of the next line. The type button will give the type directly. The programs use different algorithms. They should agree on the type!