SystemF.agda

module SystemF where

open import Agda.Primitive
open import Prelude
open import Data.List

weaken-∈ : ∀ {a : Set} (Γ₁ : List a) {Γ x y} → x ∈ (Γ₁ ++ Γ) → x ∈ (Γ₁ ++ y ∷ Γ)
weaken-∈ [] (zero refl) = suc (zero refl)
weaken-∈ [] (suc i) = suc (suc i)
weaken-∈ (x ∷ Γ₁) (zero p) = zero p
weaken-∈ (x ∷ Γ₁) (suc i) = suc (weaken-∈ Γ₁ i)

infixr 7 _⇒_
infixr 7 _=>_
data Kind : Set where
  star : Kind
  _=>_  : (k₁ k₂ : Kind) → Kind 

KindCtx : Set
KindCtx = List Kind

data Type (Δ : KindCtx) : Kind → Set where
  var : ∀ {k} → k ∈ Δ → Type Δ k
  app : ∀ {k₁ k₂} → (a=>b : Type Δ (k₁ => k₂)) → (a : Type Δ k₁) → Type Δ k₂
  all : ∀ k₁ {k₂} → Type (k₁ ∷ Δ) k₂ → Type Δ (k₁ => k₂)
  arr : ∀ {k₁ k₂ k₃} → Type Δ (k₁ => (k₂ => k₃))

_⇒_ : ∀ {Δ} → Type Δ star → Type Δ star → Type Δ star
a ⇒ b = app (app arr a) b

weakenKind : ∀ Δ₁ {Δ x k} → Type (Δ₁ ++ Δ) k → Type (Δ₁ ++ x ∷ Δ) k
weakenKind Δ₁ (var x) = var (weaken-∈ Δ₁ x)
weakenKind Δ₁ (app a b) = app (weakenKind Δ₁ a) (weakenKind Δ₁ b)
weakenKind Δ₁ (all a k) = all a (weakenKind (a ∷ Δ₁) k)
weakenKind Δ₁ arr = arr

substituteKindVar : ∀ Δ₁ {Δ a b} → Type Δ a → b ∈ (Δ₁ ++ a ∷ Δ) → Type (Δ₁ ++ Δ) b
substituteKindVar [] t (zero refl) = t
substituteKindVar [] t (suc i) = var i
substituteKindVar (x ∷ Δ₁) t (zero p) = var (zero p)
substituteKindVar (x ∷ Δ₁) t (suc i) = weakenKind [] (substituteKindVar Δ₁ t i)

substituteKind : ∀ Δ₁ {Δ a b} → Type Δ a → Type (Δ₁ ++ a ∷ Δ) b → Type (Δ₁ ++ Δ) b
substituteKind Δ₁ s (var x) = substituteKindVar Δ₁ s x
substituteKind Δ₁ s (app t t₁) = app (substituteKind Δ₁ s t) (substituteKind Δ₁ s t₁)
substituteKind Δ₁ s (all a t) = all a (substituteKind (a ∷ Δ₁) s t)
substituteKind Δ₁ s arr = arr

-- nat = ∀ a, (a → a) → (a → a)
churchNatType : Type [] (star => star)
churchNatType = all star ((var (zero refl) ⇒ var (zero refl)) ⇒
                          (var (zero refl) ⇒ var (zero refl)))

-- constType = ∀ a, a → ∀ b, b → a
constType : Type [] (star => star => star)
constType = all star (app (app arr (var (zero refl)))
                          (all star {k₂ = star} (app (app arr (var (zero refl))) (var (suc (zero refl))))))


-- constType2 = ∀ a, ∀ b, a → b → a
constType2 : Type [] (star => star => star)
constType2 = all star (all star (app {k₁ = star} (app arr
                                          (var (suc (zero refl))))
                                     (app (app arr
                                               (var (zero refl)))
                                          (var (suc (zero refl))))))

-- TODO: use All?
TypeCtx : KindCtx → Set
TypeCtx Δ = List (Σ Kind (Type Δ))

substituteKindInCtx : ∀ (k : Kind) {Δ} → (t : Type Δ k) → Σ Kind (Type (k ∷ Δ)) → Σ Kind (Type Δ)
substituteKindInCtx k t (k₂ , t₂) = k₂ , substituteKind [] t t₂

