Schema.idr

data HList : List Type -> Type where
  Nil : HList []
  (::) : t -> HList ts -> HList (t :: ts)
%name HList xs,ys

append : HList ts -> HList ts' -> HList (ts ++ ts')
append []        ys = ys
append (x :: xs) ys = x :: append xs ys

--------------------------------

data Column = TEXT | REAL | INTEGER

Table : Type
Table = List (String, Column)


interpCol : Column -> Type
interpCol TEXT    = String
interpCol REAL    = Double
interpCol INTEGER = Integer

interp : Table -> Type
interp schema = HList (map (interpCol . snd) schema)

PeopleSchema : Table
PeopleSchema = [("Name", TEXT), ("Hamsters", INTEGER)]

People : List (interp PeopleSchema)
People = [["David", 1], ["Edwin", 0]]

total
countHamsters : List (interp PeopleSchema) -> Integer
countHamsters []             = 0
countHamsters ([_, h] :: xs) = h + countHamsters xs