-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | Open records using closed type families.
--   
@package CTRex
@version 0.6


-- | This module implements extensible records using closed type famillies.
--   
--   See the <a>examples</a>.
--   
--   Lists of (label,type) pairs are kept sorted thereby ensuring that { x
--   = 0, y = 0 } and { y = 0, x = 0 } have the same type.
--   
--   In this way we can implement standard type classes such as Show, Eq,
--   Ord and Bounded for open records, given that all the elements of the
--   open record satify the constraint.
module Data.OpenRecords

-- | A label
data Label (s :: Symbol)
Label :: Label

-- | This class gives the integer associated with a type-level symbol.
--   There are instances of the class for every concrete literal: "hello",
--   etc.
--   
--   <i>Since: 4.7.0.0</i>
class KnownSymbol (n :: Symbol)

-- | A record with row r.
data Rec (r :: Row *)

-- | The kind of rows. This type is only used as a datakind. A row is a
--   typelevel entity telling us which symbols are associated with which
--   types.
data Row a

-- | The empty record
empty :: Rec Empty

-- | Type level variant of <a>empty</a>

-- | Record extension. The row may already contain the label, in which case
--   the origin value can be obtained after restriction (<a>.-</a>) with
--   the label.
extend :: KnownSymbol l => Label l -> a -> Rec r -> Rec (Extend l a r)

-- | Record extension without shadowing. The row may not already contain
--   label l.
extendUnique :: (KnownSymbol l, r :\ l) => Label l -> a -> Rec r -> Rec (Extend l a r)

-- | Type level operations of <a>extend</a> and <a>extendUnique</a>

