Create a gist now

Instantly share code, notes, and snippets.

@dagit /HList.agda
Last active Dec 14, 2015

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)
-}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment