never executed always true always false
1 {-# LANGUAGE ConstraintKinds #-}
2 {-# LANGUAGE DeriveFunctor #-}
3 {-# LANGUAGE MultiParamTypeClasses #-}
4 {-# LANGUAGE UndecidableInstances #-}
5
6 {-# OPTIONS_GHC -fno-warn-redundant-constraints #-}
7
8 module OpenCV.TypeLevel
9 ( -- * Kinds and types
10 DS(D, S), dsToMaybe
11 , Z(Z)
12 , (:::)((:::))
13
14 -- * Type level to value level conversions
15 , ToInt32(toInt32)
16 , ToNatDS(toNatDS)
17 , ToNatListDS(toNatListDS)
18
19 -- * Type functions
20 , Length
21 , Elem
22 , Relax
23
24 -- ** Predicates (constraints)
25 , In
26 , MayRelax
27 , All
28 , IsStatic
29
30 -- ** Type conversions
31 , DSNat
32 , DSNats
33 ) where
34
35 import "base" Data.Int
36 import "base" Data.Proxy
37 import "base" Data.Type.Bool
38 import "base" GHC.Exts ( Constraint )
39 import "base" GHC.TypeLits
40
41 --------------------------------------------------------------------------------
42 -- Kinds and types
43 --------------------------------------------------------------------------------
44
45 -- | 'D'ynamically or 'S'tatically known values
46 --
47 -- Mainly used as a promoted type.
48 --
49 -- Operationally exactly the 'Maybe' type
50 data DS a
51 = D -- ^ Something is dynamically known
52 | S a -- ^ Something is statically known, in particular: @a@
53 deriving (Show, Eq, Functor)
54
55 -- | Converts a DS value to the corresponding Maybe value
56 dsToMaybe :: DS a -> Maybe a
57 dsToMaybe D = Nothing
58 dsToMaybe (S a) = Just a
59
60 -- | End of list
61 data Z = Z
62
63 -- | Heterogeneous lists
64 --
65 -- Implemented as nested 2-tuples.
66 --
67 -- > f :: Int ::: Bool ::: Char ::: Z
68 -- > f = 3 ::: False ::: 'X' ::: Z
69 data a ::: b = a ::: b
70
71 infixr 5 :::
72
73
74 --------------------------------------------------------------------------------
75 -- Type level to value level conversions
76 --------------------------------------------------------------------------------
77
78 class ToInt32 a where
79 toInt32 :: a -> Int32
80
81 -- | value level: identity
82 instance ToInt32 Int32 where
83 toInt32 = id
84
85 -- | type level: reify the known natural number @n@
86 instance (KnownNat n) => ToInt32 (proxy n) where
87 toInt32 = fromInteger . natVal
88
89 --------------------------------------------------------------------------------
90
91 -- | Type level to value level conversion of numbers that are either
92 -- 'D'ynamically or 'S'tatically known.
93 --
94 -- > toNatDS (Proxy ('S 42)) == S 42
95 -- > toNatDS (Proxy 'D) == D
96 class ToNatDS a where
97 toNatDS :: a -> DS Int32
98
99 -- | value level numbers are dynamically known
100 instance ToNatDS (proxy 'D) where
101 toNatDS _proxy = D
102
103 -- | type level numbers are statically known
104 instance (ToInt32 (Proxy n)) => ToNatDS (Proxy ('S n)) where
105 toNatDS _proxy = S $ toInt32 (Proxy :: Proxy n)
106
107 --------------------------------------------------------------------------------
108
109 class ToNatListDS a where
110 toNatListDS :: a -> [DS Int32]
111
112 instance ToNatListDS (proxy '[]) where
113 toNatListDS _proxy = []
114
115 instance (ToNatDS (Proxy a), ToNatListDS (Proxy as))
116 => ToNatListDS (Proxy (a ': as)) where
117 toNatListDS _proxy = (toNatDS (Proxy :: Proxy a ))
118 : (toNatListDS (Proxy :: Proxy as))
119
120 --------------------------------------------------------------------------------
121 -- Type functions
122 --------------------------------------------------------------------------------
123
124 type family Length (xs :: [a]) :: Nat where
125 Length '[] = 0
126 Length (_x ': xs) = 1 + Length xs
127
128 type family Elem (e :: a) (xs :: [a]) :: Bool where
129 Elem _e '[] = 'False
130 Elem e (e ': _xs) = 'True
131 Elem e (_x ': xs) = Elem e xs
132
133 type In e xs = Elem e xs ~ 'True
134
135 type family DSNat (a :: ka) :: DS Nat where
136 DSNat Integer = 'D
137 DSNat Int32 = 'D
138 DSNat (Proxy n) = 'S n
139 DSNat (n :: Nat) = 'S n
140
141 type family DSNats (a :: ka) :: [DS Nat] where
142 DSNats Z = '[]
143 DSNats (x ::: xs) = DSNat x ': DSNats xs
144
145 DSNats ('[] :: [Nat]) = '[]
146 DSNats (x ': xs) = DSNat x ': DSNats xs
147
148 type family Relax (a :: DS ka) (b :: DS kb) :: Bool where
149 Relax x 'D = 'True
150 Relax ('S (x ': xs)) ('S (y ': ys)) = Relax x y && Relax ('S xs) ('S ys)
151 Relax ('S x) ('S y) = Relax x y
152 Relax x x = 'True
153 Relax x y = 'False
154
155 type MayRelax a b = Relax a b ~ 'True
156
157 -- type family LeDS_F (a :: Nat) (b :: DS Nat) :: Bool where
158 -- LeDS_F _a 'D = 'True
159 -- LeDS_F a ('S b) = a <=? b
160
161 -- type (.<=?) a b = LeDS_F a b ~ 'True
162
163 -- type LE a b = a <=? b ~ True
164 -- type GT a b = b <=? a ~ True
165
166
167 -- type family LengthDS (as :: DS [k]) :: DS Nat where
168 -- LengthDS 'D = 'D
169 -- LengthDS ('S xs) = 'S (Length xs)
170
171 -- type family MinLengthDS_F (a :: Nat) (bs :: DS [k]) :: Bool where
172 -- MinLengthDS_F _a 'D = 'True
173 -- MinLengthDS_F a bs = LeDS_F a (LengthDS bs)
174
175 -- type MinLengthDS a bs = MinLengthDS_F a bs ~ 'True
176
177 class PrivateIsStatic (ds :: DS a)
178 instance PrivateIsStatic ('S a)
179
180 class All (p :: k -> Constraint) (xs :: [k])
181 instance All p '[]
182 instance (p x, All p xs) => All p (x ': xs)
183
184 class (PrivateIsStatic ds) => IsStatic (ds :: DS a)
185 instance IsStatic ('S a)