HList.agda

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

Requires explicit level