Instantly share code, notes, and snippets.

@dagit /HList.agda
Last active May 18, 2018

Embed
What would you like to do?
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

This comment has been minimized.

SamuraiJack commented May 18, 2018

Does not seem to work for the empty HList?

@SamuraiJack

This comment has been minimized.

SamuraiJack commented May 18, 2018

Requires explicit level

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment