Finish record instances and add tests

As far as I can tell, there are now instances for all applicable
typeclasses given for primitive records. I've even added tests, which
typecheck (good news), though I don't think any of them actually run.

Author: Tom Harding

src/Data/BooleanAlgebra.purs

@@ -3,7 +3,7 @@ module Data.BooleanAlgebra
   , module Data.HeytingAlgebra
   ) where
 
-import Data.HeytingAlgebra (class HeytingAlgebra, class HeytingAlgebraRecord, ff, tt, implies, conj, disj, not, (&&), (||))
+import Data.HeytingAlgebra (class HeytingAlgebra, class HeytingAlgebraRow, ff, tt, implies, conj, disj, not, (&&), (||))
 import Data.Unit (Unit)
 import Prim.RowList as RL
 
@@ -23,6 +23,6 @@ instance booleanAlgebraFn :: BooleanAlgebra b => BooleanAlgebra (a -> b)
 
 instance booleanAlgebraRecord
   :: ( RL.RowToList row list
-     , HeytingAlgebraRecord list row row focus
+     , HeytingAlgebraRow list row row focus
      )
   => BooleanAlgebra (Record row)

src/Data/Bounded.purs

@@ -51,40 +51,3 @@ foreign import bottomNumber :: Number
 instance boundedNumber :: Bounded Number where
   top = topNumber
   bottom = bottomNumber
-
--- Similarly to the `OrdRecord` constraint, this implementation is potentially
--- unstable. However, it is left here as a reference:
-
---class BoundedRecord rowlist row subrow focus | rowlist -> subrow focus where
---  bottomRecordImpl :: RLProxy rowlist -> RProxy row -> Record subrow
---  topRecordImpl :: RLProxy rowlist -> RProxy row -> Record subrow
---
---instance boundedRecordNil :: BoundedRecord RL.Nil row () focus where
---  bottomRecordImpl _ _ = {}
---  topRecordImpl _ _ = {}
---
---instance boundedRecordCons
---    :: ( BoundedRecord rowlistTail row subrowTail subfocus
---       , Row.Cons key focus subrowTail subrow
---       , IsSymbol key
---       , Bounded focus
---       )
---    => BoundedRecord (Row.Cons key focus rowlistTail) row subrow focus where
---  bottomRecordImpl _ row
---    = unsafeInsert key (bottom :: focus)
---        (bottomRecordImpl (RLProxy :: RLProxy rowlistTail) row)
---    where key = reflectSymbol (SProxy :: SProxy key)
---
---  topRecordImpl _ row
---    = unsafeInsert key (bottom :: focus)
---        (topRecordImpl (RLProxy :: RLProxy rowlistTail) row)
---    where key = reflectSymbol (SProxy :: SProxy key)
---
---instance boundedRecord
---    :: ( RL.RowToList row list
---       , BoundedRecord list row row focus
---       , OrdRecord list row row focus
---       )
---    => Bounded (Record row) where
---  bottom = bottomRecordImpl (RLProxy :: RLProxy list) (RProxy :: RProxy row)
---  top = topRecordImpl (RLProxy :: RLProxy list) (RProxy :: RProxy row)

src/Data/CommutativeRing.purs

@@ -4,8 +4,8 @@ module Data.CommutativeRing
   , module Data.Semiring
   ) where
 
-import Data.Ring (class Ring, class RingRecord)
-import Data.Semiring (class Semiring, class SemiringRecord, add, mul, one, zero, (*), (+))
+import Data.Ring (class Ring, class RingRow)
+import Data.Semiring (class Semiring, class SemiringRow, add, mul, one, zero, (*), (+))
 import Data.Unit (Unit)
 import Prim.RowList as RL
 
@@ -25,7 +25,7 @@ instance commutativeRingFn :: CommutativeRing b => CommutativeRing (a -> b)
 
 instance commutativeRingRecord
   :: ( RL.RowToList row list
-     , SemiringRecord list row row focus
-     , RingRecord list row row focus
+     , SemiringRow list row row focus
+     , RingRow list row row focus
      )
   => CommutativeRing (Record row)

src/Data/DivisionRing.purs

@@ -7,9 +7,9 @@ module Data.DivisionRing
   , module Data.Semiring
   ) where
 
+import Data.EuclideanRing ((/))
 import Data.Ring (class Ring, negate, sub)
 import Data.Semiring (class Semiring, add, mul, one, zero, (*), (+))
