ssgip.gh

{- SSGIP Examples, Stephanie Weirich, March 24-26, 2010 -}
{-# OPTIONS --type-in-type --no-termination-check --no-positivity-check #-}
module ssgip.gh where

open import Data.Nat
open import Data.Vec hiding (_∈_)
open import Data.Unit
open import Data.Product
open import Data.Sum
open import Data.Bool
open import Relation.Binary.PropositionalEquality

infixr 50 _⇒_
-- note that this is the unicode ∶ symbol
infixr 50 _∶_ 

Choice : Set → Set → Set
Choice = \ A B → ( A × B ) ⊎ A ⊎ B ⊎ ⊤

data μ : (Set → Set) → Set where
   roll : ∀{A} → A (μ A) → μ A

unroll : ∀ {A} → μ A → A (μ A)
unroll (roll x) = x

List       : Set → Set
List A     = μ (\ B → ⊤ ⊎ (A × B))

nil        : ∀ {A} → List A
nil        = roll (inj₁ tt)

_∶_        : ∀ {A} → A → List A → List A
x ∶ xs     = roll (inj₂ (x , xs))

example-list     : List Bool
example-list     = true ∶ false ∶ nil

-- Structural definition of Nats
Nat : Set 
Nat = μ (\ N → ⊤ ⊎ N)

zilch : Nat
zilch = roll (inj₁ tt)

succ  : Nat → Nat
succ x = roll (inj₂ x)

data Kind : Set where 
  ⋆      : Kind 
  _⇒_    : Kind → Kind → Kind

data Const : Kind → Set where
  Unit  : Const ⋆
  Sum   : Const (⋆ ⇒ ⋆ ⇒ ⋆) 
  Prod  : Const (⋆ ⇒ ⋆ ⇒ ⋆)

data Ctx : Set where 
  []    : Ctx
  _∷_   : Kind → Ctx → Ctx

data V : Kind → Ctx → Set where
  VZ   : ∀ {Γ k} → V k (k ∷ Γ) 
  VS   : ∀ {Γ k' k} → V k Γ → V k (k' ∷ Γ) 

data Typ : Ctx → Kind → Set where 
  Var  : ∀ {Γ k} → V k Γ → Typ Γ k 
  Lam  : ∀ {Γ k₁ k₂} → Typ (k₁ ∷ Γ) k₂ 
       → Typ Γ (k₁ ⇒ k₂)
  App  : ∀ {Γ k₁ k₂} → Typ Γ (k₁ ⇒ k₂) → Typ Γ k₁
       → Typ Γ k₂
  Con  : ∀ {Γ k} → Const k → Typ Γ k
  Mu   : ∀ {Γ} → Typ Γ (⋆ ⇒ ⋆) → Typ Γ ⋆

Ty : Kind → Set
Ty k = Typ [] k

⟦_⟧        : Kind → Set
⟦ ⋆ ⟧      = Set
⟦ a ⇒ b ⟧  = ⟦ a ⟧ → ⟦ b ⟧

interp-c : ∀ {k} → Const k → ⟦ k ⟧
interp-c Unit     = ⊤     -- has kind Set
interp-c Sum      = _⊎_   -- has kind Set → Set → Set
interp-c Prod     = _×_

data Env : Ctx → Set where
  []   : Env [] 
  _∷_  : ∀ {k Γ} → ⟦ k ⟧ → Env Γ → Env (k ∷ Γ)

sLookup : ∀ {k Γ} → V k Γ → Env Γ → ⟦ k ⟧
sLookup VZ      (v ∷ Γ) = v
sLookup (VS x)  (v ∷ Γ) = sLookup x Γ

interp : ∀ {k Γ} → Typ Γ k → Env Γ → ⟦ k ⟧
interp (Var x)      e  = sLookup x e
interp (Lam t)      e  = \ y → interp t (y ∷ e)
interp (App t1 t2)  e  = (interp t1 e) (interp t2 e)
interp (Mu t)       e  = μ (interp t e)
interp (Con c)      e  = interp-c c

⌊_⌋ : ∀ {k} → Ty k → ⟦ k ⟧
⌊ t ⌋ = interp t []

list : Ty (⋆ ⇒ ⋆) 
list = 
  Lam (Mu (Lam 
      (App (App (Con Sum) (Con Unit)) 
      (App (App (Con Prod) (Var (VS VZ))) (Var VZ)))))

nat : Ty ⋆ 
nat = Mu (Lam (App (App (Con Sum) (Con Unit)) (Var VZ)))

Maybe : Set → Set
Maybe = \ A → ⊤ ⊎ A

maybe : Ty (⋆ ⇒ ⋆) 
maybe = 
   Lam (App (App (Con Sum) (Con Unit)) (Var VZ))

_⟨_⟩_ : (Set → Set) → (k : Kind) → ⟦ k ⟧ → Set 
b ⟨ ⋆ ⟩         t  = b t
b ⟨ k1 ⇒ k2 ⟩  t  = ∀ { A } → b ⟨ k1 ⟩ A → b ⟨ k2 ⟩ (t A)

data VarEnv  (b : Set → Set) : Ctx → Set where
   []   : VarEnv b []
   _∷_  : {k : Kind}  {Γ : Ctx}{a : ⟦ k ⟧}
          → b ⟨ k ⟩ a 
          → VarEnv b Γ 
          → VarEnv b (k ∷ Γ)

toEnv : {Γ : Ctx}{b : Set → Set} → VarEnv b Γ → Env Γ
toEnv [] = []
toEnv (_∷_ {_}{_}{a} _ r) = a ∷ toEnv r

vLookup : ∀ {Γ k}{b : Set → Set} 
           → (v : V k Γ) → (ve : VarEnv b Γ)
           → b ⟨ k ⟩ (sLookup v (toEnv ve))
vLookup VZ      (v ∷ ve)  = v
vLookup (VS x)  (v ∷ ve)  = vLookup x ve

Eq : Set → Set
Eq A = A → A → Bool

mutual
  geq-open : {Γ : Ctx}{k : Kind} 
    → (ve : VarEnv Eq Γ)
    → (t : Typ Γ k) → Eq ⟨ k ⟩ (interp t (toEnv ve))
  geq-open ve (Var v)      = vLookup v ve
  geq-open ve (Lam t)      = \ y → geq-open (y ∷ ve) t
  geq-open ve (App t1 t2)  = (geq-open ve t1) (geq-open ve t2)
  geq-open ve (Mu t)       = 
    \ x y → geq-open ve (App t (Mu t)) (unroll x) (unroll y)
  geq-open ve (Con c)      = geq-c c  

  geq-sum   : ∀ {A} → (A → A → Bool)
            → ∀ {B} → (B → B → Bool)
            → (A ⊎ B) → (A ⊎ B) → Bool
  geq-sum ra rb (inj₁ x₁) (inj₁ x₂) = ra x₁ x₂
  geq-sum ra rb (inj₂ x₁) (inj₂ x₂) = rb x₁ x₂
  geq-sum _ _ _ _  = false

  geq-prod  : ∀ {A} → (A → A → Bool) 
            → ∀{B} → (B → B → Bool)
            → (A × B) → (A × B) → Bool
  geq-prod ra rb ( x₁ , x₂ ) (y₁ , y₂) = ra x₁ y₁ ∧ rb x₂ y₂

  geq-c : {k : Kind} → (c : Const k) → Eq ⟨ k ⟩ ⌊ Con c ⌋
  geq-c Unit = \ t1 t2 → true
  geq-c Sum  = geq-sum 
  geq-c Prod = geq-prod

ConstEnv : (Set → Set) → Set
ConstEnv b = ∀ {k} → (c : Const k) → b ⟨ k ⟩ ⌊ Con c ⌋

MuGen : (Set → Set) → Set
MuGen b = ∀ {A} → b (A (μ A)) → b (μ A)


gen-open : {b : Set → Set}{Γ : Ctx}{k : Kind} 
    → ConstEnv b → (ve : VarEnv b Γ) → MuGen b
    → (t : Typ Γ k) → b ⟨ k ⟩ (interp t (toEnv ve))
gen-open ce ve d (Var v)      = vLookup v ve
gen-open ce ve d (Lam t)      = \ y → gen-open ce (y ∷ ve) d t
gen-open ce ve d (App t1 t2)  = 
   (gen-open ce ve d t1) (gen-open ce ve d t2)
gen-open ce ve d (Con c)      = ce c 
gen-open ce ve d (Mu t)       = 
   d (gen-open ce ve d (App t (Mu t)))

gen : {b : Set → Set}{k : Kind} → ConstEnv b → MuGen b
    → (t : Ty k) → b ⟨ k ⟩ ⌊ t ⌋
gen c b t = gen-open c [] b t

geq : {k : Kind} → (t : Ty k) → Eq ⟨ k ⟩ ⌊ t ⌋
geq = gen geq-c eb where
  eb : ∀ {A} → Eq (A (μ A)) → Eq (μ A)
  eb f = \ x y → f (unroll x) (unroll y)

eq-list : List Nat → List Nat → Bool
eq-list = geq (App list nat)

Count : Set → Set 
Count A = A → ℕ

gcount : {k : Kind} → (t : Ty k) → Count ⟨ k ⟩ ⌊ t ⌋
gcount = gen ee eb where
  ee : ConstEnv Count
  ee Unit = \ t → 0
  ee Sum  = g where
     g : ∀ { A } → _ → ∀ { B } → _ → (A ⊎ B) → ℕ
     g ra rb (inj₁ x) = ra x 
     g ra rb (inj₂ x) = rb x
  ee Prod = g where
     g : ∀ { A } → _ → ∀ { B } → _ → (A × B) → ℕ
     g ra rb ( x₁ , x₂ ) = ra x₁ + rb  x₂

  eb : MuGen Count
  eb f = \ x → f (unroll x)

gsize : (t : Ty (⋆ ⇒ ⋆)) → ∀ {A} → ⌊ t ⌋ A → ℕ
gsize t = gcount t (\ x → 1)

gsum : (t : Ty (⋆ ⇒ ⋆)) → ⌊ t ⌋ ℕ → ℕ
gsum t = gcount t (\ x → x)

exlist2 : List ℕ
exlist2 = 1 ∶ 2 ∶ 3 ∶ nil

_⟨_⟩₂ : (Set → Set → Set) → (k : Kind) → ⟦ k ⟧ → ⟦ k ⟧ → Set 
b ⟨ ⋆ ⟩₂         = \ t₁ t₂ → b t₁ t₂
b ⟨ k₁ ⇒ k₂ ⟩₂  = \ t₁ t₂ → ∀ { a₁ a₂ } → 
   (b ⟨ k₁ ⟩₂) a₁ a₂ → (b ⟨ k₂ ⟩₂) (t₁ a₁) (t₂ a₂)
Map : Set → Set → Set
Map A B = A → B
Vec' : ℕ -> Set -> Set
Vec' zero     = \ A -> ⊤
Vec' (suc n)  = \ A -> A × (Vec' n A)