haskelllambdafunctional-programmingk-combinators-combinator

How to type the simply typed lambda calculus term (S K K)


I am attempting to implement a simply typed lambda calculus type checker. When running sanity tests I tried typing (S K K) and my type checker throws this error:

TypeMismatch {firstType = t -> t, secondType = t -> t -> t}

The offending term is clearly the (S K K)

(\x:t -> t -> t.\y:t -> t.\z:t.x z (y z)) (\x:t.\y:t.x) (\\x:t.\y:t.x)

I think the problem arises from a lack of polymorphism because when I type check this haskell code it works fine:

k x y = x
s x y z = x z (y z)
test = s k k -- type checks

but if I specialize the type:

k :: () -> () -> ()
k x y = x
s :: (() -> () -> ()) -> (() -> ()) -> () -> ()
s x y z = x z (y z)
test = s k k -- doesn't type check 

Just for reference my type system is a simple as it gets:

data Type = T | TArr Type Type

full source


Solution

  • I will steal the ideas from a previous answer of mine to show how to ask ghci your question. But first I am going to reformulate your question slightly.

    In Haskell, we have

    s :: (a -> b -> c) -> (a -> b) -> (a -> c)
    k :: a -> b -> a
    

    and the question we want to ask is "What do these types look like after type-checking s k k?". More to the point, if we rewrite them with distinct unification variables,

    s :: (a -> b -> c) -> (a -> b) -> (a -> c)
    k :: d -> e -> d
    k :: f -> g -> f
    s k k :: h
    

    then the question becomes a unification one: we are trying to unify the type of s with the type it's being used at -- namely (d -> e -> d) -> (f -> g -> f) -> h. Now that we have a unification question in hand, we can ask in the format showed in my other answer:

    > :{
    | :t undefined
    | ::   ((a -> b -> c) -> (a -> b) -> (a -> c))
    |    ~ ((d -> e -> d) -> (f -> g -> f) -> h)
    | => (a, b, c, d, e, f, g, h)
    | :}
    undefined
    ::   ((a -> b -> c) -> (a -> b) -> (a -> c))
       ~ ((d -> e -> d) -> (f -> g -> f) -> h)
    => (a, b, c, d, e, f, g, h)
      :: (f, g -> f, f, f, g -> f, f, g, f -> f)
    

    And now we can see why your version doesn't work: in your version, you've instantiated all polymorphic variables to the base type T; but since b ~ g -> f, e ~ g -> f, and h ~ f -> f are manifestly arrow types, that certainly isn't going to work! However, any choices for f and g will work if we respect the substitution above; in particular if we choose f ~ T and g ~ T, then we have

    s :: (T -> (T -> T) -> T) -> (T -> (T -> T)) -> (T -> T)
    k1 :: T -> (T -> T) -> T
    k2 :: T -> T -> T
    s k1 k2 :: T -> T