extensible records

records.idr

module Main
import Data.String
import Data.Maybe
import Data.List
import Data.List.Elem
import Data.Vect
import Data.Morphisms
import Decidable.Equality

infixr 10 :->
infixr 10 !!
infixr 3 <*~>
infixr 4 <$~>

LabelledSpecs : Type -> Type
LabelledSpecs k = List (String, k)

data RecordEntry : (k -> Type) -> String -> k -> Type where
  (:->) : {0 a : k} -> (0 s:String) -> f a -> RecordEntry f s a

data RecordList : (k -> Type) -> LabelledSpecs k -> Type where
    Nil : RecordList c Nil
    (::) :  {s:String}
         -> {0 f:k -> Type} 
         -> {t: k}
         -> RecordEntry f s t
         -> RecordList f xs
         -> RecordList f ((s, t) :: xs)

AllConstraints : (a -> Type) -> List a -> Type
AllConstraints f [] = ()
AllConstraints f (c::cs) = (f c, AllConstraints f cs)

OverSpec : (k -> Type) -> (String, k) -> Type
OverSpec c (name, value) = c value

AllSpecs : (k -> Type) -> LabelledSpecs k -> Type
AllSpecs c = AllConstraints (OverSpec c)

-- proof that the spec has some field with a given type.
data HasField : (s:String) -> (t:k) -> LabelledSpecs k -> Type where
  [search s]
  FirstField : HasField s t ((s, t) :: _)
  NextField : (0 prf : (t == s) === False) => HasField s v xs -> HasField s v ((t, w) :: xs)
%builtin Natural HasField

implementation Uninhabited (HasField s t []) where
  uninhabited FirstField impossible
  uninhabited NextField impossible

HasField' : LabelledSpecs k -> (String, k) -> Type
HasField' r (s, t) = HasField s t r

