Skip to content

Commit c524f9e

Browse files
garybgaryb
committed
Further work on record instances
1 parent 434a877 commit c524f9e

File tree

13 files changed

+295
-292
lines changed

13 files changed

+295
-292
lines changed

‎src/Data/BooleanAlgebra.purs‎

Lines changed: 18 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,13 @@
11
module Data.BooleanAlgebra
22
( class BooleanAlgebra
33
, module Data.HeytingAlgebra
4+
, class BooleanAlgebraRecord
45
) where
56

6-
import Data.HeytingAlgebra (class HeytingAlgebra, class HeytingAlgebraRow, ff, tt, implies, conj, disj, not, (&&), (||))
7+
import Data.HeytingAlgebra (class HeytingAlgebra, class HeytingAlgebraRecord, ff, tt, implies, conj, disj, not, (&&), (||))
8+
import Data.Symbol (class IsSymbol)
79
import Data.Unit (Unit)
10+
import Prim.Row as Row
811
import Prim.RowList as RL
912

1013
-- | The `BooleanAlgebra` type class represents types that behave like boolean
@@ -20,9 +23,18 @@ class HeytingAlgebra a <= BooleanAlgebra a
2023
instance booleanAlgebraBoolean :: BooleanAlgebra Boolean
2124
instance booleanAlgebraUnit :: BooleanAlgebra Unit
2225
instance booleanAlgebraFn :: BooleanAlgebra b => BooleanAlgebra (a -> b)
26+
instance booleanAlgebraRecord :: (RL.RowToList row list, BooleanAlgebraRecord list row row) => BooleanAlgebra (Record row)
2327

24-
instance booleanAlgebraRecord
25-
:: ( RL.RowToList row list
26-
, HeytingAlgebraRow list row row focus
27-
)
28-
=> BooleanAlgebra (Record row)
28+
-- | A class for records where all fields have `BooleanAlgebra` instances, used
29+
-- | to implement the `BooleanAlgebra` instance for records.
30+
class HeytingAlgebraRecord rowlist row subrow <= BooleanAlgebraRecord rowlist row subrow | rowlist -> subrow
31+
32+
instance booleanAlgebraRecordNil :: BooleanAlgebraRecord RL.Nil row ()
33+
34+
instance booleanAlgebraRecordCons
35+
:: ( IsSymbol key
36+
, Row.Cons key focus subrowTail subrow
37+
, BooleanAlgebraRecord rowlistTail row subrowTail
38+
, BooleanAlgebra focus
39+
)
40+
=> BooleanAlgebraRecord (RL.Cons key focus rowlistTail) row subrow

‎src/Data/CommutativeRing.purs‎

Lines changed: 19 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -2,11 +2,14 @@ module Data.CommutativeRing
22
( class CommutativeRing
33
, module Data.Ring
44
, module Data.Semiring
5+
, class CommutativeRingRecord
56
) where
67

7-
import Data.Ring (class Ring, class RingRow)
8-
import Data.Semiring (class Semiring, class SemiringRow, add, mul, one, zero, (*), (+))
8+
import Data.Ring (class Ring, class RingRecord)
9+
import Data.Semiring (class Semiring, add, mul, one, zero, (*), (+))
10+
import Data.Symbol (class IsSymbol)
911
import Data.Unit (Unit)
12+
import Prim.Row as Row
1013
import Prim.RowList as RL
1114

1215
-- | The `CommutativeRing` class is for rings where multiplication is
@@ -22,10 +25,18 @@ instance commutativeRingInt :: CommutativeRing Int
2225
instance commutativeRingNumber :: CommutativeRing Number
2326
instance commutativeRingUnit :: CommutativeRing Unit
2427
instance commutativeRingFn :: CommutativeRing b => CommutativeRing (a -> b)
28+
instance commutativeRingRecord :: (RL.RowToList row list, CommutativeRingRecord list row row) => CommutativeRing (Record row)
2529

26-
instance commutativeRingRecord
27-
:: ( RL.RowToList row list
28-
, SemiringRow list row row focus
29-
, RingRow list row row focus
30-
)
31-
=> CommutativeRing (Record row)
30+
-- | A class for records where all fields have `CommutativeRing` instances, used
31+
-- | to implement the `CommutativeRing` instance for records.
32+
class RingRecord rowlist row subrow <= CommutativeRingRecord rowlist row subrow | rowlist -> subrow
33+
34+
instance commutativeRingRecordNil :: CommutativeRingRecord RL.Nil row ()
35+
36+
instance commutativeRingRecordCons
37+
:: ( IsSymbol key
38+
, Row.Cons key focus subrowTail subrow
39+
, CommutativeRingRecord rowlistTail row subrowTail
40+
, CommutativeRing focus
41+
)
42+
=> CommutativeRingRecord (RL.Cons key focus rowlistTail) row subrow

‎src/Data/Eq.purs‎

Lines changed: 16 additions & 21 deletions
Original file line numberDiff line numberDiff line change
@@ -1,19 +1,17 @@
11
module Data.Eq
22
( class Eq, eq, (==), notEq, (/=)
33
, class Eq1, eq1, notEq1
4-
5-
, class EqRow
6-
, eqRecordImpl
4+
, class EqRecord, eqRecord
75
) where
86

97
import Data.HeytingAlgebra ((&&))
10-
import Data.Internal.Record (unsafeGet)
11-
import Type.Data.RowList (RLProxy(..))
128
import Data.Symbol (class IsSymbol, SProxy(..), reflectSymbol)
139
import Data.Unit (Unit)
1410
import Data.Void (Void)
1511
import Prim.Row as Row
1612
import Prim.RowList as RL
13+
import Record.Unsafe (unsafeGet)
14+
import Type.Data.RowList (RLProxy(..))
1715

1816
-- | The `Eq` type class represents types which support decidable equality.
1917
-- |
@@ -63,6 +61,9 @@ instance eqVoid :: Eq Void where
6361
instance eqArray :: Eq a => Eq (Array a) where
6462
eq = eqArrayImpl eq
6563

64+
instance eqRec :: (RL.RowToList row list, EqRecord list row) => Eq (Record row) where
65+
eq = eqRecord (RLProxy :: RLProxy list)
66+
6667
foreign import refEq :: forall a. a -> a -> Boolean
6768
foreign import eqArrayImpl :: forall a. (a -> a -> Boolean) -> Array a -> Array a -> Boolean
6869

@@ -76,29 +77,23 @@ instance eq1Array :: Eq1 Array where
7677
notEq1 :: forall f a. Eq1 f => Eq a => f a -> f a -> Boolean
7778
notEq1 x y = (x `eq1` y) == false
7879

79-
-- | A typeclass to characterise rows of types that are all Eq..
80-
class EqRow rowlist row focus | rowlist -> focus where
81-
eqRecordImpl :: RLProxy rowlist -> Record row -> Record row -> Boolean
80+
-- | A class for records where all fields have `Eq` instances, used to implement
81+
-- | the `Eq` instance for records.
82+
class EqRecord rowlist row where
83+
eqRecord :: RLProxy rowlist -> Record row -> Record row -> Boolean
8284

83-
instance eqRowNil :: EqRow RL.Nil row focus where
84-
eqRecordImpl _ _ _ = true
85+
instance eqRowNil :: EqRecord RL.Nil row where
86+
eqRecord _ _ _ = true
8587

8688
instance eqRowCons
87-
:: ( EqRow rowlistTail row subfocus
89+
:: ( EqRecord rowlistTail row
8890
, Row.Cons key focus rowTail row
8991
, IsSymbol key
9092
, Eq focus
9193
)
92-
=> EqRow (RL.Cons key focus rowlistTail) row focus where
93-
eqRecordImpl _ ra rb = (get ra == get rb) && tail
94+
=> EqRecord (RL.Cons key focus rowlistTail) row where
95+
eqRecord _ ra rb = (get ra == get rb) && tail
9496
where
9597
key = reflectSymbol (SProxy :: SProxy key)
9698
get = unsafeGet key :: Record row -> focus
97-
tail = eqRecordImpl (RLProxy :: RLProxy rowlistTail) ra rb
98-
99-
instance eqRecord
100-
:: ( RL.RowToList row list
101-
, EqRow list row focus
102-
)
103-
=> Eq (Record row) where
104-
eq = eqRecordImpl (RLProxy :: RLProxy list)
99+
tail = eqRecord (RLProxy :: RLProxy rowlistTail) ra rb

‎src/Data/HeytingAlgebra.purs‎

Lines changed: 50 additions & 68 deletions
Original file line numberDiff line numberDiff line change
@@ -1,29 +1,13 @@
11
module Data.HeytingAlgebra
2-
( class HeytingAlgebra
3-
4-
, tt
5-
, ff
6-
, implies
7-
, conj
8-
, disj
9-
, not
10-
, (&&)
11-
, (||)
12-
13-
, class HeytingAlgebraRow
14-
, ffRecordImpl
15-
, ttRecordImpl
16-
, impliesRecordImpl
17-
, conjRecordImpl
18-
, disjRecordImpl
19-
, notRecordImpl
2+
( class HeytingAlgebra, tt, ff, implies, conj, disj, not, (&&), (||)
3+
, class HeytingAlgebraRecord, ffRecord, ttRecord, impliesRecord, conjRecord, disjRecord, notRecord
204
) where
215

22-
import Data.Internal.Record (unsafeGet, unsafeInsert)
236
import Data.Symbol (class IsSymbol, SProxy(..), reflectSymbol)
247
import Data.Unit (Unit, unit)
258
import Prim.Row as Row
269
import Prim.RowList as RL
10+
import Record.Unsafe (unsafeGet, unsafeSet)
2711
import Type.Data.Row (RProxy(..))
2812
import Type.Data.RowList (RLProxy(..))
2913

@@ -87,82 +71,80 @@ instance heytingAlgebraFunction :: HeytingAlgebra b => HeytingAlgebra (a -> b) w
8771
disj f g a = f a || g a
8872
not f a = not (f a)
8973

74+
instance heytingAlgebraRecord :: (RL.RowToList row list, HeytingAlgebraRecord list row row) => HeytingAlgebra (Record row) where
75+
ff = ffRecord (RLProxy :: RLProxy list) (RProxy :: RProxy row)
76+
tt = ttRecord (RLProxy :: RLProxy list) (RProxy :: RProxy row)
77+
conj = conjRecord (RLProxy :: RLProxy list)
78+
disj = disjRecord (RLProxy :: RLProxy list)
79+
implies = impliesRecord (RLProxy :: RLProxy list)
80+
not = notRecord (RLProxy :: RLProxy list)
81+
9082
foreign import boolConj :: Boolean -> Boolean -> Boolean
9183
foreign import boolDisj :: Boolean -> Boolean -> Boolean
9284
foreign import boolNot :: Boolean -> Boolean
9385

94-
class HeytingAlgebraRow rowlist row subrow focus | rowlist -> subrow focus where
95-
ffRecordImpl :: RLProxy rowlist -> RProxy row -> Record subrow
96-
ttRecordImpl :: RLProxy rowlist -> RProxy row -> Record subrow
97-
impliesRecordImpl :: RLProxy rowlist -> Record row -> Record row -> Record subrow
98-
disjRecordImpl :: RLProxy rowlist -> Record row -> Record row -> Record subrow
99-
conjRecordImpl :: RLProxy rowlist -> Record row -> Record row -> Record subrow
100-
notRecordImpl :: RLProxy rowlist -> Record row -> Record subrow
101-
102-
instance heytingAlgebraRowNil :: HeytingAlgebraRow RL.Nil row () focus where
103-
conjRecordImpl _ _ _ = {}
104-
disjRecordImpl _ _ _ = {}
105-
ffRecordImpl _ _ = {}
106-
impliesRecordImpl _ _ _ = {}
107-
notRecordImpl _ _ = {}
108-
ttRecordImpl _ _ = {}
109-
110-
instance heytingAlgebraRowCons
86+
-- | A class for records where all fields have `HeytingAlgebra` instances, used
87+
-- | to implement the `HeytingAlgebra` instance for records.
88+
class HeytingAlgebraRecord rowlist row subrow | rowlist -> subrow where
89+
ffRecord :: RLProxy rowlist -> RProxy row -> Record subrow
90+
ttRecord :: RLProxy rowlist -> RProxy row -> Record subrow
91+
impliesRecord :: RLProxy rowlist -> Record row -> Record row -> Record subrow
92+
disjRecord :: RLProxy rowlist -> Record row -> Record row -> Record subrow
93+
conjRecord :: RLProxy rowlist -> Record row -> Record row -> Record subrow
94+
notRecord :: RLProxy rowlist -> Record row -> Record subrow
95+
96+
instance heytingAlgebraRecordNil :: HeytingAlgebraRecord RL.Nil row () where
97+
conjRecord _ _ _ = {}
98+
disjRecord _ _ _ = {}
99+
ffRecord _ _ = {}
100+
impliesRecord _ _ _ = {}
101+
notRecord _ _ = {}
102+
ttRecord _ _ = {}
103+
104+
instance heytingAlgebraRecordCons
111105
:: ( IsSymbol key
112106
, Row.Cons key focus subrowTail subrow
113-
, HeytingAlgebraRow rowlistTail row subrowTail subfocus
107+
, HeytingAlgebraRecord rowlistTail row subrowTail
114108
, HeytingAlgebra focus
115109
)
116-
=> HeytingAlgebraRow (RL.Cons key focus rowlistTail) row subrow focus where
117-
conjRecordImpl _ ra rb = insert (conj (get ra) (get rb)) tail
110+
=> HeytingAlgebraRecord (RL.Cons key focus rowlistTail) row subrow where
111+
conjRecord _ ra rb = insert (conj (get ra) (get rb)) tail
118112
where
119113
key = reflectSymbol (SProxy :: SProxy key)
120114
get = unsafeGet key :: Record row -> focus
121-
insert = unsafeInsert key :: focus -> Record subrowTail -> Record subrow
122-
tail = conjRecordImpl (RLProxy :: RLProxy rowlistTail) ra rb
115+
insert = unsafeSet key :: focus -> Record subrowTail -> Record subrow
116+
tail = conjRecord (RLProxy :: RLProxy rowlistTail) ra rb
123117

124-
disjRecordImpl _ ra rb = insert (disj (get ra) (get rb)) tail
118+
disjRecord _ ra rb = insert (disj (get ra) (get rb)) tail
125119
where
126120
key = reflectSymbol (SProxy :: SProxy key)
127121
get = unsafeGet key :: Record row -> focus
128-
insert = unsafeInsert key :: focus -> Record subrowTail -> Record subrow
129-
tail = disjRecordImpl (RLProxy :: RLProxy rowlistTail) ra rb
122+
insert = unsafeSet key :: focus -> Record subrowTail -> Record subrow
123+
tail = disjRecord (RLProxy :: RLProxy rowlistTail) ra rb
130124

131-
impliesRecordImpl _ ra rb = insert (implies (get ra) (get rb)) tail
125+
impliesRecord _ ra rb = insert (implies (get ra) (get rb)) tail
132126
where
133127
key = reflectSymbol (SProxy :: SProxy key)
134128
get = unsafeGet key :: Record row -> focus
135-
insert = unsafeInsert key :: focus -> Record subrowTail -> Record subrow
136-
tail = impliesRecordImpl (RLProxy :: RLProxy rowlistTail) ra rb
129+
insert = unsafeSet key :: focus -> Record subrowTail -> Record subrow
130+
tail = impliesRecord (RLProxy :: RLProxy rowlistTail) ra rb
137131

138-
ffRecordImpl _ row = insert ff tail
132+
ffRecord _ row = insert ff tail
139133
where
140134
key = reflectSymbol (SProxy :: SProxy key)
141-
insert = unsafeInsert key :: focus -> Record subrowTail -> Record subrow
142-
tail = ffRecordImpl (RLProxy :: RLProxy rowlistTail) row
135+
insert = unsafeSet key :: focus -> Record subrowTail -> Record subrow
136+
tail = ffRecord (RLProxy :: RLProxy rowlistTail) row
143137

144-
notRecordImpl _ row
138+
notRecord _ row
145139
= insert (not (get row)) tail
146140
where
147141
key = reflectSymbol (SProxy :: SProxy key)
148142
get = unsafeGet key :: Record row -> focus
149-
insert = unsafeInsert key :: focus -> Record subrowTail -> Record subrow
150-
tail = notRecordImpl (RLProxy :: RLProxy rowlistTail) row
143+
insert = unsafeSet key :: focus -> Record subrowTail -> Record subrow
144+
tail = notRecord (RLProxy :: RLProxy rowlistTail) row
151145

152-
ttRecordImpl _ row = insert tt tail
146+
ttRecord _ row = insert tt tail
153147
where
154148
key = reflectSymbol (SProxy :: SProxy key)
155-
insert = unsafeInsert key :: focus -> Record subrowTail -> Record subrow
156-
tail = ttRecordImpl (RLProxy :: RLProxy rowlistTail) row
157-
158-
instance heytingAlgebraRecord
159-
:: ( RL.RowToList row list
160-
, HeytingAlgebraRow list row row focus
161-
)
162-
=> HeytingAlgebra (Record row) where
163-
ff = ffRecordImpl (RLProxy :: RLProxy list) (RProxy :: RProxy row)
164-
tt = ttRecordImpl (RLProxy :: RLProxy list) (RProxy :: RProxy row)
165-
conj = conjRecordImpl (RLProxy :: RLProxy list)
166-
disj = disjRecordImpl (RLProxy :: RLProxy list)
167-
implies = impliesRecordImpl (RLProxy :: RLProxy list)
168-
not = notRecordImpl (RLProxy :: RLProxy list)
149+
insert = unsafeSet key :: focus -> Record subrowTail -> Record subrow
150+
tail = ttRecord (RLProxy :: RLProxy rowlistTail) row

‎src/Data/Internal/Record.js‎

Lines changed: 0 additions & 14 deletions
This file was deleted.

‎src/Data/Internal/Record.purs‎

Lines changed: 0 additions & 14 deletions
This file was deleted.

0 commit comments

Comments
 (0)