Define type.

2 files changed, 93 insertions, 0 deletions

diff --git a/Everything.agda b/Everything.agda
index 0127e7e..a2b808f 100644
--- a/Everything.agda
+++ b/Everything.agda
@@ -2,3 +2,4 @@
 module Everything where
 
 import Data.BinOp
+import Data.Type
diff --git a/src/Data/Type.agda b/src/Data/Type.agda
new file mode 100644
index 0000000..e0637ba
--- /dev/null
+++ b/src/Data/Type.agda
@@ -0,0 +1,92 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Data.List using (List; _++_; map; filter; foldl)
+open import Data.Nat using (ℕ; _≟_)
+
+module Data.Type
+  (mkFresh : List ℕ → ℕ)
+  where
+
+open import Data.BinOp using (BinOp)
+open import Data.Bool using (if_then_else_)
+open import Data.Nat.Properties using (≤-totalOrder)
+open import Function using (_∘_)
+open import Relation.Binary.PropositionalEquality using (_≢_)
+open import Relation.Nullary using (¬_)
+open import Relation.Nullary.Decidable using (isYes)
+open import Relation.Nullary.Negation using (¬?)
+
+open List
+open ℕ
+
+infix 5 _,_
+infix 4 _≈_
+
+-- Type Definition ------------------------------------------------------------
+
+data Type : Set where
+  var : (α : ℕ) → Type
+  unit : Type
+  bin  : (⊗ : BinOp) → Type → Type → Type
+  all  : (α : ℕ) → Type → Type
+
+free : Type → List ℕ
+free (var α)     = α ∷ []
+free unit        = []
+free (bin ⊗ A B) = free A ++ free B
+free (all α A)   = filter (¬? ∘ (α ≟_)) (free A)
+
+-- Variable Renaming ----------------------------------------------------------
+
+record Subst {a} (A : Set a) : Set a where
+  pattern
+  constructor _,_
+  field
+    from : ℕ
+    to : A
+
+open Subst
+
+Renaming : Set
+Renaming = Subst ℕ
+
+{-# DISPLAY Subst ℕ = Renaming #-}
+
+private
+  variable
+    α β : ℕ
+    ⊗ : BinOp
+    A B C D : Type
+
+applyRenaming : List Renaming → ℕ → ℕ
+applyRenaming ρs α =
+  foldl (λ α (from , to) → if isYes (α ≟ from) then to else α) α ρs
+
+rename : List Renaming → Type → Type
+rename ρs (var α)     = var (applyRenaming ρs α)
+rename ρs unit        = unit
+rename ρs (bin ⊗ A B) = bin ⊗ (rename ρs A) (rename ρs B)
+rename ρs (all α A)   =
+  let β = mkFresh (map (applyRenaming ρs) (free A)) in
+  all β (rename ((α , β) ∷ ρs) A)
+
+-- Alpha Equivalence ----------------------------------------------------------
+
+data _≈_ : Type → Type → Set where
+  var  : ∀ α → var α ≈ var α
+  unit : unit ≈ unit
+  bin  : A ≈ C → B ≈ D → bin ⊗ A B ≈ bin ⊗ C D
+  all  : let γ = mkFresh (free (all α A) ++ free (all β B)) in
+         rename ((γ , α) ∷ []) A ≈ rename ((γ , β) ∷ []) B → all α A ≈ all β B
+
+-- Basic Manipulations --------------------------------------------------------
+
+subst : List Renaming → Subst Type → Type → Type
+subst ρs α⇒A (var β) =
+  let γ = applyRenaming ρs β in
+  if isYes (γ ≟ α⇒A .from) then α⇒A .to else var γ
+subst ρs α⇒A unit = unit
+subst ρs α⇒A (bin ⊗ B C) = bin ⊗ (subst ρs α⇒A B) (subst ρs α⇒A C)
+subst ρs α⇒A (all β B) =
+  let γ = mkFresh (map (applyRenaming ρs) (free (α⇒A .to) ++ free B)) in
+  all γ (subst ((β , γ) ∷ ρs) α⇒A B)