Skip to content

Commit 1c6a562

Browse files
author
Tom Harding
committed
BooleanAlgebra, Bounded, CommutativeRing, HeytingAlgebra, Ring
SO MANY INSTANCES
1 parent 4e192c8 commit 1c6a562

File tree

5 files changed

+166
-5
lines changed

5 files changed

+166
-5
lines changed

‎src/Data/BooleanAlgebra.purs‎

Lines changed: 8 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,8 +3,9 @@ module Data.BooleanAlgebra
33
, module Data.HeytingAlgebra
44
) where
55

6-
import Data.HeytingAlgebra (class HeytingAlgebra, ff, tt, implies, conj, disj, not, (&&), (||))
6+
import Data.HeytingAlgebra (class HeytingAlgebra, class HeytingAlgebraRecord, ff, tt, implies, conj, disj, not, (&&), (||))
77
import Data.Unit (Unit)
8+
import Prim.RowList as RL
89

910
-- | The `BooleanAlgebra` type class represents types that behave like boolean
1011
-- | values.
@@ -19,3 +20,9 @@ class HeytingAlgebra a <= BooleanAlgebra a
1920
instance booleanAlgebraBoolean :: BooleanAlgebra Boolean
2021
instance booleanAlgebraUnit :: BooleanAlgebra Unit
2122
instance booleanAlgebraFn :: BooleanAlgebra b => BooleanAlgebra (a -> b)
23+
24+
instance booleanAlgebraRecord
25+
:: ( RL.RowToList row list
26+
, HeytingAlgebraRecord list row row focus
27+
)
28+
=> BooleanAlgebra (Record row)

‎src/Data/Bounded.purs‎

Lines changed: 37 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -51,3 +51,40 @@ foreign import bottomNumber :: Number
5151
instance boundedNumber :: Bounded Number where
5252
top = topNumber
5353
bottom = bottomNumber
54+
55+
-- Similarly to the `OrdRecord` constraint, this implementation is potentially
56+
-- unstable. However, it is left here as a reference:
57+
58+
--class BoundedRecord rowlist row subrow focus | rowlist -> subrow focus where
59+
-- bottomRecordImpl :: RLProxy rowlist -> RProxy row -> Record subrow
60+
-- topRecordImpl :: RLProxy rowlist -> RProxy row -> Record subrow
61+
--
62+
--instance boundedRecordNil :: BoundedRecord RL.Nil row () focus where
63+
-- bottomRecordImpl _ _ = {}
64+
-- topRecordImpl _ _ = {}
65+
--
66+
--instance boundedRecordCons
67+
-- :: ( BoundedRecord rowlistTail row subrowTail subfocus
68+
-- , Row.Cons key focus subrowTail subrow
69+
-- , IsSymbol key
70+
-- , Bounded focus
71+
-- )
72+
-- => BoundedRecord (Row.Cons key focus rowlistTail) row subrow focus where
73+
-- bottomRecordImpl _ row
74+
-- = unsafeInsert key (bottom :: focus)
75+
-- (bottomRecordImpl (RLProxy :: RLProxy rowlistTail) row)
76+
-- where key = reflectSymbol (SProxy :: SProxy key)
77+
--
78+
-- topRecordImpl _ row
79+
-- = unsafeInsert key (bottom :: focus)
80+
-- (topRecordImpl (RLProxy :: RLProxy rowlistTail) row)
81+
-- where key = reflectSymbol (SProxy :: SProxy key)
82+
--
83+
--instance boundedRecord
84+
-- :: ( RL.RowToList row list
85+
-- , BoundedRecord list row row focus
86+
-- , OrdRecord list row row focus
87+
-- )
88+
-- => Bounded (Record row) where
89+
-- bottom = bottomRecordImpl (RLProxy :: RLProxy list) (RProxy :: RProxy row)
90+
-- top = topRecordImpl (RLProxy :: RLProxy list) (RProxy :: RProxy row)

‎src/Data/CommutativeRing.purs‎

Lines changed: 10 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -4,9 +4,10 @@ module Data.CommutativeRing
44
, module Data.Semiring
55
) where
66

7-
import Data.Ring (class Ring)
8-
import Data.Semiring (class Semiring, add, mul, one, zero, (*), (+))
7+
import Data.Ring (class Ring, class RingRecord)
8+
import Data.Semiring (class Semiring, class SemiringRecord, add, mul, one, zero, (*), (+))
99
import Data.Unit (Unit)
10+
import Prim.RowList as RL
1011

1112
-- | The `CommutativeRing` class is for rings where multiplication is
1213
-- | commutative.
@@ -21,3 +22,10 @@ instance commutativeRingInt :: CommutativeRing Int
2122
instance commutativeRingNumber :: CommutativeRing Number
2223
instance commutativeRingUnit :: CommutativeRing Unit
2324
instance commutativeRingFn :: CommutativeRing b => CommutativeRing (a -> b)
25+
26+
instance commutativeRingRecord
27+
:: ( RL.RowToList row list
28+
, SemiringRecord list row row focus
29+
, RingRecord list row row focus
30+
)
31+
=> CommutativeRing (Record row)

‎src/Data/HeytingAlgebra.purs‎

Lines changed: 108 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,31 @@
11
module Data.HeytingAlgebra
2-
( class HeytingAlgebra, tt, ff, implies, conj, disj, not
3-
, (&&), (||)
2+
( class HeytingAlgebra
3+
4+
, tt
5+
, ff
6+
, implies
7+
, conj
8+
, disj
9+
, not
10+
, (&&)
11+
, (||)
12+
13+
, class HeytingAlgebraRecord
14+
, ffRecordImpl
15+
, ttRecordImpl
16+
, impliesRecordImpl
17+
, conjRecordImpl
18+
, disjRecordImpl
19+
, notRecordImpl
420
) where
521

22+
import Data.Internal.Record (unsafeGet, unsafeInsert)
23+
import Data.RowList (RLProxy(..))
24+
import Data.Symbol (class IsSymbol, SProxy(..), reflectSymbol)
625
import Data.Unit (Unit, unit)
26+
import Prim.Row as Row
27+
import Prim.RowList as RL
28+
import Type.Data.Row (RProxy(..))
729

830
-- | The `HeytingAlgebra` type class represents types that are bounded lattices with
931
-- | an implication operator such that the following laws hold:
@@ -68,3 +90,87 @@ instance heytingAlgebraFunction :: HeytingAlgebra b => HeytingAlgebra (a -> b) w
6890
foreign import boolConj :: Boolean -> Boolean -> Boolean
6991
foreign import boolDisj :: Boolean -> Boolean -> Boolean
7092
foreign import boolNot :: Boolean -> Boolean
93+
94+
class HeytingAlgebraRecord 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 heytingAlgebraRecordNil :: HeytingAlgebraRecord RL.Nil row () focus where
103+
conjRecordImpl _ _ _ = {}
104+
disjRecordImpl _ _ _ = {}
105+
ffRecordImpl _ _ = {}
106+
impliesRecordImpl _ _ _ = {}
107+
notRecordImpl _ _ = {}
108+
ttRecordImpl _ _ = {}
109+
110+
instance heytingAlgebraRecordCons
111+
:: ( IsSymbol key
112+
, Row.Cons key focus subrowTail subrow
113+
, HeytingAlgebraRecord rowlistTail row subrowTail subfocus
114+
, HeytingAlgebra focus
115+
)
116+
=> HeytingAlgebraRecord (RL.Cons key focus rowlistTail) row subrow focus where
117+
conjRecordImpl _ ra rb
118+
= unsafeInsert key
119+
(conj (unsafeGet' key ra) (unsafeGet' key rb))
120+
(conjRecordImpl (RLProxy :: RLProxy rowlistTail) ra rb)
121+
where key = reflectSymbol (SProxy :: SProxy key)
122+
unsafeGet' = unsafeGet :: String -> Record row -> focus
123+
124+
disjRecordImpl _ ra rb
125+
= unsafeInsert key
126+
(disj (unsafeGet' key ra) (unsafeGet' key rb))
127+
(disjRecordImpl (RLProxy :: RLProxy rowlistTail) ra rb)
128+
where key = reflectSymbol (SProxy :: SProxy key)
129+
unsafeGet' = unsafeGet :: String -> Record row -> focus
130+
131+
impliesRecordImpl _ ra rb
132+
= unsafeInsert key
133+
(implies (unsafeGet' key ra) (unsafeGet' key rb))
134+
(impliesRecordImpl (RLProxy :: RLProxy rowlistTail) ra rb)
135+
where
136+
key = reflectSymbol (SProxy :: SProxy key)
137+
unsafeGet' = unsafeGet :: String -> Record row -> focus
138+
139+
ffRecordImpl _ _
140+
= unsafeInsert key (ff :: focus)
141+
( ffRecordImpl
142+
(RLProxy :: RLProxy rowlistTail)
143+
(RProxy :: RProxy row)
144+
)
145+
where
146+
key = reflectSymbol (SProxy :: SProxy key)
147+
unsafeGet' = unsafeGet :: String -> Record row -> focus
148+
149+
notRecordImpl _ row
150+
= unsafeInsert key (not (unsafeGet' key row))
151+
(notRecordImpl (RLProxy :: RLProxy rowlistTail) row)
152+
where
153+
key = reflectSymbol (SProxy :: SProxy key)
154+
unsafeGet' = unsafeGet :: String -> Record row -> focus
155+
156+
ttRecordImpl _ _
157+
= unsafeInsert key (tt :: focus)
158+
( ttRecordImpl
159+
(RLProxy :: RLProxy rowlistTail)
160+
(RProxy :: RProxy row)
161+
)
162+
where
163+
key = reflectSymbol (SProxy :: SProxy key)
164+
unsafeGet' = unsafeGet :: String -> Record row -> focus
165+
166+
instance heytingAlgebraRecord
167+
:: ( RL.RowToList row list
168+
, HeytingAlgebraRecord list row row focus
169+
)
170+
=> HeytingAlgebra (Record row) where
171+
ff = ffRecordImpl (RLProxy :: RLProxy list) (RProxy :: RProxy row)
172+
tt = ttRecordImpl (RLProxy :: RLProxy list) (RProxy :: RProxy row)
173+
conj = conjRecordImpl (RLProxy :: RLProxy list)
174+
disj = conjRecordImpl (RLProxy :: RLProxy list)
175+
implies = conjRecordImpl (RLProxy :: RLProxy list)
176+
not = notRecordImpl (RLProxy :: RLProxy list)

‎src/Data/Ring.purs‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,9 @@
11
module Data.Ring
22
( class Ring, sub, negate, (-)
33
, module Data.Semiring
4+
5+
, class RingRecord
6+
, subRecordImpl
47
) where
58

69
import Data.Internal.Record (unsafeGet, unsafeInsert)

0 commit comments

Comments
 (0)