extensible_rec.idr

{-
  See: http://lpaste.net/104020
  and https://github.com/gonzaw/extensible-records
-}
module Record

import Data.List

%default total

data HList : List Type -> Type where
  Nil : HList []
  (::) : a -> HList xs -> HList (a :: xs)

infix 5 :=

data Field : lbl -> Type -> Type where
  (:=) : (label : lbl) ->
          (value : b) -> Field label b

labelsOf : List (lbl, Type) -> List lbl
labelsOf [] = []
labelsOf ((label, _) :: xs) = label :: labelsOf xs

toFields : List (lbl, Type) -> List Type
toFields [] = []
toFields ((l, t) :: xs) = (Field l t) :: toFields xs

data IsSet : List t -> Type where
  IsSetNil : IsSet []
  IsSetCons : Not (Elem x xs) -> IsSet xs -> IsSet (x :: xs)

data Record : List (lty, Type) -> Type where
  MkRecord : IsSet (labelsOf ts) -> HList (toFields ts) ->
                                    Record ts

infixr 6 +:

rnil : Record []
rnil = MkRecord IsSetNil []

prepend : { label : lbl,
          xs : List (lbl, Type),
          prf : Not (Elem label (labelsOf xs))
        } ->
        Field label t ->
        Record xs ->
        Record ((label, t) :: xs)
prepend {prf} f (MkRecord isSet fs) = MkRecord (IsSetCons prf isSet) (f :: fs)

unitOrVoid : DecEq lbl => lbl -> List (lbl, Type) -> Type
unitOrVoid label ts with (isElem label $ labelsOf ts)
    | (Yes prf) = Void
    | (No no) = Unit

(+:) : DecEq lbl =>
  { label : lbl, xs : List (lbl, Type) } ->
  { default () witness : (unitOrVoid label xs) } ->
  Field label t ->
  Record xs ->
  Record ((label, t) :: xs)

(+:) {witness} {label} {xs} f r with (isElem label $ labelsOf xs)
    | (Yes prf) = absurd witness
    | (No no) = prepend {prf = no} f r

foo : Record [("Book", String), ("Year", Integer)]
foo = ("Book" := "yolo") +: ("Year" := 1234) +: rnil


-- Valid and compiles
-- ("Book" := "yolo") +: ("Year" := 1234) +: rnil
-- Wont compile
-- ("Year" := "yolo") +: ("Year" := 1234) +: rnil