blob: a5bbb9534cad14b495759e845dd19d39d378f9f5 (
plain)
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
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
|
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE UndecidableSuperClasses #-}
module T10592 where
import Data.Kind (Type)
import Prelude (Bool(True,False),Integer,Ordering)
import qualified Prelude
--------------------
-- class hierarchy
class Boolean (Logic a) => Eq a where
type Logic a :: Type
(==) :: a -> a -> Logic a
(/=) :: a -> a -> Logic a
a/=b = not (a==b)
class Eq a => POrd a where
inf :: a -> a -> a
class POrd a => MinBound a where
minBound :: a
class POrd a => Lattice a where
sup :: a -> a -> a
class (Lattice a, MinBound a) => Bounded a where
maxBound :: a
class Bounded a => Complemented a where
not :: a -> a
class Bounded a => Heyting a where
infixr 3 ==>
(==>) :: a -> a -> a
class (Complemented a, Heyting a) => Boolean a
(||) :: Boolean a => a -> a -> a
(||) = sup
(&&) :: Boolean a => a -> a -> a
(&&) = inf
--------------------
-- Bool instances
-- (these work fine)
instance Eq Bool where
type Logic Bool = Bool
(==) = (Prelude.==)
instance POrd Bool where
inf True True = True
inf _ _ = False
instance MinBound Bool where
minBound = False
instance Lattice Bool where
sup False False = False
sup _ _ = True
instance Bounded Bool where
maxBound = True
instance Complemented Bool where
not True = False
not False = True
instance Heyting Bool where
False ==> _ = True
True ==> a = a
instance Boolean Bool
--------------------
-- Integer instances
-- (these work fine)
instance Eq Integer where
type Logic Integer = Bool
(==) = (Prelude.==)
instance POrd Integer where
inf = Prelude.min
instance Lattice Integer where
sup = Prelude.max
--------------------
-- function instances
-- (these cause GHC to loop)
instance Eq b => Eq (a -> b) where
type Logic (a -> b) = a -> Logic b
f==g = \a -> f a == g a
instance POrd b => POrd (a -> b) where
inf f g = \a -> inf (f a) (g a)
instance MinBound b => MinBound (a -> b) where
minBound = \_ -> minBound
instance Lattice b => Lattice (a -> b) where
sup f g = \a -> sup (f a) (g a)
instance Bounded b => Bounded (a -> b) where
maxBound = \_ -> maxBound
instance Complemented b => Complemented (a -> b) where
not f = \a -> not (f a)
instance Heyting b => Heyting (a -> b) where
f ==> g = \a -> f a ==> g a
instance Boolean b => Boolean (a -> b)
|
