A strongly typed polymorphic lambda calculus

Polymorphic.agda

module Polymorphic where

import Level
open Level using (Level; _⊔_)
open import Function
open import Data.Product hiding (map)
open import Data.List hiding (all)

data Index {A : Set} : List A → A → Set where
  zero : ∀ {τ Γ} → Index (τ ∷ Γ) τ
  suc  : ∀ {σ τ Γ} (i : Index Γ τ) → Index (σ ∷ Γ) τ

-- http://strictlypositive.org/ren-sub.pdf
record PreKit {A : Set} (F G : List A → A → Set) : Set where
  constructor preKit
  field
    vr : ∀ {  τ Γ} → Index Γ τ → F Γ τ
    tm : ∀ {  τ Γ} → F Γ τ → G Γ τ
    wk : ∀ {σ τ Γ} → F Γ τ → F (σ ∷ Γ) τ

  lift : ∀ {σ τ Γ Δ} → (∀ {x} → Index Γ x → F Δ x) → Index (σ ∷ Γ) τ → F (σ ∷ Δ) τ
  lift f zero    = vr zero
  lift f (suc i) = wk (f i)

record Kit {A : Set} (G : List A → A → Set) : Set₁ where
  constructor kit
  field
    vr   : {τ : A} {Γ : List A} → Index Γ τ → G Γ τ
    trav : ∀ {F} → PreKit F G → ∀ {τ Γ Δ} → (∀ {x} → Index Γ x → F Δ x) → G Γ τ → G Δ τ

  rename : ∀ {τ Γ Δ} → (∀ {x} → Index Γ x → Index Δ x) → G Γ τ → G Δ τ
  rename = trav (preKit id vr suc)

  subst : ∀ {τ Γ Δ} → (∀ {x} → Index Γ x → G Δ x) → G Γ τ → G Δ τ
  subst = trav (preKit vr id (rename suc))

  subst₀ : ∀ {σ τ Γ} → G (σ ∷ Γ) τ → G Γ σ → G Γ τ
  subst₀ {σ} {τ} {Γ} t s = subst f t
    where
    f : ∀ {x} → Index (σ ∷ Γ) x → G Γ x
    f zero = s
    f (suc i) = vr i

open Kit {{...}}

infixr 2 _⇒_
infixr 1 _⇒!_

data Kind : Set where
  *   : Kind
  _⇒_ : (σ τ : Kind) → Kind

data Type (Γ : List Kind) : Kind → Set where
  var  : ∀ {τ} (i : Index Γ τ) → Type Γ τ
  app  : ∀ {σ τ} (f : Type Γ (σ ⇒ τ)) (x : Type Γ σ) → Type Γ τ
  lam  : ∀ {σ τ} (q : Type (σ ∷ Γ) τ) → Type Γ (σ ⇒ τ)

  _⇒!_ : (σ : Kind)     (τ : Type (σ ∷ Γ) *) → Type Γ *
  _⇒_  : (σ : Type Γ *) (τ : Type Γ *) → Type Γ *

typeKit : Kit Type
typeKit = kit var helper
  where
  helper : ∀ {F} → PreKit F Type → ∀ {τ Γ Δ} → (∀ {x} → Index Γ x → F Δ x) → Type Γ τ → Type Δ τ
  helper pk f (var i)   = PreKit.tm pk (f i)
  helper pk f (app g x) = app (helper pk f g) (helper pk f x)
  helper pk f (lam q)   = lam (helper pk (PreKit.lift pk f) q)
  helper pk f (σ ⇒! τ) = σ             ⇒! helper pk (PreKit.lift pk f) τ
  helper pk f (σ ⇒  τ) = helper pk f σ ⇒  helper pk f τ


data Term {ΓK} (Γ : List (Type ΓK *)) : Type ΓK * → Set where
  var  : ∀ {τ} → Index Γ τ → Term Γ τ
  app  : ∀ {σ τ} (f : Term Γ (σ ⇒  τ)) (x : Term Γ  σ) → Term Γ τ
  app! : ∀ {k τ} (f : Term Γ (k ⇒! τ)) (x : Type ΓK k) → Term Γ (subst₀ τ x)
  lam  : ∀ {σ τ} (q : Term (σ ∷ Γ) τ) → Term Γ (σ ⇒ τ)
  lam! : ∀ {k} {τ : Type (k ∷ ΓK) *} (q : Term {k ∷ ΓK} (map (rename suc) Γ) τ) → Term Γ (k ⇒! τ)

identity : Term {[]} [] (* ⇒! (var zero ⇒ var zero))
identity = lam! (lam (var zero))

Leibniz : ∀ {Γ} → Type Γ (* ⇒ * ⇒ *)
Leibniz = lam (lam ((* ⇒ *) ⇒! (app (var zero) (var (suc zero)) ⇒ app (var zero) (var (suc (suc zero))))))

refl : Term {[]} [] (* ⇒! app (app Leibniz (var zero)) (var zero))
refl = lam! {!!} -- not reducing!

sym : Term {[]} [] (* ⇒! * ⇒! app (app Leibniz (var zero)) (var (suc zero)) ⇒ app (app Leibniz (var (suc zero))) (var zero))
sym = lam! (lam! (lam {!!})) -- not reducing!

I need a $ for types that actually reduces, to fill in those holes.