Typed Combinators

Posted on 2012-12-01 by Chris Warburton

How can we specify types without using variables? We can create Universal languages without variables by using combinators. Can we create a universal set of combinators for types? Probably. What would they look like? Well, let’s focus on dependent types, since they’re the most interesting. There’s an extension of untyped Combinatory Logic called Illative Combinatory Logic which adds types and annotations. In the paper ‘Systems of Illative Combinatory Logic Complete For First-Order Propositional And Predicate Calculus’ by Barendregt, Bunder and Dekkers, there are a few different systems considered; they all have the S and K combinators familiar from Schoenfinkel:

data UnsafeCom = cK
               | cS

This syntax looks like Haskell, but I’ll actually be using [Idris] 1. It looks similar to Haskell, but has dependent types. Since Idris uses ‘S’ as the ‘successor’ function for Peano-style Natural numbers, I’ve prefixed my constructors with ‘c’ for Combinator. The reason they’re ‘Unsafe’ is because, at the moment, we’re not doing any type-checking.

We need to add two new combinators for the type system, L and Ξ (which I’ll shamefully write as X):

                | cL
                | cX

I’ll explain these individually below. While the raw combinators are all in place, life is easier if we add some extra, redundant combinators to help with our notation. These are:

We can, as usual, apply one combinator to another:

                | (@) UnsafeCom UnsafeCom
infixl 10 @

That last line just lets us write x @ y @ z instead of ((@) ((@) x y) z.

The derived combinators can be constructed as follows:

P x y = X(Kx)(Ky)

F x y z = Xx(S(Ky)z)

G x y z = Xx(Syz)

H = S(KL)K

The Ξ combinator is clearly popular. It is a form of type annotation: ‘Ξxy’ says that ‘given an x, we can get a y’. This is actually quite powerful, since it can denote subtyping (x is a subtype of y), dependent functions like Gxyz, which sends any input to ‘z’ through ‘y’ as well, sending the resulting type to G for annotation. Non-dependent functions are typed with F (or Gx(Ky)z).

The type of types is L, so ‘Lx’ tells us that ‘x’ is a type. By carefully restricting what we are allowed to derive, we can avoid dangerous type-of-type-of-type scenarios (tackled with ‘universes’ in other systems). For example, if a function takes types as arguments and return values, we don’t annotate it directly; we only annotate its argument and result, since they fit in the level described by L.

Okay, time to see how these work. There are no new beta-reduction rules, so we just have the familiar S and K rules:

reduce     (cK @ x @ y) = x
reduce (cS @ x @ y @ z) = x @ z @ (y @ z)
reduce          (x @ y) = (reduce x) @ (reduce y)
reduce                x = x

Now we can add our typing rules. These take the form of natural deduction rules, which we encode as dependent function types. The idea is that we have a ‘context’ of known terms, which we can use to construct new terms. The construction rules are functions from contexts to terms; however, this is similar enough to Idris’s type-checker that we can keep the context implicit.

Here we make a Typed datatype which wraps ‘unsafe’ combinators. By making the constructors dependent functions, we can enforce our rules:

data WellTyped : UnsafeCom -> Set where

The first typing rule is that anything in the context can be derived. Since the Combinatory Logic context is the same as the Idris context, this is just the identity function:

  Id : WellTyped c -> WellTyped c

The next rule is that beta-reduction of a well-typed term gives us a well-typed term. Here x = y is a type. This is common in dependently typed programs; it acts as proof that the left and right are identical, since it’s only constructor is refl x : x = x. Without a value of this type, we can’t run the function:

  Beta : WellTyped c -> (reduce c = c') -> WellTyped c'

Now the rules become specific to the system we’re using. The following rules apply to the ‘IP’ system, which uses the P and H combinators for convenience.

cP @ x @ y encodes that x implies y. Therefore, given cP @ x @ y and x we can imply y; decoding the information in the type:

  Pe : WellTyped (cP @ x @ y) -> WellTyped x -> WellTyped y

We can also go the other way. If the existence of x would imply y, and x is a proposition (encoded as cH @ x) then we can derive cP @ x @ y. Because x may not exist, we encode if x then y as a function taking x as an argument. This is the standard way to construct implications in type theory:

  Pi : (WellTyped x -> WellTyped y)
       -> WellTyped (cH @ x)
       -> WellTyped (cP @ x @ y)

Finally if, given a proposition x, y is a proposition, then cP @ x @ y is a proposition:

  PH : (WellTyped x -> WellTyped (cH @ y))
       -> WellTyped (cH @ x)
       -> WellTyped (cH @ (cP @ x @ y))

This lets us use propositional logic with combinators; however, it’s a far cry from the rich type system that we want. The next- most-sophisticated system is called ‘IΞ’ and makes direct use of the Ξ and L combinators.

If having an x implies having a y, and v is an x, then v is also a y:

  Xe : WellTyped (cX @ x @ y)
          -> WellTyped (x @ v)
          -> WellTyped (y @ v)

If, given a of type x, a has type y, then x is a sub-type of y:

  Xi : (WellTyped (x @ a) -> WellTyped (y @ a))
          -> WellTyped (cL @ x)
          -> WellTyped (cX @ x @ y)

If, given a of type x, we know ya is a proposition, then x being a sub-type of y is also a proposition:

   XH : (WellTyped (x @ a) -> WellTyped (cH @ (y @ a)))
          -> WellTyped (cL @ x)
          -> WellTyped (cH @ (cX @ x @ y))

This is more powerful since we can talk about the relationships between types, but we still don’t get a recognisable type-system since, for example, we don’t really have functions. That’s what system ‘IF’ brings to the table.

If z is a function from x to y, and v has type x, then zv has type y:

  Fe : WellTyped (cF @ x @ y @ z)
       -> WellTyped (x @ v)
       -> WellTyped (y @ (z @ v))

If, given a of type x, za has type y, then z has type x -> y:

  Fi : (WellTyped (x @ a) -> WellTyped (y @ (z @ a)))
       -> WellTyped (cL @ x)
       -> WellTyped (cF @ x @ y @ z)

If, given a of type x, y is a type, then x -> y is a type:

  FL : (WellTyped (x @ a) -> WellTyped (cL @ y))
       -> WellTyped (cL @ x)
       -> WellTyped (cL @ (cF @ x @ y))

These are non-dependent functions though. To get a dependent type system with combinators requires the impressive ‘IG’ system:

If z has an input type x and an output type given by the function y, and v has type x, then zv has type yv:

  Ge : WellTyped (cG @ x @ y @ z)
       -> WellTyped (x @ v)
       -> WellTyped (y @ v @ (z @ v))

If, given an a of type x, za has type ya, and x is a type, then z is a dependent function:

  Gi : (WellTyped (x @ a) -> WellTyped (y @ a @ (z @ a))
       -> WellTyped (cL @ x)
       -> WellTyped (cG @ x @ y @ z)

If, given an a of type x, ya is a type, and x is a type, then the dependent function of x and y is a type:

  GL : (WellTyped (x @ a) -> WellTyped (cL @ (y @ a)))
       -> WellTyped (cL @ x)
       -> WellTyped (cL @ (cG @ x @ y))

These simple implementations of four typed combinatory logic systems have been interesting me for the past week or so. A current limitation is that datatypes must be defined as axioms. I’m trying to overcome that with a simple porting of GADTs to combinatory forms. It’s looking promising so far :)