Last active

Embed URL

HTTPS clone URL

SSH clone URL

You can clone with HTTPS or SSH.

Download Gist
View SOTrie.agda
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76
module SOTrie where
 
open import Data.Unit
open import Category.Functor
open import Function
open import Level
open import Relation.Binary
 
-- A context is just a snoc-list.
data Cxt {𝒂} (A : Set 𝒂) : Set 𝒂 where
ε : Cxt A
_∷ᵣ_ : Cxt A A Cxt A
 
-- Context membership.
data _∈_ {𝒂} {A : Set 𝒂} (a : A) : Cxt A → Set 𝒂 where
here : {Δ} a ∈ Δ ∷ᵣ a
there : {Δ a′} a ∈ Δ a ∈ Δ ∷ᵣ a′
infix 3 _∈_
 
-- Well-formed types, using de Bruijn indices.
data _⊢ₜ (Δ : Cxt ⊤) : Set where
1ₜ : Δ ⊢ₜ
Varₜ : _ ∈ Δ Δ ⊢ₜ
_×ₜ_ : Δ ⊢ₜ Δ ⊢ₜ Δ ⊢ₜ
μₜ : Δ ∷ᵣ _ ⊢ₜ Δ ⊢ₜ
infix 3 _⊢ₜ
 
-- A closed type.
Type : Set
Type = ε ⊢ₜ
 
-- Type-level substitutions and renamings.
Sub Ren : Rel (Cxt ⊤) zero
Sub Δ Δ′ = _ ∈ Δ Δ′ ⊢ₜ
Ren Δ Δ′ = {x} x ∈ Δ x ∈ Δ′
 
-- Renaming extension.
extendᵣ : {Δ Δ′} Ren Δ Δ′ Ren (Δ ∷ᵣ _) (Δ′ ∷ᵣ _)
extendᵣ ρ here = here
extendᵣ ρ (there x) = there (ρ x)
 
-- Lift a type renaming to a type.
_*ᵣ_ : {Δ Δ′} Ren Δ Δ′ Δ ⊢ₜ Δ′ ⊢ₜ
_ *ᵣ 1= 1
ρ *ᵣ (Varₜ x) = Varₜ (ρ x)
ρ *ᵣ (τ₁ ×ₜ τ₂) = (ρ *ᵣ τ₁) ×ₜ (ρ *ᵣ τ₂)
ρ *ᵣ (μₜ τ) = μₜ (extendᵣ ρ *ᵣ τ)
 
-- Substitution extension.
extend : {Δ Δ′} Sub Δ Δ′ Sub (Δ ∷ᵣ _) (Δ′ ∷ᵣ _)
extend θ here = Varₜ here
extend θ (there x) = there *ᵣ (θ x)
 
-- Lift a type substitution to a type.
_*_ : {Δ Δ′} Sub Δ Δ′ Δ ⊢ₜ Δ′ ⊢ₜ
θ * 1= 1
θ * Varₜ x = θ x
θ * (τ₁ ×ₜ τ₂) = (θ * τ₁) ×ₜ (θ * τ₂)
θ * μₜ τ = μₜ (extend θ * τ)
 
data Trie {𝒂} (A : Set 𝒂) : Type → Set 𝒂 where
〈〉ₛ : A 1ₜ ▷ A
×ₛ : {τ₁ τ₂} τ₁ ▷ τ₂ ▷ A τ₁ ×ₜ τ₂ ▷ A
Rollₛ : {τ} (const (μₜ τ) * τ) ▷ A μₜ τ ▷ A
 
infixr 5 Trie
syntax Trie A τ = τ ▷ A
 
fmap fmap′ : {𝒂} {A B : Set 𝒂} {τ} (A B) τ ▷ A τ ▷ B
fmap f (〈〉ₛ x) = 〈〉ₛ (f x)
fmap f (×ₛ σ) = ×ₛ (fmap (fmap′ f) σ)
fmap f (Rollₛ σ) = Rollₛ (fmap f σ)
 
fmap′ f (〈〉ₛ x) = 〈〉ₛ (f x)
fmap′ f (×ₛ σ) = ×ₛ (fmap′ (fmap f) σ)
fmap′ f (Rollₛ σ) = Rollₛ (fmap′ f σ)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Something went wrong with that request. Please try again.