weakenTypeCtx : ∀ Δ₁ {k Δ} → TypeCtx (Δ₁ ++ Δ) → TypeCtx (Δ₁ ++ k ∷ Δ)
weakenTypeCtx Δ₁ Γ = map (λ x → fst x , weakenKind Δ₁ (snd x)) Γ

data Term (Δ : KindCtx) (Γ : TypeCtx Δ) : (k : Kind) → Type Δ k → Set where
  var : ∀ {k} {a : Type Δ k} → (k , a) ∈ Γ → Term Δ Γ k a
  app : ∀ {k₁ k₂ k₃} {a b} (f : Term Δ Γ k₁ (app (app arr a) b)) → (x : Term Δ Γ k₂ a) → Term Δ Γ k₃ b
  lam : ∀ {k₁ k₂ k₃} (a : Type Δ k₁) {b} → Term Δ ((k₁ , a) ∷ Γ) k₂ b → Term Δ Γ k₃ (app (app arr a) b)
  -- weakenTypeCtx might look strange:
  -- but as we add new kind variable to kind contex Δ,
  -- we "weaken" current type context Γ, reindexing all kind variables
  -- The constType example below demonstrates what happens
  all : ∀ k₁ {k₂} {b : Type (k₁ ∷ Δ) k₂} (x : Term (k₁ ∷ Δ) (weakenTypeCtx [] Γ) k₂ b) → Term Δ Γ (k₁ => k₂) (all k₁ b)
  allapp : ∀ {k₁ k₂} {a : Type Δ (k₁ => k₂)} (x : Term Δ Γ (k₁ => k₂) a) (b : Type Δ k₁) → Term Δ Γ k₂ (app a b)

-- zero : ∀ a, (a → a) → (a → a)
-- zero = Λ a : *, λ s : (a → a), λ z : a, z
--
-- = ?                                    -- Δ = [],          Γ = [],                  k = * => *,  τ = ∀ a : *, (a → a) → a → a
-- = Λ a : *, ?                           -- Δ = [a : star],  Γ = [],                  k = *,       τ = (a → a) → a → a
-- = Λ a : *, λ s : (a → a), ?            -- Δ = [a : star],  Γ = [s : a → a],         k = *,       τ = a → a
-- = Λ a : *, λ s : (a → a), λ z : a, ?   -- Δ = [a : star],  Γ = [z : a, s = a → a],  k = *,       τ = a
--
--
churchZero : Term [] [] (star => star) churchNatType
churchZero = all star (lam (app (app arr (var (zero refl))) (var (zero refl)))
                           (lam (var (zero refl))
                                (var (zero refl))))

-- const : ∀ a b, a → b → a
-- const = Λ a : *, Λ b : *, λ x : a, λ y : b, a
-- const : ∀ a, a → ∀ b, b → a
-- const = Λ a : *, λ x : a, Λ b : *, λ y : b, a
--
-- = ?                                      -- Δ = [],                    Γ = [],                      k = * => * => *,  τ = ∀ a, a → ∀ b, b → a
-- = Λ a : *, ?                             -- Δ = [a : star],            Γ = [],                      k = * => *,       τ = a → ∀ b, b → a
-- = Λ a : *, Λ x : a, ?                    -- Δ = [a : star],            Γ = [x : a = 0],             k = * => *,       τ = ∀ b, b → a
-- = Λ a : *, λ x : a, Λ b : *, ?           -- Δ = [b : star, a : star],  Γ = [x : a = 1],             k = *,            τ = b → a
-- = Λ a : *, λ x : a, Λ b : *, λ y : b, ?  -- Δ = [b : star, a : star],  Γ = [y : b = 0, x : a = 1],  k = *,            τ = b
--

churchConst : Term [] [] (star => star => star) constType
churchConst = all star (lam (var (zero refl))
                            (all star (lam (var (zero refl))
                                           (var (suc (zero refl))))))

churchConst2 : Term [] [] (star => star => star) constType2
churchConst2 = all star (all star (lam (var (suc (zero refl)))
                                       (lam (var (zero refl))
                                            (var (suc (zero refl)))))) 

-- Can't write eval, SysemF is impredicative, Agda is predicative!
{-
Ki : Kind → Level
Ki star = lzero
Ki (k => k₁) = lsuc (Ki k ⊔ Ki k₁)

Env : KindCtx → Set
Env Δ = All Ki Δ -- doesn't work, and shouldn't
-}