-- | Rename a label. The row may already contain the new label , in which
--   case the origin value can be obtained after restriction (<a>.-</a>)
--   with the new label.
rename :: (KnownSymbol l, KnownSymbol l') => Label l -> Label l' -> Rec r -> Rec (Rename l l' r)

-- | Rename a label. The row may not already contain the new label.
renameUnique :: (KnownSymbol l, KnownSymbol l', r :\ l') => Label l -> Label l' -> Rec r -> Rec (Rename l l' r)

-- | Type level operation of <a>rename</a> and <a>renameUnique</a>

-- | Record restriction. Delete the label l from the record.
(.-) :: KnownSymbol l => Rec r -> Label l -> Rec (r :- l)

-- | Type level operation of <a>.-</a>

-- | Update the value associated with the label.
update :: KnownSymbol l => Label l -> r :! l -> Rec r -> Rec r

-- | Record selection
(.!) :: KnownSymbol l => Rec r -> Label l -> r :! l

-- | Type level operation of <a>.!</a>

-- | Record union (not commutative)
(.++) :: Rec l -> Rec r -> Rec (l :++ r)

-- | Type level operation of <a>.++</a>

-- | Record disjoint union (commutative)
(.+) :: Disjoint l r => Rec l -> Rec r -> Rec (l :+ r)

-- | Type level operation of <a>.+</a>

-- | Does the row lack (i.e. it has not) the specified label?
type (:\) r l = LacksP l r ~ LabelUnique l

-- | Are the two rows disjoint? (i.e. their sets of labels are disjoint)
type Disjoint l r = DisjointR l r ~ IsDisjoint
class Labels (r :: Row *)
labels :: Labels r => Rec r -> [String]

-- | If the constaint <tt>c</tt> holds for all elements in the row
--   <tt>r</tt>, then the methods in this class are available.
class Forall (r :: Row *) (c :: * -> Constraint)
rinit :: Forall r c => CWit c -> (forall a. c a => a) -> Rec r
erase :: Forall r c => CWit c -> (forall a. c a => a -> b) -> Rec r -> [b]
eraseZip :: Forall r c => CWit c -> (forall a. c a => a -> a -> b) -> Rec r -> Rec r -> [b]

-- | A witness of a constraint. For use like this <tt>rinit (CWit :: CWit
--   Bounded) minBound</tt>
data CWit (c :: * -> Constraint)
data FWit (f :: * -> *)

-- | Here we provide a datatype for denoting record operations. Use
--   <a>.|</a> to actually apply the operations.
--   
--   This allows us to chain operations with nicer syntax. For example we
--   can write:
--   
--   <pre>
--   p :&lt;-| z .| y :&lt;- 'b' .| z :!= False .| x := 2 .| y := 'a' .| empty
--   </pre>
--   
--   Which results in:
--   
--   <pre>
--   { p=False, x=2, y='b' }
--   </pre>
--   
--   Without this sugar, we would have written it like this:
--   
--   <pre>
--   rename z p $ update y 'b' $ extendUnique z False $ extend x 2 $ extend y 'a' empty
--   </pre>
--   
--   <ul>
--   <li><i><tt>:&lt;-</tt></i> Record update. Sugar for
--   <a>update</a>.</li>
--   <li><i><tt>:=</tt></i> Record extension. Sugar for <a>extend</a>.</li>
--   <li><i><tt>:!=</tt></i> Record extension, without shadowing. Sugar for
--   <a>extendUnique</a>.</li>
--   <li><i><tt>:&lt;-|</tt></i> Record label renaming. Sugar for
--   <a>rename</a>.</li>
--   <li><i><tt>:&lt;-!</tt></i> Record label renaming. Sugar for
--   <a>renameUnique</a>.</li>
--   </ul>
data RecOp (c :: Row * -> Constraint) (rowOp :: RowOp *)
(:<-) :: Label l -> a -> RecOp (HasType l a) RUp
(:=) :: Label l -> a -> RecOp NoConstr (l ::= a)
(:!=) :: Label l -> a -> RecOp (Lacks l) (l ::= a)
(:<-|) :: Label l' -> Label l -> RecOp NoConstr (l' ::<-| l)
(:<-!) :: Label l' -> Label l -> RecOp (Lacks l') (l' ::<-| l)

-- | Type level datakind corresponding to <a>RecOp</a>. Here we provide a
--   datatype for denoting row operations. Use <a>:|</a> to actually apply
--   the type level operation.
--   
--   This allows us to chain type level operations with nicer syntax. For
--   example we can write:
--   
--   <pre>
--   "p" ::&lt;-| "z" :| RUp :| "z" ::= Bool :| "x" ::= Double :| "y" ::= Char :| Empty
--   </pre>
--   
--   As the type of the expression:
--   
--   <pre>
--   p :&lt;-| z .| y :&lt;- 'b' .| z :!= False .| x := 2 .| y := 'a' .| empty
--   </pre>
--   
--   Without this sugar, we would have written it like this:
--   
--   <pre>
--   Rename "p" "z" (Extend "z" Bool (Extend x Double (Extend "x" Int Empty)))
--   </pre>
--   
--   Of course, we can also just write:
--   
--   <pre>
--   "p" ::= Bool :| "x" ::= Double :| "y" ::= Int :|  Empty
--   </pre>
--   
--   instead, doing the computation ourselves, or even let the type infer.
--   
--   <ul>
--   <li><i><tt>RUp</tt></i> Type level equivalent of <a>:&lt;-</a>. Is the
--   identity Row Operation.</li>
--   <li><i><tt>::=</tt></i> Type level equivalent of <a>:=</a>. Row
--   extension. Sugar for <a>Extend</a>.</li>
--   <li><i><tt>::&lt;-|</tt></i> Type level equivalent of <a>:&lt;-|</a>.
--   Row label renaming. Sugar for <a>Rename</a>.</li>
--   </ul>
data RowOp (a :: *)
RUp :: RowOp a
(::=) :: Symbol -> a -> RowOp a
(::<-|) :: Symbol -> Symbol -> RowOp a

-- | Apply an operation to a record.
(.|) :: c r => RecOp c ro -> Rec r -> Rec (ro :| r)

-- | Apply a (typelevel) operation to a row. Type level operation of
--   <a>.|</a>
instance Forall r Bounded => Bounded (Rec r)
instance (Eq (Rec r), Forall r Ord) => Ord (Rec r)
instance Forall r Eq => Eq (Rec r)
instance (Labels r, Forall r Show) => Show (Rec r)
instance (KnownSymbol l, RZipt t1 t2) => RZipt ((l ':-> v1) : t1) ((l ':-> v2) : t2)
instance RZipt '[] '[]
instance RZipt r1 r2 => RowZip ('R r1) ('R r2)
instance (KnownSymbol l, Forall ('R t) c, c a) => Forall ('R ((l ':-> a) : t)) c
instance Forall ('R '[]) c
instance (KnownSymbol l, c v, RMapc c f t) => RMapc c f ((l ':-> v) : t)
instance RMapc c f '[]
instance RMapc c f r => RowMapC c f ('R r)
instance (KnownSymbol l, RowMapx f t) => RowMapx f ((l ':-> v) : t)
instance RowMapx f '[]
instance RowMapx f r => RowMap f ('R r)
instance (KnownSymbol l, Labels ('R t)) => Labels ('R ((l ':-> v) : t))
instance Labels ('R '[])
instance (r :! l) ~ a => HasType l a r
instance r :\ l => Lacks l r
instance NoConstr a
instance KnownSymbol s => Show (Label s)