-import Data.EuclideanRing ((/))
 
 -- | The `DivisionRing` class is for non-zero rings in which every non-zero
 -- | element has a multiplicative inverse. Division rings are sometimes also

src/Data/Eq.purs

@@ -2,13 +2,13 @@ module Data.Eq
   ( class Eq, eq, (==), notEq, (/=)
   , class Eq1, eq1, notEq1
 
-  , class EqRecord
+  , class EqRow
   , eqRecordImpl
   ) where
 
 import Data.HeytingAlgebra ((&&))
 import Data.Internal.Record (unsafeGet)
-import Data.RowList (RLProxy(..))
+import Type.Data.RowList (RLProxy(..))
 import Data.Symbol (class IsSymbol, SProxy(..), reflectSymbol)
 import Data.Unit (Unit)
 import Data.Void (Void)
@@ -76,28 +76,29 @@ instance eq1Array :: Eq1 Array where
 notEq1 :: forall f a. Eq1 f => Eq a => f a -> f a -> Boolean
 notEq1 x y = (x `eq1` y) == false
 
-class EqRecord rowlist row focus | rowlist -> focus where
+-- | A typeclass to characterise rows of types that are all Eq..
+class EqRow rowlist row focus | rowlist -> focus where
   eqRecordImpl :: RLProxy rowlist -> Record row -> Record row -> Boolean
 
-instance eqRecordNil :: EqRecord RL.Nil row focus where
+instance eqRowNil :: EqRow RL.Nil row focus where
   eqRecordImpl _ _ _ = true
 
-instance eqRecordCons
-    :: ( EqRecord rowlistTail row subfocus
+instance eqRowCons
+    :: ( EqRow rowlistTail row subfocus
        , Row.Cons key focus rowTail row
        , IsSymbol key
        , Eq focus
        )
-    => EqRecord (RL.Cons key focus rowlistTail) row focus where
-  eqRecordImpl _ ra rb
-    = unsafeGet' key ra == unsafeGet key rb
-        && eqRecordImpl (RLProxy :: RLProxy rowlistTail) ra rb
-    where key = reflectSymbol (SProxy :: SProxy key)
-          unsafeGet' = unsafeGet :: String -> Record row -> focus
+    => EqRow (RL.Cons key focus rowlistTail) row focus where
+  eqRecordImpl _ ra rb = (get ra == get rb) && tail
+    where
+      key = reflectSymbol (SProxy :: SProxy key)
+      get = unsafeGet key :: Record row -> focus
+      tail = eqRecordImpl (RLProxy :: RLProxy rowlistTail) ra rb
 
 instance eqRecord
     :: ( RL.RowToList row list
-       , EqRecord list row focus
+       , EqRow list row focus
        )
     => Eq (Record row) where
   eq = eqRecordImpl (RLProxy :: RLProxy list)

src/Data/HeytingAlgebra.purs

@@ -10,7 +10,7 @@ module Data.HeytingAlgebra
   , (&&)
   , (||)
 
-  , class HeytingAlgebraRecord
+  , class HeytingAlgebraRow
   , ffRecordImpl
   , ttRecordImpl
   , impliesRecordImpl
@@ -20,12 +20,12 @@ module Data.HeytingAlgebra
   ) where
 
 import Data.Internal.Record (unsafeGet, unsafeInsert)
-import Data.RowList (RLProxy(..))
 import Data.Symbol (class IsSymbol, SProxy(..), reflectSymbol)
 import Data.Unit (Unit, unit)
 import Prim.Row as Row
 import Prim.RowList as RL
 import Type.Data.Row (RProxy(..))
+import Type.Data.RowList (RLProxy(..))
 
 -- | The `HeytingAlgebra` type class represents types that are bounded lattices with
 -- | an implication operator such that the following laws hold:
@@ -91,81 +91,73 @@ foreign import boolConj :: Boolean -> Boolean -> Boolean
 foreign import boolDisj :: Boolean -> Boolean -> Boolean
 foreign import boolNot :: Boolean -> Boolean
 
-class HeytingAlgebraRecord rowlist row subrow focus | rowlist -> subrow focus where
+class HeytingAlgebraRow rowlist row subrow focus | rowlist -> subrow focus where
   ffRecordImpl :: RLProxy rowlist -> RProxy row -> Record subrow
   ttRecordImpl :: RLProxy rowlist -> RProxy row -> Record subrow
   impliesRecordImpl :: RLProxy rowlist -> Record row -> Record row -> Record subrow
   disjRecordImpl :: RLProxy rowlist -> Record row -> Record row -> Record subrow
   conjRecordImpl :: RLProxy rowlist -> Record row -> Record row -> Record subrow
   notRecordImpl :: RLProxy rowlist -> Record row -> Record subrow
 
