A puzzle about typing
- 20 January 2012
- Computation, Programming
While making a comment on Stackoverflow I noticed something: suppose we have a term in the $\lambda$-calculus in which no abstracted variable is used more than once. For example, $\lambda a b c . (a b) (\lambda d. d c)$ is such a term, but $\lambda f . f (\lambda x . x x)$ is not because $x$ is used twice. If I am not mistaken, all such terms can be typed. For example:
# fun a b c -> (a b) (fun d -> d c) ;;
- : ('a -> (('b -> 'c) -> 'c) -> 'd) -> 'a -> 'b -> 'd =
# fun a b c d e e' f g h i j k l m n o o' o'' o''' p q r r' s t u u' v w x y z ->
q u i c k b r o w n f o' x j u' m p s o'' v e r' t h e' l a z y d o''' g;;
- : 'a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j ->
'k -> 'l -> 'm -> 'n -> 'o -> 'p -> 'q -> 'r -> 's -> 't ->
('u -> 'j -> 'c -> 'l -> 'b -> 'v -> 'p -> 'w -> 'o -> 'g ->
'q -> 'x -> 'k -> 'y -> 'n -> 't -> 'z -> 'r -> 'a1 -> 'e ->
'b1 -> 'c1 -> 'i -> 'f -> 'm -> 'a -> 'd1 -> 'e1 -> 'd -> 's
-> 'h -> 'f1) -> 'v -> 'b1 -> 'z -> 'c1 -> 'u -> 'y -> 'a1
-> 'w -> 'x -> 'e1 -> 'd1 -> 'f1 =
</pre>
What is the easiest way to see that this really is the case?
A related question is this (I am sure people have thought about it): how big can a type of a typeable $\lambda$-term be? For example, the Ackermann function can be typed as follows, although the type prevents it from doing the right thing in a typed setting:
# let one = fun f x -> f x ;;
val one : ('a -> 'b) -> 'a -> 'b =
# let suc = fun n f x -> n f (f x) ;;
val suc : (('a -> 'b) -> 'b -> 'c) -> ('a -> 'b) -> 'a -> 'c =
# let ack = fun m -> m (fun f n -> n f (f one)) suc ;;
val ack :
((((('a -> 'b) -> 'a -> 'b) -> 'c) ->
(((('a -> 'b) -> 'a -> 'b) -> 'c) -> 'c -> 'd) -> 'd) ->
((('e -> 'f) -> 'f -> 'g) -> ('e -> 'f) -> 'e -> 'g) -> 'h) -> 'h =
</pre>
That's one mean type there! Can it be “explained”? Hmm, why _does_ `ack` compute the Ackermann function in the untyped $\lambda$-calculus?
How to comment on this blog:
At present comments are disabled because the relevant script died.
If you comment on this post on Mastodon and
mention
andrejbauer@mathstodon.xyz, I will
gladly respond.
You are also welcome to contact me directly.
Comments
I think I have an answer to the first part of the puzzle: two simple types with disjoint type variables will always unify: thinking of types as binary trees, just superimpose the two trees and read off the substitutions from the places where one tree terminates earlier than the other. When typing a term, we must do a unification for each application; if term variables are only used once then the left- and right-hand terms of any application can be given types with disjoint type variables.
I don't know about "easiest", but here's one way.
Let's think about what type inference does with such a term. For each term $s$ that occurs as a subterm or a bound variable, let $T(s)$ be the type variable associated with s during type inference. Then type inference generates equations of the two forms $$T(a) = T(b) \to T(ab)$$ and $$T(\lambda x.a) = T(x) \to T(a)$$ Now totally order occurrences of subterms by traversing the tree of occurrences generally from right to left, but where each application node is traversed before its children, and each abstraction node is traversed after its children. This totally orders the occurrences. Now since each term $s$ in a $T(s)$ occurs at most once, the total order on occurrences induces a total order on the $T(s)$ (where we also traverse any $T(x)$ for a bound variable that has no occurrence before the $T(\lambda x.a)$ that binds it).
Observe that this total order puts the left side of each equation after both terms on the right side. So the system of equations can be solved in that order.
In your example $\lambda a.\lambda b.\lambda c.(a b) (\lambda d. d c)$, the order is as follows:
T((a b) (\d. d c)) unconstrained (call it 'd) T(d c) unconstrained (call it 'c) T(c) unconstrained (call it 'b) T(d) = T(c) -> T(d c) T(\d. d c) = T(d) -> T(d c) T(a b) = T(\d. d c) -> T((a b) (\d. d c)) T(b) unconstrained (call it 'a) T(a) = T(b) -> T(a b) T(\c.(a b) (\d. d c)) = T(c) -> T((a b) (\d. d c)) T(\b.\c.(a b) (\d. d c)) = T(b) -> T(\c.(a b) (\d. d c)) T(\a.\b.\c.(a b) (\d. d c)) = T(a) -> T(\b.\c.(a b) (\d. d c))We can also use this analysis to figure out how many type variables the solution will have, by counting the number of type variables and equations (exercise).
The ack example can be given types in the polymorphic lambda calculus that will allow it to do the right thing, too.
one : forall r. (r -> r) -> r -> r suc : (forall r. (r -> r) -> r -> r) -> (forall r. (r -> r) -> r -> r) ack : (forall r. (r -> r) -> r -> r) -> (forall r. (r -> r) -> r -> r) -> (forall r. (r -> r) -> r -> r)
Also, the ack definition makes essential use of Nat (= forall r. (r -> r) -> r -> r) being a first class type. If we put in expicit instantiations:
ack m = m (Nat -> Nat) ((f : Nat -> Nat) (n : Nat) -> n Nat f (f one)) suc
For one, we eliminate m over Nat -> Nat, but that's not an insurmountable problem. The problem is the \f n -> n f (f 1) expression. That is the suc case, so we take f : T -> T, and use it to produce a T -> T. We start by abstracting over n, which must have type T. Then, we need to eliminate n as a natural using f as the successor function. This means that n : (T -> T) -> T -> T. So we need T ~ (T -> T) -> T -> T, but this is impossible without recursive types or an encoding thereof. System F can handle it using impredicativity, and the untyped lambda calculus can handle it because it just doesn't care, but simple types are going to fall down, and not allow you to call ack with the values you want.
Maybe it's possible to do similar tricks to multiplication. That is:
isn't available, but:
is. But I couldn't come up with an obvious variation of your above code that qualified.
[sourcecode gutter="false"] # type nat = { iter : 'a . ('a -> 'a) -> 'a -> 'a };; # let one = { iter = fun f x -> f x };; # let succ n = { iter = fun f x -> n.iter f (f x) };; # let ack m = m.iter (fun f n -> n.iter f (f one)) succ;; val ack : nat -> nat -> nat = <fun> # let to_int n = n.iter ((+) 1) 0;; # let rec of_int = function 0 -> { iter = fun f x -> x } | n -> succ (of_int (n - 1));; # to_int (ack (of_int 2) (of_int 3));; - : int = 9 </pre>
@gasche: Very good, I forgot ocaml had polymorphic records of this kind.