Antoine Leblanc

This is a short continuation of Outlining type checking for your toy language (and many others). In my previous post, I introduced a way of classifying type checking and type inference as a transformation on an abstract syntax tree whose type system was a type parameter:

{-# LANGUAGE FunctionalDependencies #-}

class Monad m => Typecheck m l t | l t -> m where
    typecheck :: l t -> m t

class (Typecheck m l t) => Infer m l t | l t -> m where
    infer :: l (Maybe t) -> m (l t)

I was using a lambda calculus whose type system I had made into a type parameter:

data LambdaCalc t
	= Var String
	| Apply (LambdaCalc t) (LambdaCalc t)
	| Abstract (String, t) (LambdaCalc t)
	deriving (Functor, ...)

What I was walking through was the reasoning for doing things this way, especially how it means we can separate the stages of analysis really cleanly.

But hang on, what if we start treating the toy language's type system as the toy language?

---

If we bring the complexity of the type system up to something like System F Omega, we can ask the questions previously asked for the lambda calculus itself but about our type system:

1. forall introduces type variables to type expressions.
2. Function is a constant with kind Type -> Type.
3. We have a notion of kindedness, as in (2), where Function has a kind instead of a type.
4. There are various reduction rules we can pull from for how to evaluate types during type checking.

We can follow through on this with something along these lines:

type KindcheckM = ...

data Kind
    -- AKA `*`, or `Type`. The type of types.
    = MyType 
    | Arrow Kind Kind

data MyTypeSystem k 
    = Forall (String, k) MyTypeSystem
    | Function (MyTypeSystem k) (MyTypeSystem k)
    | TypeVar String
    | TypeCon String

instance Typecheck KindcheckM MyTypeSystem Kind where
    typecheck :: MyTypeSystem Kind -> KindcheckM Kind
    typecheck expr = ...

instance Infer KindcheckM MyTypeSystem Kind where
    infer :: MyTypeSystem (Maybe Kind) -> KindcheckM (MyTypeSystem Kind)
    infer = ...

Can we take it a step further? Well, not like this. Kindedness does not at this point have the complexity we would want to be able to apply those same questions to it and get satisfying answers.

But if we were to step up the type system to a Dependent one, one where general expressions can live in type land we can tie this up in a way that fits the style I've been going for here. We will need one fancy tool so that we can feed host types to themselves:

newtype Fix (f :: * -> *) = Fix {unfix :: f (Fix f)}

Fix feels a bit like a form of dark magic, but it can be thought of doing the same thing we do when we build a recursive function. Once again this is a simplification, but one to smooth past complexity and maintain focus.

When we have Fix, it might tempt to just declare LambdaCalc (Fix LambdaCalc) as a dependently typed calculus. However there's a few modifications to the original I would like to do to:

-- A bit of housekeeping: I've made variables and constants distinct
-- types and added constants to the lambda calculus because now, they
-- not only represent "runtime" values but can also represent compile
-- time ones. `Function` now occupies a similar space in the language
-- as any user-defined constants. And some variable `a` could mean a
-- type variable or a variable that .
data Variable = ...
data Constant = ...

-- A lambda calculus with variables, constants, and the type system 
-- made into parameters so we can focus on the important things in 
-- life like good tea and time with friends and loved ones.
data DepLambdaCalc t
	= Var Variable
	| Const Constant
	| Apply (DepLambdaCalc t) (DepLambdaCalc t)
	| Abstract (Variable, t) (DepLambdaCalc t)
	-- Okay, everything is looking fine so far. 
	-- But with dependent typing we can lift up a variable into the
	-- type system. So we need to add one more thing:
	| Lift (Variable, t) t

I've introduced Lift which can be thought of as: abstract but it lifts the variable up into the type system. This is not necessarily the correct way of doing things, or the best explanation, but it's how I'm doing it here. As with how I renamed $\mathrm{\lambda <!--\; -->}$ abstraction to simply Abstract, in type theory this is represented with $\mathrm{\Pi <!--\; -->}$ (capital letter pi).

With this, we can now make it fit the forms of the typeclasses and have enough space to do at least some dependent type system shenanigans smoothly:

type DepTypecheckM = ...

instance Typecheck DepTypecheckM DepLambdaCalc (Fix DepLambdaCalc) where
	typecheck :: DepLambdaCalc (Fix DepLambdaCalc) 
			  -> DepTypecheckM (Fix DepLambdaCalc)
    typecheck expr = ...

-- Not all dependent terms can have their types inferred,
-- that's just the showbiz of complex type theories.
instance Infer DepTypecheckM DepLambdaCalc (Fix DepLambdaCalc) where
    infer :: DepLambdaCalc (Maybe (Fix DepLambdaCalc))
          -> DepTypecheckM (DepLambdaCalc (Fix DepLambdaCalc))
    infer expr = ... 

We have now fed the lambda calculus to itself as its own type system. At least, I've shown a way we could do that. I have not written type checker code in a long time, it takes a lot of effort. But, the framework has been successfully turned onto itself.