SystemF.agda

module SystemF where

data Kind : Set where
  * : Kind
  _=>_ : Kind -> Kind -> Kind

data KindContext : Set where
  [] : KindContext
  _,_ : KindContext -> Kind -> KindContext

data TypeVar : KindContext -> Kind -> Set where
  here : forall {H K} -> TypeVar (H , K) K
  there : forall {H K K'} -> TypeVar H K -> TypeVar (H , K') K

data Type (H : KindContext) : Kind -> Set where
  var : forall {K} -> TypeVar H K -> Type H K
  FOO : Type H *
  _=>_ : Type H * -> Type H * -> Type H *
  all : (K : Kind) -> Type (H , K) * -> Type H *
  lam : forall {K'} -> (K : Kind) -> Type (H , K) K' -> Type H (K => K')
  app : forall {K K'} -> Type H (K => K') -> Type H K -> Type H K'

wkRen : forall {H H' : KindContext} {K'} -> (forall {K} -> TypeVar H K -> TypeVar H' K) -> forall {K} -> TypeVar (H , K') K -> TypeVar (H' , K') K
wkRen r here = here
wkRen r (there v) = there (r v)

renType : forall {H H'} -> (forall {K} -> TypeVar H K -> TypeVar H' K) -> forall {K} -> Type H K -> Type H' K
renType r (var x) = var (r x)
renType r FOO = FOO
renType r (A => B) = renType r A => renType r B
renType r (all K A) = all K (renType (wkRen r) A)
renType r (lam K A) = lam K (renType (wkRen r) A)
renType r (app A B) = app (renType r A) (renType r B)

wkEnv : forall {H H' K'} -> (forall {K} -> TypeVar H K -> Type H' K) -> forall {K} -> TypeVar (H , K') K -> Type (H' , K') K
wkEnv env here = var here
wkEnv env (there v) = renType there (env v)

subType : forall {H H'} -> (forall {K} -> TypeVar H K -> Type H' K) -> forall {K} -> Type H K -> Type H' K
subType env (var x) = env x
subType env FOO = FOO
subType env (A => B) = subType env A => subType env B
subType env (all K A) = all K (subType (wkEnv env) A)
subType env (lam K A) = lam K (subType (wkEnv env) A)
subType env (app A B) = app (subType env A) (subType env B)

wkType : forall {H K K'} -> Type H K -> Type (H , K') K
wkType A = renType there A

substitution : forall {H K K'} -> Type H K' -> TypeVar (H , K') K -> Type H K
substitution A here = A
substitution A (there v) = var v

substType : forall {H K K'} -> Type H K' -> Type (H , K') K -> Type H K
substType A B = subType (substitution A) B

{-# TERMINATING #-}
reduce : forall {H K} -> Type H K -> Type H K
reduce (var x) = var x
reduce FOO = FOO
reduce (A => B) = reduce A => reduce B
reduce (all K A) = all K (reduce A)
reduce (lam K A) = lam K (reduce A)
reduce (app A B) with reduce A | reduce B
... | lam K A' | B' = reduce (substType B' A')
... | A' | B' = app A' B'

data TypeReduce {H} : (K : Kind) -> Type H K -> Type H K -> Set where
  var : forall {K} {x : TypeVar H K} -> TypeReduce K (var x) (var x)
  FOO : TypeReduce * FOO FOO
  _=>_ : forall {A A' B B'} -> TypeReduce * A A' -> TypeReduce * B B' -> TypeReduce * (A => B) (A' => B')
  all : (K : Kind) -> forall {A A'} -> TypeReduce * A A' -> TypeReduce * (all K A) (all K A')
  lam : (K : Kind) -> forall {K' A A'} -> TypeReduce K' A A' -> TypeReduce (K => K') (lam K A) (lam K A')
  app : forall {K K'} {A A' B B' C} -> TypeReduce (K => K') A (lam K A') -> TypeReduce K B B' -> TypeReduce K' (substType B' A') C -> TypeReduce K' (app A B) C

data TypeContext : KindContext -> Set where
  [] : TypeContext []
  _,term_ : forall {H} -> TypeContext H -> Type H * -> TypeContext H
  _,type_ : forall {H} -> TypeContext H -> (K : Kind) -> TypeContext (H , K)


data TermVar : {H : KindContext} -> TypeContext H -> Type H * -> Set where
  here : forall {H} {G : TypeContext H} {A} -> TermVar (G ,term A) A
  there-term : forall {H} {G : TypeContext H} {A B} -> TermVar G A -> TermVar (G ,term B) A
  there-type : forall {H} {G : TypeContext H} {A K} -> TermVar G A -> TermVar (G ,type K) (wkType A)

data Term {H : KindContext} (G : TypeContext H) : Type H * -> Set where
  var : forall {A : Type H *} -> TermVar G A -> Term G A
  lam : forall {A B : Type H *} -> Term (G ,term A) B -> Term G (A => B)
  app : forall {A B : Type H *} -> Term G (A => B) -> Term G A -> Term G B
  abs : forall {K : Kind} {B : Type (H , K) *} -> Term (G ,type K) B -> Term G (all K B)
  inst : forall {K : Kind} {B : Type (H , K) *} -> Term G (all K B) -> (A : Type H K) -> Term G (reduce (substType A B))