HList.agda

module HList where

open import Agda.Primitive public
  using (Level; lzero; lsuc; _⊔_)

data Σ {l k} (A : Set l) (B : A -> Set k) : Set (l ⊔ k) where
  _,_ : (a : A) -> (B a) -> Σ A B

infixr 3 _,_

data Zero : Set where
  -- Empty

data One : Set where
  *  : One

data Two : Set where
  tt : Two
  ff : Two

_<?>_ : forall {l} {X : Set l} -> X -> X -> Two -> X
_<?>_ A B tt = A
_<?>_ A B ff = B

_+_ : Set -> Set -> Set
A + B = Σ Two (A <?> B)

data Nat : Set where
  z : Nat
  s : Nat -> Nat

{-# BUILTIN NATURAL Nat #-}

data <_ : Nat -> Set where
  z : forall {n : Nat}        -> < (s n)
  s : forall {n : Nat} -> < n -> < (s n)

data Maybe (X : Set) : Set where
  !!  : Maybe X
  !_! : X -> Maybe X

record EndoFunctor (F : Set -> Set) : Set1 where
  field
    map  : forall {S T} -> (S -> T) -> F S -> F T
open EndoFunctor {{...}} public

record Eq (X : Set) : Set where
  field
    _==_ : X -> X -> Two
open Eq {{...}} public

data HL (L : Set) : Nat -> Set₁ where
  <>           : HL L 0
  [_of_at_]->_ :
       forall
       {n  : Nat}
    -> (X  : Set)
    -> (x  : X)
    -> (l  : L)
    -> (hl : HL L n)
    ->  HL L (s n)

elem : forall {n : Nat} {L : Set} {{eq : Eq L}} -> HL L n -> L -> Maybe (< n)
elem  <>                     l = !!
elem ([ X of x at l₁ ]-> hl) l with l == l₁
elem ([ X of x at l₁ ]-> hl) l | tt          = ! z !
elem ([ X of x at l₁ ]-> hl) l | ff with elem hl l
elem ([ X of x at l₁ ]-> hl) l | ff | !!     = !!
elem ([ X of x at l₁ ]-> hl) l | ff | ! ix ! = ! s ix !

ty : forall {n : Nat} {L : Set} -> HL L n -> < n -> Set
ty  <>                    ()
ty ([ X of x at l ]-> hl)  z     = X
ty ([ X of x at l ]-> hl) (s ix) = ty hl ix

val : forall {n : Nat} {L : Set} -> (hl : HL L n) -> (ix : < n)-> (ty hl ix)
val  <>                    ()
val ([ X of x at l ]-> hl)  z     = x
val ([ X of x at l ]-> hl) (s ix) = val hl ix

_o_ : forall {l} {A B C : Set l} -> (B -> C) -> (A -> B) -> (A -> C)
f o g = λ x -> f (g x)

infixr 9 _o_

lookup :
     forall
     {n : Nat}
     {L : Set}
     {{eq : Eq L}}
     {{f : EndoFunctor Maybe}}
  -> (hl : HL L n)
  -> L
  -> Maybe (Σ (< n) (ty hl))

lookup hl l = map (\ ix -> ix , val hl ix) (elem hl l)

hl : HL Nat 3
hl = [ One of * at 0 ]-> [ Two of tt at 1 ]-> [ Nat of 10 at 2 ]-> <>

instance eqNat : Eq Nat
eqNat = record { _==_ = _=N=_ }
  where
    _=N=_ : Nat -> Nat -> Two
    z   =N= z   = tt
    s m =N= s n = m =N= n
    _   =N= _   = ff

instance functorMaybe : EndoFunctor Maybe
functorMaybe = record { map = mapM }
  where
    mapM : forall {A B} -> (A -> B) -> Maybe A -> Maybe B
    mapM f !!    = !!
    mapM f ! x ! = ! f x !