Lists

We define the data type of lists to be used in other examples.

module list where

open import map
open import Data.List using (_∷_ ; [] )
open import Data.Vec renaming (_∷_ to _¦_ ; [] to [||] ; [_] to [|_|])
open import Data.Unit renaming (tt to ∗)
open import Data.Product using (_,_)

We first define the type variables and contexts we will use later on.

α β : mix-var
α = tvar 
β = tvar 

Γα Γβ : type-context {mix-var}
Γα = ⟦ [| α |] ⟧
Γβ = ⟦ [| β |] ⟧

We define now the data type of lists, with the usual constructors nil and cons.

List-id : id-TC-var
List-id = 

nil-id cons-id : id-data-constructor
nil-id = 
cons-id = 

List-name : TC-var 
List-name = TC List-id 

nil cons : data-constructor 
nil = nil-id ∷ [] ⇒ᵀ [| varᵀ α |]
cons = cons-id ∷ (varᵀ β ∷ (appᵀ List-name [ [| varᵀ β |] ]) ∷ []) ⇒ᵀ [| (varᵀ β) |]

List : user-defined {mix-var} 
List = dataᵀ List-name whereᵀ (nil ∷ cons ∷ [])

List[_] = λ x → data-typeᵀ List [ [| x |] ]
cons[_,_] = λ x y → dc cons (x ¦ y ¦ [||])
nil[] = dc nil [||]

Finally, we justify the application of List to type expressions.

⊢nil : Γα ∥ ∅ ⊢ᶜ nil
⊢nil = dcᵀ-intro {G = List-name} ∗ (var-intro ∋-last , ∗)

⊢cons : Γβ ∥ ∅ ⊢ᶜ cons
⊢cons = dcᵀ-intro {G = List-name} (var-intro ∋-last , app-intro (var-intro ∋-last , ∗) ∋-last , ∗) (var-intro ∋-last , ∗)

⊢List : ∀ {Γ χ φ} → _ → Γ ∥ χ ⊢ List[ φ ]
⊢List ⊢φ =
  data-intro {k = } {G = List-name}
  {Γcs = Γα ∷ Γβ ∷ []}
  {χcs = ∅ ∷ ∅ ∷ []}
  (⊢nil , ⊢cons , ∗)
  (⊢φ , ∗)