The GADT Seq

Here we define the proper GADT Seq of sequences. It will be used several times in the examples.

module seq 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 introduce variables and contexts for the declaration of Seq’s data constructors.

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

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

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

We then define Seq as usual, with a constructor const producing a sequence from a piece of raw data, and a constructor pair making a sequence of pairs from sequences of the pair’s constituent types.

Seq-id : id-TC-var
Seq-id = 

Seq-name : TC-var 
Seq-name = TC Seq-id 

const-id pair-id : id-data-constructor
const-id = 
pair-id = 

const pair : data-constructor 
const = const-id ∷ [ varᵀ α ] ⇒ᵀ [| (varᵀ α) |]
pair = pair-id ∷ (appᵀ Seq-name [ [| varᵀ β |] ] ∷ appᵀ Seq-name [ [| varᵀ γ |] ] ∷ []) ⇒ᵀ [| ((varᵀ β) ×ᵀ (varᵀ γ)) |]

Seq : user-defined {mix-var} 
Seq = dataᵀ Seq-name whereᵀ (const ∷ pair ∷ [])

Seq[_] = λ x → data-typeᵀ Seq [ [| x |] ]
const[_] = λ x → dc const [| x |]
pair[_,_] = λ x y → dc pair (x ¦ y ¦ [||] )

Finally, we justify the application of Seq to a type expression.

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

⊢pair : Γβγ ∥ (∅ , ( , Seq-name)) ⊢ᶜ pair
⊢pair = dcᵀ-intro {G = Seq-name} (app-intro (var-intro (∋-rec ∋-last) , ∗) ∋-last , (app-intro (var-intro ∋-last , ∗) ∋-last , ∗)) (×-intro (var-intro (∋-rec ∋-last) ) (var-intro ∋-last) , ∗)

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