-instance heytingAlgebraRecordNil :: HeytingAlgebraRecord RL.Nil row () focus where
+instance heytingAlgebraRowNil :: HeytingAlgebraRow RL.Nil row () focus where
   conjRecordImpl _ _ _ = {}
   disjRecordImpl _ _ _ = {}
   ffRecordImpl _ _ = {}
   impliesRecordImpl _ _ _ = {}
   notRecordImpl _ _ = {}
   ttRecordImpl _ _ = {}
 
-instance heytingAlgebraRecordCons
+instance heytingAlgebraRowCons
     :: ( IsSymbol key
        , Row.Cons key focus subrowTail subrow
-       , HeytingAlgebraRecord rowlistTail row subrowTail subfocus
+       , HeytingAlgebraRow rowlistTail row subrowTail subfocus
        , HeytingAlgebra focus
        )
-    => HeytingAlgebraRecord (RL.Cons key focus rowlistTail) row subrow focus where
-  conjRecordImpl _ ra rb
-    = unsafeInsert key
-        (conj (unsafeGet' key ra) (unsafeGet' key rb))
-        (conjRecordImpl (RLProxy :: RLProxy rowlistTail) ra rb)
-    where key = reflectSymbol (SProxy :: SProxy key)
-          unsafeGet' = unsafeGet :: String -> Record row -> focus
-
-  disjRecordImpl _ ra rb
-    = unsafeInsert key
-        (disj (unsafeGet' key ra) (unsafeGet' key rb))
-        (disjRecordImpl (RLProxy :: RLProxy rowlistTail) ra rb)
-    where key = reflectSymbol (SProxy :: SProxy key)
-          unsafeGet' = unsafeGet :: String -> Record row -> focus
-
-  impliesRecordImpl _ ra rb
-    = unsafeInsert key
-        (implies (unsafeGet' key ra) (unsafeGet' key rb))
-        (impliesRecordImpl (RLProxy :: RLProxy rowlistTail) ra rb)
+    => HeytingAlgebraRow (RL.Cons key focus rowlistTail) row subrow focus where
+  conjRecordImpl _ ra rb = insert (conj (get ra) (get rb)) tail
     where
       key = reflectSymbol (SProxy :: SProxy key)
-      unsafeGet' = unsafeGet :: String -> Record row -> focus
-
-  ffRecordImpl _ _
-    = unsafeInsert key (ff :: focus)
-        ( ffRecordImpl
-            (RLProxy :: RLProxy rowlistTail)
-            (RProxy :: RProxy row)
-        )
+      get = unsafeGet key :: Record row -> focus
+      insert = unsafeInsert key :: focus -> Record subrowTail -> Record subrow
+      tail = conjRecordImpl (RLProxy :: RLProxy rowlistTail) ra rb
+
+  disjRecordImpl _ ra rb = insert (disj (get ra) (get rb)) tail
+    where
+      key = reflectSymbol (SProxy :: SProxy key)
+      get = unsafeGet key :: Record row -> focus
+      insert = unsafeInsert key :: focus -> Record subrowTail -> Record subrow
+      tail = disjRecordImpl (RLProxy :: RLProxy rowlistTail) ra rb
+
+  impliesRecordImpl _ ra rb = insert (implies (get ra) (get rb)) tail
     where
       key = reflectSymbol (SProxy :: SProxy key)
-      unsafeGet' = unsafeGet :: String -> Record row -> focus
+      get = unsafeGet key :: Record row -> focus
+      insert = unsafeInsert key :: focus -> Record subrowTail -> Record subrow
+      tail = impliesRecordImpl (RLProxy :: RLProxy rowlistTail) ra rb
+
+  ffRecordImpl _ row = insert ff tail
+    where
+      key = reflectSymbol (SProxy :: SProxy key)
+      insert = unsafeInsert key :: focus -> Record subrowTail -> Record subrow
+      tail = ffRecordImpl (RLProxy :: RLProxy rowlistTail) row
 
   notRecordImpl _ row
