lambdacalc.scala

object LambdaCalculus {
  sealed trait Type
  case class Arrow[S <: Type, T <: Type]() extends Type
  case class Base() extends Type

  sealed trait Ctx
  case class Nil() extends Ctx
  case class Cons[X <: Type, XS <: Ctx]() extends Ctx

  sealed trait In[T <: Type, TS <: Ctx]
  case class Here[T <: Type, TS <: Ctx]() extends In[T, Cons[T,TS]]
  case class There[P <: Type, T <: Type, TS <: Ctx, V <: In[T,TS]]() extends In[T, Cons[P,TS]]

  sealed trait WellTyped[T <: Type, TS <: Ctx]

  case class Variable[
    T <: Type,
    TS <: Ctx,
    V <: In[T, TS]]() extends
  //-------------------------
    WellTyped[T, TS]

  case class Abstraction[
    S <: Type,
    T <: Type,
    TS <: Ctx,
    E <: WellTyped[T, Cons[S, TS]]]() extends
  //-----------------------------------------
    WellTyped[Arrow[S,T], TS]

  case class Application[
    S <: Type,
    T <: Type,
    TS <: Ctx,
    F <: WellTyped[Arrow[S,T], TS],
    E <: WellTyped[S, TS]]() extends
  //--------------------------------
    WellTyped[T, TS]

  def test1[T <: Type]() : WellTyped[Arrow[T,T], Nil] = Abstraction[T, T, Nil, Variable[T, Cons[T, Nil], Here[T, Nil]]]()
}