HasFields : (l:LabelledSpecs k) -> LabelledSpecs k -> Type
HasFields l r = AllConstraints (HasField' r)  l

remField : LabelledSpecs k -> (String, k) -> LabelledSpecs k
remField [] _ = []
remField ((s, k) :: specs) (t, l) = 
  if (s == t) then specs else (s, k) :: remField specs (t, l)

remFields :  (l:LabelledSpecs k)
          -> LabelledSpecs k 
          -> LabelledSpecs k
remFields spec [] = spec
remFields spec (x :: xs) = remFields (remField spec x) xs

data NubFields : LabelledSpecs k -> LabelledSpecs k -> LabelledSpecs k ->Type where
  MkNubFields : {spec:LabelledSpecs k} -> {fields: LabelledSpecs k} -> NubFields spec fields (remFields spec fields)

data WithRecordFields :  LabelledSpecs k
                      -> LabelledSpecs k 
                      -> LabelledSpecs k
                      -> LabelledSpecs k 
                      -> Type where
  MkWithRecordFields :  {spec:LabelledSpecs k} 
                     -> {mandatory: LabelledSpecs k}
                     -> {optional: LabelledSpecs k}
                     -> {other: LabelledSpecs k}
                     -> HasFields spec mandatory
                     => NubFields spec (optional ++ mandatory) other
                     => WithRecordFields spec mandatory optional other

data Record : (k -> Type) -> LabelledSpecs k -> Type where
  MkRecord : RecordList f l -> Record f l

listView : Record f s -> RecordList f s
listView (MkRecord x) = x

RecordEntryType : (s:String) -> (l:LabelledSpecs k) -> (k -> Type) -> HasField s t l  => Type
RecordEntryType s ((s, t) :: _) f @{FirstField}= f t
RecordEntryType s (_ :: xs) f @{NextField x}= RecordEntryType s xs f

mkRecord : RecordList f l -> Record f l
mkRecord = MkRecord

hasFieldToIndex : HasField s t r -> Integer
hasFieldToIndex FirstField = 0
hasFieldToIndex (NextField prevField) = 1 + hasFieldToIndex prevField
%builtin NaturalToInteger natToInteger

get : (0 s:String) -> HasField s t r => Record f r -> (f t)
get @{FirstField} s (MkRecord (_ :-> v :: _)) = v
get @{NextField later} s (MkRecord (_ :: r)) = get @{later} s (MkRecord r)

getMaybe : {r : LabelledSpecs k} -> (0 s:String) -> Record f r -> Maybe (f t)
getMaybe s (MkRecord []) = Nothing
getMaybe t (MkRecord ((s :-> z) :: y))

FooRecord : (Type -> Type) -> Type
FooRecord f = Record f [("anint", Int), ("astring", String)]

testx : FooRecord Prelude.id
testx = mkRecord ["anint" :-> 3, "astring" :-> "foo"]

foo : HasFields [("anint", Int), ("astring", String)] r => Record Prelude.id r -> String
foo x = show (get "anint" x) ++ get "astring" x

data Any : Type where 
  MkAny : a -> Any

getAny : Any -> a
getAny (MkAny a) = believe_me a

getTypeOf : {a:Type} -> a -> Type
getTypeOf {a=tp} _ = tp

mapRecordList : ({a : k} -> f a -> g a) -> RecordList f l -> RecordList g l
mapRecordList f [] = []
mapRecordList f ((s :-> v) :: y) = (s :-> f v) :: mapRecordList f y

fillRecordList : (l:LabelledSpecs k) -> (forall a. f a) -> RecordList f l
fillRecordList [] v = []
fillRecordList ((s, x) :: xs) v = s :-> v :: fillRecordList xs v

mapRecord : ({a : k} -> f a -> g a) -> Record f l -> Record g l
mapRecord f (MkRecord x) = MkRecord $ mapRecordList f x

zipWithRecordList :  ({a : k} -> f a -> g a -> h a)
                  -> RecordList f l 
                  -> RecordList g l
                  -> RecordList h l
zipWithRecordList f [] [] = []
zipWithRecordList f (s :-> x :: z) (s :-> y :: w) = 
  s :-> f x y :: zipWithRecordList f z w

zipWithRecord :  ({a : k} -> f a -> g a -> h a)
              -> Record f l 
              -> Record g l
              -> Record h l
zipWithRecord f (MkRecord rl1) (MkRecord rl2) = MkRecord $ zipWithRecordList f rl1 rl2              


-- natural transformation
(~>) : (k -> Type) -> (k -> Type) -> k -> Type
(~>) f g a = f a -> g a

(<$~>) : ({a : k} -> f a -> g a) -> Record f l -> Record g l
(<$~>) = mapRecord

(<*~>) : Record (f ~> g) l -> Record f l -> Record g l
(<*~>) = zipWithRecord ($)

foldMapRecordList : Monoid m => ({a : Type} -> f a -> m) -> RecordList f l -> m
foldMapRecordList f [] = neutral
foldMapRecordList f ((s :-> x) :: y) = f x <+> foldMapRecordList f y

foldrRecordList : ({a : Type} -> f a -> acc -> acc) -> acc -> RecordList f l -> acc
foldrRecordList f acc [] = acc
foldrRecordList f acc ((s :-> x) :: y) =  f x $ foldrRecordList f acc y

foldlRecordList : ({a : Type} -> acc -> f a -> acc) -> acc -> RecordList f l -> acc
foldlRecordList f acc [] = acc
foldlRecordList f acc ((s :-> x) :: y) = foldlRecordList f (f acc x) y

recordListLabels : {l : LabelledSpecs k} -> RecordList (const String) l
recordListLabels {l = []} = []
recordListLabels {l = ((lbl, x) :: xs)} = (lbl :-> lbl) :: recordListLabels {l = xs}

recordLabels : {l : _} -> Record (const String) l
recordLabels = MkRecord $ recordListLabels {l}

recordListDicts : (0 c : k -> Type) -> (l : LabelledSpecs k) -> (cs : AllSpecs c l) => RecordList c l
recordListDicts _ [] = []
recordListDicts c ((s, x) :: xs) {cs=(c1,_)} = (s :-> c1) :: recordListDicts c xs

recordDicts : (0 c : k -> Type) -> (l : LabelledSpecs k) -> (cs : AllSpecs c l) => Record c l
recordDicts c l {cs} = MkRecord $ recordListDicts c l {cs=cs}