larrytheliquid · February 5, 2017 22:38
diff --git a/GenerallyIndexed.agda b/GenerallyIndexed.agda
 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)

 ----------------------------------------------------------------------
	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)

	----------------------------------------------------------------------