/
Quotient.purs
71 lines (51 loc) · 2.03 KB
/
Quotient.purs
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
-- | Approximation of quotient types.
module Type.Quotient
( class Canonical
, canonical
, Quotient
, type (/)
, mkQuotient
, runQuotient
, Id
, Abs
, Mod
) where
import Data.Ord (abs)
import Prelude
import Type.Nat1 (kind Nat1, class IsNat1, N1Proxy(..), reifyNat1)
import Type.Proxy (Proxy(..))
--------------------------------------------------------------------------------
-- | Equivalence relation disguised as a canonicalization function.
class Canonical a e | e -> a where
canonical :: Proxy e -> a -> a
--------------------------------------------------------------------------------
-- | Quotient type with equivalence relation `e`. The runtime representation is
-- | identical to that of `a`.
newtype Quotient a e = Quotient a
infixl 9 type Quotient as /
-- | Pair a value with an equivalence relation.
mkQuotient :: ∀ a e. a -> a / e
mkQuotient = Quotient
-- | Canonicalize a value using an equivalence relation such that the caller
-- | cannot observe distinct wrappees.
runQuotient :: ∀ a e. Canonical a e => a / e -> a
runQuotient (Quotient a) = canonical (Proxy :: Proxy e) a
instance eqQuotient :: (Eq a, Canonical a e) => Eq (a / e) where
eq a b = eq (runQuotient a) (runQuotient b)
instance ordQuotient :: (Ord a, Canonical a e) => Ord (a / e) where
compare a b = compare (runQuotient a) (runQuotient b)
instance showQuotient :: (Show a, Canonical a e) => Show (a / e) where
show a = "(mkQuotient " <> show a <> ")"
--------------------------------------------------------------------------------
-- | `T / Id ~ T`.
foreign import data Id :: Type
-- | Negative values are equivalent to their positive counterparts.
foreign import data Abs :: Type
-- | Integers modulo some positive number.
foreign import data Mod :: Nat1 -> Type
instance canonicalId :: Canonical a Id where
canonical _ = id
instance canonicalAbs :: (Ord a, Ring a) => Canonical a Abs where
canonical _ = abs
instance canonicalMod :: (IsNat1 n) => Canonical Int (Mod n) where
canonical _ a = a `mod` reifyNat1 (N1Proxy :: N1Proxy n)