Instantly share code, notes, and snippets. dagit/HList.agda Last active Mar 10, 2019

 module HList where open import Level open import Data.Bool open import Data.Nat hiding (_⊔_) open import Data.Vec open import Data.List data HList {a} : List (Set a) → Set (Level.suc a) where [] : HList [] _∷_ : {HeadT : Set a}{TailT : List (Set a)} (x : HeadT) (xs : HList TailT) → HList (HeadT ∷ TailT) data HVec {a} : (n : ℕ) → Vec (Set a) n → Set (Level.suc a) where [] : HVec 0 [] _∷_ : ∀{m}{HeadT : Set a}{TailT : Vec (Set a) m} (x : HeadT) (xs : HVec m TailT) → HVec (ℕ.suc m) (HeadT ∷ TailT) test₁ : HVec 3 (Bool ∷ ℕ ∷ List Bool ∷ []) test₁ = true ∷ 5 ∷ (true ∷ false ∷ []) ∷ [] test₂ : HList (Vec ℕ 1 ∷ ℕ ∷ Bool ∷ []) test₂ = x ∷ 0 ∷ true ∷ [] where x : Vec ℕ 1 x = 1 ∷ [] {- These are simpler definitions if you prefer not to deal with levels. data HList : List Set → Set₁ where [] : HList [] _∷_ : {HeadT : Set }{TailT : List Set} (x : HeadT) (xs : HList TailT) → HList (HeadT ∷ TailT) data HVec : (n : ℕ) → Vec Set n → Set₁ where [] : HVec 0 [] _∷_ : ∀{m}{HeadT : Set }{TailT : Vec Set m} (x : HeadT) (xs : HVec m TailT) → HVec (ℕ.suc m) (HeadT ∷ TailT) -}

SamuraiJack commented May 18, 2018

 Does not seem to work for the empty HList?

SamuraiJack commented May 18, 2018

 Requires explicit level