1 {- -*- coding: utf-8 -*- -}
7 FunctionalDependencies,
14 module Data.HList.Prelude
53 import Types.Data.Bool
54 import Types.Data.Num hiding ((:*:))
63 deriving (Show, Eq, Ord, Read, Typeable)
73 deriving (Show, Eq, Ord, Read, Typeable)
75 instance List l => List (Cons e l)
77 hCons :: List l => e -> l -> Cons e l
84 class ExtendT e l where
86 (.&.) :: e -> l -> e :&: l
88 instance ExtendT e Nil where
89 type e :&: Nil = Cons e Nil
90 e .&. nil = hCons e nil
92 instance List l => ExtendT e (Cons e' l) where
93 type e :&: Cons e' l = Cons e (Cons e' l)
94 e .&. Cons e' l = hCons e (hCons e' l)
100 class AppendT l l' where
102 (.++.) :: l -> l' -> l :++: l'
104 instance List l => AppendT Nil l where
108 instance ( List (l :++: l')
110 ) => AppendT (Cons e l) l' where
111 type Cons e l :++: l' = Cons e (l :++: l')
112 (Cons e l) .++. l' = hCons e (l .++. l')
115 class ApplyT f a where
117 apply :: f -> a -> Apply f a
118 apply _ _ = undefined
121 class Apply2T f a b where
123 apply2 :: f -> a -> b -> Apply2 f a b
124 apply2 _ _ _ = undefined
129 instance ApplyT Id a where
134 data AppendA = AppendA
136 instance AppendT a b => Apply2T AppendA a b where
137 type Apply2 AppendA a b = a :++: b
138 apply2 _ a b = a .++. b
141 class FoldrT f v l where
143 hFoldr :: f -> v -> l -> Foldr f v l
145 instance FoldrT f v Nil where
146 type Foldr f v Nil = v
149 instance ( FoldrT f v l
150 , Apply2T f e (Foldr f v l)
151 ) => FoldrT f v (Cons e l) where
152 type Foldr f v (Cons e l) = Apply2 f e (Foldr f v l)
153 hFoldr f v (Cons e l) = apply2 f e (hFoldr f v l)
156 class ConcatT ls where
158 hConcat :: ls -> Concat ls
160 instance FoldrT AppendA Nil ls => ConcatT ls where
161 type Concat ls = Foldr AppendA Nil ls
162 hConcat ls = hFoldr AppendA hNil ls
167 hMap :: f -> l -> Map f l
169 instance MapT f Nil where
173 instance ( ApplyT f x
176 ) => MapT f (Cons x xs) where
177 type Map f (Cons x xs) = Cons (Apply f x) (Map f xs)
178 hMap f (Cons x xs) = hCons (apply f x) (hMap f xs)
182 type instance All f Nil = True
183 type instance All f (Cons x xs) = If (Apply f x) (All f xs) False
187 type instance Length Nil = D0
188 type instance Length (Cons e l) = Succ (Length l)
193 -- OccursMany (zero or more)
194 class OccursMany e l where
195 hOccursMany :: l -> [e]
197 instance OccursMany e Nil where
203 => OccursMany e (Cons e l)
205 hOccursMany (Cons e l) = e : hOccursMany l
210 => OccursMany e (Cons e' l)
212 hOccursMany (Cons _ l) = hOccursMany l
214 -- OccursMany1 (one or more)
215 class OccursMany1 e l where
216 hOccursMany1 :: l -> [e]
218 instance Fail (TypeNotFound e) => OccursMany1 e Nil where
219 hOccursMany1 _ = undefined
224 => OccursMany1 e (Cons e l)
226 hOccursMany1 (Cons e l) = e : hOccursMany l
231 => OccursMany1 e (Cons e' l)
233 hOccursMany1 (Cons _ l) = hOccursMany1 l
235 -- OccursOpt (zero or one)
236 class OccursOpt e l where
237 hOccursOpt :: l -> Maybe e
239 instance OccursOpt e Nil where
240 hOccursOpt _ = Nothing
242 instance OccursNot e l => OccursOpt e (Cons e l) where
243 hOccursOpt (Cons e _) = Just e
245 instance OccursOpt e l => OccursOpt e (Cons e' l) where
246 hOccursOpt (Cons _ l) = hOccursOpt l
249 class Occurs e l where
254 instance Fail (TypeNotFound e) => Occurs e Nil
261 => Occurs e (Cons e l)
263 hOccurs (Cons e _) = e
268 => Occurs e (Cons e' l)
270 hOccurs (Cons _ l) = hOccurs l
275 instance OccursNot e Nil
276 instance Fail (TypeFound e) => OccursNot e (Cons e l)
277 instance OccursNot e l => OccursNot e (Cons e' l)
281 instance NoDuplicates Nil
282 instance OccursNot e l => NoDuplicates (Cons e l)
286 "Strongly Typed Heterogeneous Collections"
291 ==========================
292 9 By chance or by design?
294 We will now discuss the issues surrounding the definition of type
295 equality, inequality, and unification — and give implementations
296 differing in simplicity, genericity, and portability.
298 We define the class TypeEq x y b for type equality. The class relates
299 two types x and y to the type HTrue in case the two types are equal;
300 otherwise, the types are related to HFalse. We should point out
301 however groundness issues. If TypeEq is to return HTrue, the types
302 must be ground; TypeEq can return HFalse even for unground types,
303 provided they are instantiated enough to determine that they are not
304 equal. So, TypeEq is total for ground types, and partial for unground
305 types. We also define the class TypeCast x y: a constraint that holds
306 only if the two types x and y are unifiable. Regarding groundness of x
307 and y, the class TypeCast is less restricted than TypeEq. That is,
308 TypeCast x y succeeds even for unground types x and y in case they can
309 be made equal through unification. TypeEq and TypeCast are related to
310 each other as fol- lows. Whenever TypeEq succeeds with HTrue, TypeCast
311 succeeds as well. Whenever TypeEq succeeds with HFalse, TypeCast
312 fails. But for unground types, when TypeCast succeeds, TypeEq might
313 fail. So the two complement each other for unground types. Also,
314 TypeEq is a partial predicate, while TypeCast is a relation. That’s
317 class TypeEq x y b | x y -> b
318 instance TypeEq x x True
319 instance TypeCast False b =>
322 class TypeCast a b | a -> b, b -> a
326 class TypeCast' t a b | t a -> b, t b -> a
328 typeCast' :: t -> a -> b
330 class TypeCast'' t a b | t a -> b, t b -> a
332 typeCast'' :: t -> a -> b
334 instance TypeCast' () a b => TypeCast a b
336 typeCast x = typeCast' () x
338 instance TypeCast'' t a b => TypeCast' t a b
340 typeCast' = typeCast''
342 instance TypeCast'' () a a