Skip to content

Instantly share code, notes, and snippets.

@larrytheliquid
Last active February 5, 2017 22:38
Show Gist options
  • Save larrytheliquid/e2bec348c9fb7d894ff25e61efa0349c to your computer and use it in GitHub Desktop.
Save larrytheliquid/e2bec348c9fb7d894ff25e61efa0349c to your computer and use it in GitHub Desktop.
open import Data.Unit
open import Data.Bool
open import Data.Nat
open import Data.Product
module _ where
{-
This odd approach gives you 2 choices when defining an indexed type:
1. Use a McBride-Dagand encoding so your datatype
"need not store its indices".
2. Use a standard "propositional" encoding, whose semantics
is defined without an external equality type.
Using either choice, we still get "general" indexed types
in the Dybjer-Setzer sense. That is, the
initial algebra constructor can only be matched against
when the index constraints are met. In contrast,
"restricted" indexed types are encoded as a parameterized type
with explicit propositional equality arguments, and can
always match against the initial algebra before an equality
argument (i.e. restricted types are a subset of all
Agda types).
-}
----------------------------------------------------------------------
data Desc (I : Set) : Set₁ where
`ι : I → Desc I
`δ : I → Desc I → Desc I
`σ : (A : Set) (D : A → Desc I) → Desc I
⟦_⟧ : {I : Set} (D : Desc I) (X : I → I → Set) → Set
⟦ `ι i ⟧ X = ⊤
-- take diagonal of X
⟦ `δ i D ⟧ X = X i i × ⟦ D ⟧ X
⟦ `σ A D ⟧ X = Σ A λ a → ⟦ D a ⟧ X
idx : {I : Set} (D : Desc I) (X : I → I → Set) (xs : ⟦ D ⟧ X) → I
idx (`ι i) X tt = i
idx (`δ i D) X (x , xs) = idx D X xs
idx (`σ A D) X (a , xs) = idx (D a) X xs
-- Combine McBride-Dagand indexed descriptions
-- where we compute a description from an index
-- with Dybjer-Setzer "general" type families
-- where we compute an index from arguments.
-- Key: definition of ⟦_⟧ by diagonal in inductive case
data μ {I : Set} (R : I → Desc I) (i : I) : I → Set where
init : (xs : ⟦ R i ⟧ (μ R)) → μ R i (idx (R i) (μ R) xs)
----------------------------------------------------------------------
module CompVec where
-- compute desc from index
VecD : Set → ℕ → Desc ℕ
VecD A zero = `ι zero
VecD A (suc n) = `σ A λ _ → `δ n (`ι (suc n))
-- take diagonal of μ (VecD A)
Vec : Set → ℕ → Set
Vec A n = μ (VecD A) n n
nil : (A : Set) → Vec A zero
nil A = init tt
cons : (A : Set) (n : ℕ) → A → Vec A n → Vec A (suc n)
cons A n a xs = init (a , xs , tt)
----------------------------------------------------------------------
module PropVec where
-- ignore the index
-- but do not need separate propositional equality (≡)
VecD : Set → ℕ → Desc ℕ
VecD A _ = `σ Bool λ where
true → `ι zero
false → `σ ℕ λ n → `σ A λ _ → `δ n (`ι (suc n))
-- take diagonal of μ (VecD A)
Vec : Set → ℕ → Set
Vec A n = μ (VecD A) n n
nil : (A : Set) → Vec A zero
nil A = init (true , tt)
cons : (A : Set) (n : ℕ) → A → Vec A n → Vec A (suc n)
cons A n a xs = init (false , n , a , xs , tt)
----------------------------------------------------------------------
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment