ML Type Theory in Plain English

This is not simple English but I think that it is plain English.

As a teenager I had a proof that there were an infinite number of twin primes. I showed it to Tom Apostle who kindly wrote a small “FALSE” in the middle of the page. Of course, he was right, but it sort seemed like a small quibble. Just a few years later as I studied symbolic logic I reviewed my proof and saw that I had invalidly transposed two adjacent implicit quantifiers. Order of quantifiers is vital and now I object to omitting them. See Keynes quote.

In OCaml “f x” means about what “f(x)” conventionally means. When I type “let f x = x;;” to OCaml’s top level REPL program it replies “val f : 'a -> 'a = <fun>” which means that it assigns the type 'a -> 'a to f. That, in turn, means that the type of f x is the same as the type of x. To understand more complex examples I posit that this can be said in the following form:

or ‘f’ appears freely in the above which captures what the system learns about f. I hope the pattern is clear. We will elaborate the pattern and eventually define it precisely.

Small latin letters denote values, Greek letters denote types and x:α means that x is of type α. We quantify both values and types. All my Greek type identifiers will be quantified. OCaml has its own notation for what they call ‘type variables’ but the OCaml type expressions omit quantifiers and I do not understand them.

I lean heavily on my experience with First-order logic.

“let f (p, q) = p q;;” yields “val f : ('a -> 'b) * 'a -> 'b = <fun>” or better “val f : (('a → 'b) * 'a) -> 'b = <fun>”.

Applying our pattern we get:
∀α ∀β ∀p ∀q ((p:(α → β) ⋀ q:α) ⊃ (f (p, q)):β).

With the fixed width font I quote OCaml’s way of describing types. I use the non ASCII symbols for a notation that I understand. In each case I try to make the two look as much alike as possible.

I think we must unpack the Curry-Howard correspondence.