{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE OverlappingInstances #-}
{-# LANGUAGE UndecidableInstances #-}

{- 
   poor man's extensible and concatenable records

   supporting both scoped and unique label records

     class Label label  | record field labels
     label := value     | record fields

   predicates:

     rec `Lacks` label  | lacks predicate: record lacks field label
     rA `Disjoint` rB   | record disjointness: records share no field labels

   scoped records operations:

     field :# rec       | record extension
     rec #? label       | field selection
     rec #- label       | field removal
    (rec #! label) val  | field update: update field label with value
    (rec #@ old) new    | field renaming: rename existing field label old to new
     recA ## recB       | symmetric record concatenation
     recA #^ recB       | left-biased record field type intersection
     recA #^^ recB      | left-biased record field label intersection
     recA #& recB       | record projection: for each recB field, select matching recA field

   other record operations: 

     field !:# rec      | strict record extension: no duplicate field labels
     rec !#- label      | strict field removal: remove existing field label from rec
    (rec !#! label) val | strict field update: update existing field label with value
     recA !## recB      | symmetric disjoint record concatenation
     recA !#& recB      | strict record projection: permute recA to match recB

   types:

      class Label l where label :: l
      class Has label rec lbool | label rec -> lbool
      class Lacks rec label
      class Disjoint recA recB

      label :: (Label l) => l
      (:=) :: label -> value -> label := value

      (:#) :: field -> record -> field :# record
      (!:#) :: (Lacks rec label) => (label := val) -> rec -> (label := val) :# rec

      (#?) :: (Select label val rec) => rec -> label -> val

      (#-) :: (Remove label rec rec') => rec -> label -> rec'
      (!#-) :: (Has label rec LTrue, Remove label rec rec') => rec -> label -> rec'

      (#!) :: (Remove label rec rec') => rec -> label -> value -> (label := value) :# rec'
      (!#!) :: (Has label rec LTrue, Remove label rec rec') 
            => rec -> label -> value -> (label := value) :# rec'

      (#@) :: (Remove label1 rec rec', Select label1 val rec) 
           => rec -> label -> label1 -> (label := val) :# rec'

      (##) :: (Concat recA recB recAB) => recA -> recB -> recAB
      (!##) :: (recA `Disjoint` recB, Concat recA recB recAB) => recA -> recB -> recAB

      (#^) :: (Intersect recA recB recAB) => recA -> recB -> recAB
      (#^^) :: (Intersect' recA recB recAB) => recA -> recB -> recAB

      (#&) :: (Project recA recB) => recA -> recB -> recB
      (!#&) :: (Project' recA recB) => recA -> recB -> recB

   see main at the bottom for examples of use.

   please let me know of any practically relevant missing operations

   Claus Reinke
   
   February 2006:
     submitted to support proposal for first class labels in Haskell'

   November 2007: 
    added many more operations and predicates, replaced pairs with 
    symbolic constructors, added strict operations
-}

module Data.Record where
import Data.List(intercalate)

-- | record field labels
class Label l where label :: l

-- | record fields
infixr 1 :=
data label := value = label := value deriving Show

-- | record extension
infixr 0 :#
data field :# record = field :# record deriving Show

-- | strict record extension: no duplicate field labels
infixr 0 !:#
(!:#) :: (record `Lacks` label) => (label := val) -> record -> (label := val) :# record
field !:# record = field :# record

-- | field selection: select field label with type val from record
infixl #?

class Select label val record | label record -> val where
  (#?) :: record -> label -> val

instance Select label val ((label:=val):#r) where
  ((_:=val):#_) #? label = val

instance Select label val r => Select label val (l:#r) where
  (_:#r)       #? label = r #? label

class SelectAux label val record lbool
instance SelectAux label val record LFalse
instance Select label val record => SelectAux label val record LTrue

-- | field removal: remove field label from record
infixl #-

class Remove label record record' | label record -> record' where
  (#-) :: record -> label -> record'  

instance Remove label () () where
  () #- label = ()

{- why do things the easy way if there's a complicated way, too? -}

data LTrue  = LTrue deriving Show
data LFalse = LFalse deriving Show

class    MkBool lbool  where mkBool :: lbool
instance MkBool LTrue  where mkBool = LTrue
instance MkBool LFalse where mkBool = LFalse

class TNot b nb | b -> nb, nb -> b where tnot :: b -> nb
instance TNot LTrue LFalse where tnot _ = LFalse
instance TNot LFalse LTrue where tnot _ = LTrue

class    Has label record lbool | label record -> lbool
instance Has label () LFalse
instance Has label ((label:=val):#r) LTrue
instance Has label r lbool => Has label (l:#r) lbool

instance (RHead r h, MkBool lbool, Has label h lbool, RemoveAux label r r' lbool) 
         => Remove label r r' where
  record #- label = removeAux record label (mkBool::lbool)

class RHead r h | r -> h

instance RHead ((l:=v):#r) ((l:=v):#())

class RemoveAux label record record' lbool | label record lbool -> record' where
  removeAux :: record -> label -> lbool -> record'  

instance RemoveAux label (l:#r) r LTrue where
  removeAux (l:#r) label _ = r

instance Remove label r r' => RemoveAux label (l:#r) (l:#r') LFalse where
  removeAux (l:#r) label _ = (l:# (r #- label))

{-
  wouldn't this be nice and simple? unfortunately, GHC
  complains that the very one substitution instance of the
  3rd rule that we are not interested in is in conflict
  with the functional dependency..

class Remove label record record' | label record -> record' where
  (#-) :: record -> label -> record'  

instance Remove label () () where
  () #- label = ()

instance Remove label ((label:=val):#r) r where
  (_:#r) #- label = r

instance Remove label r r' => Remove label (l:#r) (l:#r') where
  (l:#r) #- label = (l:# (r #- label))
-}

-- | strict field removal: remove field label from record, only if field exists
infixl !#-
(!#-) :: (Has label record LTrue, Remove label record record') => record -> label -> record'
record !#- label = record #- label

-- | lacks: record lacks field label
class Lacks record label
instance Remove label record record => Lacks record label

-- | field update: update field label with value
infix #!

record #! label = \value->((label:=value) :# (record #- label))

-- | strict field update: update existing field label with value
infix !#!

record !#! label = \value->((label:=value) :# (record !#- label))

-- | field renaming: rename existing field oldlabel to newlabel
infix #@

record #@ newlabel = \oldlabel->((newlabel:=record #? oldlabel) :# (record #- oldlabel))

-- | symmetric record concatenation: concatenate fields of recA and recB
infixr ##

class Concat recA recB recAB | recA recB -> recAB where
  (##) :: recA -> recB -> recAB

instance Concat () recB recB where
  _ ## recB = recB

instance Concat (lA:#()) recB (lA:#recB) where
  (lA:#()) ## recB = (lA:#recB)

instance Concat rA recB recRAB => Concat (lA:#rA) recB (lA:#recRAB) where
  (lA:#rA) ## recB = (lA :# (rA ## recB))

-- | strict symmetric record concatenation: concatenate fields of disjoint recA and recB
infixr !##
(!##) :: (recA `Disjoint` recB, Concat recA recB recAB) => recA -> recB -> recAB
recA !## recB = recA ## recB

-- | left-biased record field type intersection: select sub-record of recA whose field types occur in recB
-- fields with different types on shared labels are an error
infixr #^

class Intersect recA recB recAB | recA recB -> recAB where
  (#^) :: recA -> recB -> recAB

instance (Label l, Has l recB b, SelectAux l v recB b, TNot b nb
         ,RemoveAux l ((l:=v):#()) recAB nb) 
      => Intersect ((l:=v):#()) recB recAB
  where ((l:=v):#()) #^ recB = removeAux ((l:=v):#()) l (undefined::nb)

instance (Label l, Has l recB b, SelectAux l v recB b, TNot b nb
         ,Intersect recA recB recAB', RemoveAux l ((l:=v):#()) first nb
         ,Concat first recAB' recAB) 
      => Intersect ((l:=v):#recA) recB recAB
  where ((l:=v):#recA) #^ recB = (removeAux ((l:=v):#()) l (undefined::nb)) ## (recA #^ recB)


-- | left-biased record field label intersection: select sub-record of recA whose field types occur in recB
-- fields with different types on shared labels are taken from recA
infixr #^^

class Intersect' recA recB recAB | recA recB -> recAB where
  (#^^) :: recA -> recB -> recAB

instance (Label l, Has l recB b, TNot b nb
         ,RemoveAux l ((l:=v):#()) recAB nb) 
      => Intersect' ((l:=v):#()) recB recAB
  where ((l:=v):#()) #^^ recB = removeAux ((l:=v):#()) l (undefined::nb)

instance (Label l, Has l recB b, TNot b nb
         ,Intersect' recA recB recAB', RemoveAux l ((l:=v):#()) first nb
         ,Concat first recAB' recAB) 
      => Intersect' ((l:=v):#recA) recB recAB
  where ((l:=v):#recA) #^^ recB = (removeAux ((l:=v):#()) l (undefined::nb)) ## (recA #^^ recB)

-- | record disjointness: records share no field labels
class Disjoint recA recB
instance Disjoint () recB
instance (Label l, recB `Lacks` l, Disjoint recA recB)
      => Disjoint ((l:=v):#recA) recB

-- | record projection: select sub-record of recA that type-matches recB
infixr #&

class Project recA recB where
  (#&) :: recA -> recB -> recB

instance (Label l, Select l v recA) 
      => Project recA ((l:=v):#()) 
  where recA #& _ = ((l:=recA #? l):# ())
          where l = label::l

instance (Label l, Select l v recA, Project recA recB) 
      => Project recA ((l:=v):#recB) 
  where recA #& _ = ((l:=recA #? l) :# (recA #& (undefined::recB)))
          where l = label::l

-- | strict record projection: permute recA to type-match recB
infixr !#&

class Project' recA recB where
  (!#&) :: recA -> recB -> recB

instance Project' ((l:=v):#()) ((l:=v):#()) where
 recA !#& _ = recA

instance (Label l, Select l v recA, Remove l recA recA', Project' recA' recB) 
      => Project' recA ((l:=v):#recB) where
 recA !#& _ = ((l:=recA #? l) :# ((recA #- l) !#& (undefined::recB)))
  where l = label::l

-- some labels and examples

data A = A deriving Show; instance Label A where label = A
data B = B deriving Show; instance Label B where label = B
data C = C deriving Show; instance Label C where label = C
data D = D deriving Show; instance Label D where label = D

r1 = ((A:=True) :# ((B:='a') :# ((C:=1) :# ())))

r2 = ((A:=False) :# ((B:='b') :# ((C:=2) :# r1)))

r3 = ((D:="hi there") :# ((B:=["who's calling"]) :# ()))

r4a = r1 ## r3
r4b = r3 ## r1

x1 r = (r #? B, r #? C, r #? A)

x2 r = (r #? B, r #? D)

x3 r = r #- D #- B

l1 = [r1, r2 #& r1, r4a #& r1, (r4b #- B) #& r1]

l2 = [(r1 #& r) !#& r, ((r2 #& r1) #- C) !#& r, ((r4a #& r1) #- C) !#& r, (r4b #- B #- D #- C) !#& r]
  where r = undefined::(B:=Char):#(A:=Bool):#()

f1 :: (record `Lacks` A) => record -> record
f1 = id

d :: (recA `Disjoint` recB) => recA -> recB -> ()
d _ _ = ()

test = do
  putStrLn "\nsome records"
  putStrLn $ "r1 : "++ show r1
  putStrLn $ "r2 : "++ show r2
  putStrLn $ "r3 : "++ show r3
  putStrLn "\nsymmetric record concatenation"
  putStrLn $ "r4a = r1 ## r3:\n\t"++ show r4a
  putStrLn $ "r4b = r3 ## r1:\n\t"++ show r4b
  putStrLn "\nrecord selection"
  putStrLn "\nx1 r = (r #? B, r #? C, r #? A)"
  putStrLn $ "x1 r1: "++ show (x1 r1)
  putStrLn $ "x1 r2: "++ show (x1 r2)
  putStrLn $ "x1 r4a: "++ show (x1 r4a)
  putStrLn $ "x1 r4b: "++ show (x1 r4b)
  putStrLn "\nx2 r = (r #? B, r #? D)\n"
  putStrLn $ "x2 r4a: "++ show (x2 r4a)
  putStrLn $ "x2 r4b: "++ show (x2 r4b)
  putStrLn "\nrecord field removal"
  putStrLn "\nx3 r = r #- D #- B\n"
  putStrLn $ "x3 r1: "++ show (x3 r1)
  putStrLn $ "x3 r2: "++ show (x3 r2)
  putStrLn $ "x3 r3: "++ show (x3 r3)
  putStrLn $ "x3 r4a: "++ show (x3 r4a)
  putStrLn $ "x3 r4b: "++ show (x3 r4b)
  putStrLn "\nstrict record field removal"
  putStrLn $ "\nr1 !#- B :\n\t" ++ show (r1 !#- B)
  putStrLn "\nrecord field update"
  putStrLn $ "\n(r2 #! B) \"dingbats\":\n\t"++ show ((r2 #! B) "dingbats")
  putStrLn "\nrecord field renaming"
  putStrLn $ "\n(r2 #@ D) C:\n\t"++ show ((r2 #@ D) C)
  putStrLn "\nrecord projection, lists of projected records"
  putStrLn $ "\nl1 = [r1, r2 #& r1, r4a #& r1, (r4b #- B) #& r1]\n"
            ++"\n    l1: ["++intercalate "\n\t," (map show l1)++"]"
  putStrLn "\nrecord field type intersection"
  putStrLn $ "\nr1 #^ r2: " ++ show (r1 #^ r2)
  putStrLn "\nleft-biased record field label intersection"
  putStrLn $ "\nr1 #^^ r3: " ++ show (r1 #^^ r3)
  putStrLn $ "\nr4a #^^ r4b: " ++ show (r4a #^^ r4b)
  putStrLn $ "\nr4b #^^ r4a: " ++ show (r4b #^^ r4a)
  putStrLn "\nrecord permutation, lists of permuted records"
  putStrLn $ "\nl2 = [(r1 #& r) !#& r, ((r2 #& r1) #- C) !#& r"
            ++", ((r4a #& r1) #- C) !#& r, (r4b #- B #- D #- C) !#& r]"
            ++"\n  where r = undefined::(B:=Char):#(A:=Bool):#()\n"
            ++"\n    l2: ["++intercalate "\n\t," (map show l2)++"]"
  putStrLn "\n(record `Lacks` field) predicate"
  putStrLn $ "\nf1 :: (record `Lacks` A) => record -> record"
          ++ "\nf1 = id\n"
          ++ "\nf1 (r1 #- A):\n\t" ++ show (f1 (r1 #- A))
  putStrLn "\n(recA `Disjoint` recB) predicate"
  putStrLn $ "\nd :: (recA `Disjoint` recB) => recA -> recB -> ()"
          ++ "\nd _ _ = ()\n"
          ++ "\nd r1 (r3 #- B):\n\t" ++ show (d r1 (r3 #- B))
  putStrLn ""