-    = unsafeInsert key (not (unsafeGet' key row))
-        (notRecordImpl (RLProxy :: RLProxy rowlistTail) row)
+    = insert (not (get row)) tail
     where
       key = reflectSymbol (SProxy :: SProxy key)
-      unsafeGet' = unsafeGet :: String -> Record row -> focus
-
-  ttRecordImpl _ _
-    = unsafeInsert key (tt :: focus)
-        ( ttRecordImpl
-            (RLProxy :: RLProxy rowlistTail)
-            (RProxy :: RProxy row)
-        )
+      get = unsafeGet key :: Record row -> focus
+      insert = unsafeInsert key :: focus -> Record subrowTail -> Record subrow
+      tail = notRecordImpl (RLProxy :: RLProxy rowlistTail) row
+
+  ttRecordImpl _ row = insert tt tail
     where
       key = reflectSymbol (SProxy :: SProxy key)
-      unsafeGet' = unsafeGet :: String -> Record row -> focus
+      insert = unsafeInsert key :: focus -> Record subrowTail -> Record subrow
+      tail = ttRecordImpl (RLProxy :: RLProxy rowlistTail) row
 
 instance heytingAlgebraRecord
     :: ( RL.RowToList row list
-       , HeytingAlgebraRecord list row row focus
+       , HeytingAlgebraRow list row row focus
        )
     => HeytingAlgebra (Record row) where
   ff = ffRecordImpl  (RLProxy :: RLProxy list) (RProxy :: RProxy row)

src/Data/Monoid.purs

@@ -3,6 +3,9 @@ module Data.Monoid
   , power
   , guard
   , module Data.Semigroup
+
+  , class MonoidRow
+  , memptyRecordImpl
   ) where
 
 import Data.Boolean (otherwise)
@@ -11,10 +14,11 @@ import Data.EuclideanRing (mod, (/))
 import Data.Internal.Record (unsafeInsert)
 import Data.Ord ((<=))
 import Data.Ordering (Ordering(..))
-import Data.RowList (RLProxy(..))
-import Data.Semigroup (class Semigroup, class SemigroupRecord, (<>))
+import Type.Data.RowList (RLProxy(..))
+import Data.Semigroup (class Semigroup, class SemigroupRow, (<>))
 import Data.Symbol (class IsSymbol, SProxy(..), reflectSymbol)
 import Data.Unit (Unit, unit)
+import Prim.Row as Row
 import Prim.RowList as RL
 
 -- | A `Monoid` is a `Semigroup` with a value `mempty`, which is both a
@@ -45,33 +49,33 @@ instance monoidString :: Monoid String where
 instance monoidArray :: Monoid (Array a) where
   mempty = []
 
-class MonoidRecord rowlist row focus | rowlist -> row focus where
-  monoidRecordImpl :: RLProxy rowlist -> Record row
+class MonoidRow rowlist subrow focus | rowlist -> subrow focus where
+  memptyRecordImpl :: RLProxy rowlist -> Record subrow
 
-instance monoidRecordNil :: MonoidRecord RL.Nil () focus where
-  monoidRecordImpl _ = {}
+instance monoidRowNil :: MonoidRow RL.Nil () focus where
+  memptyRecordImpl _ = {}
 
-instance monoidRecordCons
+instance monoidRowCons
     :: ( IsSymbol key
        , Monoid focus
-       , MonoidRecord rowlistTail row subfocus
+       , Row.Cons key focus subrowTail subrow
+       , MonoidRow rowlistTail subrowTail subfocus
        )
-    => MonoidRecord (RL.Cons key focus rowlistTail) row focus where
-  monoidRecordImpl _
-    = unsafeInsert key
-        (mempty :: focus)
-        (monoidRecordImpl (RLProxy :: RLProxy rowlistTail))
+    => MonoidRow (RL.Cons key focus rowlistTail) subrow focus where
+  memptyRecordImpl _
+    = insert mempty tail
     where
       key = reflectSymbol (SProxy :: SProxy key)
+      insert = unsafeInsert key :: focus -> Record subrowTail -> Record subrow
+      tail = memptyRecordImpl (RLProxy :: RLProxy rowlistTail)
 
 instance monoidRecord
     :: ( RL.RowToList row list
-       , SemigroupRecord list row row focus
-       , MonoidRecord list row focus
+       , SemigroupRow list row row focus
+       , MonoidRow list row focus
        )
     => Monoid (Record row) where
-  mempty = monoidRecordImpl (RLProxy :: RLProxy list)
-
+  mempty = memptyRecordImpl (RLProxy :: RLProxy list)
 
 -- | Append a value to itself a certain number of times. For the
 -- | `Multiplicative` type, and for a non-negative power, this is the same as