Type inference for a scala combinator calculus data model

Question

I'm trying out a very light-weight encoding of combinator calculus in scala. Initially, I'm simply implementing the S and K combinators, application and constant values. Later I hope to lift scala functions in and allow evaluation of an expression as a scala function. However, that's for later. Here is what I have so far.

/** Combinator expression */
sealed abstract class CE

/** Application: CE| (x y) <=> LC| (x:(A=>B) y:A) : B */
case class Ap[A <: CE, B <: CE, X](e1: A, e2: B) extends CE

/** A raw value with type */
case class Value[T](v: T) extends CE

/** Some combinator */
sealed abstract class Comb extends CE

/** The S combinator: CE| S x y z
 *                    LC| λx:(A=>B=>C).λy:(A=>B).λz:A.(x z (y z)) : C
 *  S : ∀A.∀B.∀C. (A => B => C) => (A => B) => A => C
 */
case object S extends Comb
/** The K combinator: CE| K x y
 *                    LC| λx:A.λy:B.x:A : A
 *  K : ∀A => ∀B => A
 */
case object K extends Comb

Now I would like to do some type inference over this. For simplicity of implementing small- and large-step reduction, the data model is untyped, so I'd like types to be external to this structure. Let's introduce something to hold the type information.

trait TypeOf { type typeOf }

The Value type is easy.

implicit def typeOfValue[T](vt: Value[T]) : TypeOf =
    new TypeOf { type typeOf = T }

Application is a little more tricky, but basically boils down to function application. Let's introduce a type ⊃ for combinator application, to avoid confusion with normal scala application.

/** Combinator application */
class ⊃[+S, -T]

implicit def typeOfAp[Ap[A, B], A <: CE, B <: CE], X, Y](Ap(A, B)
  (implicit aIsFXY: A#typeOf =:= (X⊃Y), bIsX: B#typeOf =:= X) : TypeOf =
      { type typeOf = Y }

This is where I get stuck. I need to represent the type of the S and K combinators. However, they are universally quantified types. You don't know their actual type until you start applying them. Let's take K as an example.

(K x:X y:Y) : X
(K x:X) : ∀Y.Y => X
(K) : ∀X.x => ∀Y.Y => X

The first couple of times I tried to work with this, I make K parameterised as K[X, Y], but this is (catastrophically) insufficiently polymorphic. The type of K should be waiting for the type of the first argument, and then of the next. If you apply K to just one value, then the type of the next argument should not yet be fixed. You should be able to take (K x:X) and apply it to a string, or to an int or whatever type you like.

So my problem is how to write the implicit that generates the typeOf for S and K, and how to handle the ∀-quantified types correctly. Perhaps I want something like this?

implicit def typeOfK(k: K.type): TypeOf = { type typeOf = ∀[X, X ⊃ (∀[Y, Y⊃X])] }

However, I'm not sure how I should be writing the ∀ type to do the plumbing. I've a feeling that in addition to getting ∀ right, there will be a second implicit for typeOfAp to handle the A#typeOf =:= ∀[...] case in addition to the exiting A#typeOf =:= ⊃[...] one.

Thanks,

Matthew

Answer 1

Does this help?

trait λ {
    type ap[X] <: λ
}

type K = λ {
    type ap[X<:λ] = λ {
        type ap[Y<:λ] = X
    }
}

type S = λ {
    type ap[X<:λ] = λ {
        type ap[Y<:λ] = λ {
            type ap[Z<:λ] = X#ap[Z]#ap[Y#ap[Z]]
        }
    }
}

type I = S#ap[K]#ap[K]

def ap[X<:λ,Y<:λ](x:X,y:Y): X#ap[Y]