tel

Simpler, Easier!

Lennart Augustsson, Oct 25, 2007

In a recent paper, Simply Easy! (An Implementation of a Dependently Typed Lambda Calculus), the authors argue that type checking a dependently typed language is easy. I agree whole-heartedly, it doesn't have to be difficult at all. But I don't think the paper presents the easiest way to do it. So here is my take on how to write a simple dependent type checker. (There's nothing new here, and the authors of the paper are undoubtedly familiar with all of it.)

First, the untyped lambda calculus.

I'll start by implementing the untyped lambda calculus. It's a very simple language with just three constructs: variables, applications, and lambda expressions, i.e.,

tel

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE LambdaCase #-}

-- Code obviously based on <http://andrej.com/plzoo/html/levy.html>

module CBPV where

import Control.Applicative
import Control.Monad

tel

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE LambdaCase #-}

-- Code obviously based on <http://andrej.com/plzoo/html/levy.html>

-- This is right now *not really* CBPV. In particular, the Rec binder
-- is both less well-behaved and far more complex than it ought to
-- be. Instead of passing a computation back (which should never be
-- possible as variables do not have computation types) it should pass
-- back a thunk.

tel

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE DeriveFunctor #-}

module Tesser where

import Control.Monad
import Data.Bifunctor
import Data.List (foldl')

tel

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE DeriveFunctor #-}

module Tesser where

import Data.List (foldl')
import Data.Profunctor
import Data.Bifunctor

tel

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE DeriveFunctor #-}

module Tesser where

import Data.List (foldl')
import Data.Profunctor
import Data.Bifunctor

tel

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DataKinds #-}

module HetComp where

type family as ++ bs :: [k] where

tel

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeOperators #-}

type b <~ a = forall c . (b -> c) -> a -> c

back :: (a -> b) -> (b <~ a)
back f = (. f)

fwd :: (b <~ a) -> (a -> b)
fwd g = g id

tel

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE GADTs #-}

module FreeCat where

import Control.Category
import Prelude hiding ((.), id)

data Cat p a b where
  Inj  :: p a b -> Cat p a b

tel

{-# LANGUAGE DeriveFunctor              #-}
{-# LANGUAGE FlexibleInstances          #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE LambdaCase                 #-}
{-# LANGUAGE MultiParamTypeClasses      #-}
{-# LANGUAGE ScopedTypeVariables        #-}
{-# LANGUAGE TemplateHaskell            #-}

module Huff where