Data/HList/Prelude.hs

   1 {- -*- coding: utf-8 -*- -}
   2 {-# LANGUAGE
   3   DeriveDataTypeable,
   4   EmptyDataDecls,
   5   FlexibleContexts,
   6   FlexibleInstances,
   7   FunctionalDependencies,
   8   MultiParamTypeClasses,
   9   OverlappingInstances,
  10   TypeFamilies,
  11   TypeOperators,
  12   UndecidableInstances
  13   #-}
  14 module Data.HList.Prelude
  15     ( HList
  16
  17     , HNil(..)
  18     , hNil
  19
  20     , HCons(..)
  21     , hCons
  22
  23     , HExtendT(..)
  24     , HAppendT(..)
  25
  26     , ApplyT(..)
  27     , Apply2T(..)
  28
  29     , Id(..)
  30     , HAppendA(..)
  31
  32     , HFoldrT(..)
  33     , HConcatT(..)
  34     , HMapT(..)
  35
  36     , HAll
  37     , HLength
  38
  39     , Fail
  40     , TypeFound
  41     , TypeNotFound
  42     , HOccursMany(..)
  43     , HOccursMany1(..)
  44     , HOccursOpt(..)
  45     , HOccurs(..)
  46     , HOccursNot
  47
  48     , HNoDuplicates
  49     )
  50     where
  51
  52 import Data.Typeable
  53 import Types.Data.Bool
  54 import Types.Data.Num hiding ((:*:))
  55
  56
  57 -- HList
  58 class HList l
  59
  60 -- HNil
  61 data HNil
  62     = HNil
  63       deriving (Show, Eq, Ord, Read, Typeable)
  64
  65 instance HList HNil
  66
  67 hNil :: HNil
  68 hNil = HNil
  69
  70 -- HCons
  71 data HCons e l
  72     = HCons e l
  73       deriving (Show, Eq, Ord, Read, Typeable)
  74
  75 instance HList l => HList (HCons e l)
  76
  77 hCons :: HList l => e -> l -> HCons e l
  78 hCons = HCons
  79
  80 -- HExtendT
  81 infixr 2 :&:
  82 infixr 2 .&.
  83
  84 class HExtendT e l where
  85     type e :&: l
  86     (.&.) :: e -> l -> e :&: l
  87
  88 instance HExtendT e HNil where
  89     type e :&: HNil = HCons e HNil
  90     e .&. nil = hCons e nil
  91
  92 instance HList l => HExtendT e (HCons e' l) where
  93     type e :&: HCons e' l = HCons e (HCons e' l)
  94     e .&. HCons e' l = hCons e (hCons e' l)
  95
  96 -- HAppendT
  97 infixr 1 :++:
  98 infixr 1 .++.
  99
 100 class HAppendT l l' where
 101     type l :++: l'
 102     (.++.) :: l -> l' -> l :++: l'
 103
 104 instance HList l => HAppendT HNil l where
 105     type HNil :++: l = l
 106     _ .++. l = l
 107
 108 instance ( HList (l :++: l')
 109          , HAppendT l l'
 110          ) => HAppendT (HCons e l) l' where
 111     type HCons e l :++: l' = HCons e (l :++: l')
 112     (HCons e l) .++. l' = hCons e (l .++. l')
 113
 114 -- ApplyT
 115 class ApplyT f a where
 116     type Apply f a
 117     apply :: f -> a -> Apply f a
 118     apply _ _ = undefined
 119
 120 -- Apply2T
 121 class Apply2T f a b where
 122     type Apply2 f a b
 123     apply2 :: f -> a -> b -> Apply2 f a b
 124     apply2 _ _ _ = undefined
 125
 126 -- Id
 127 data Id = Id
 128
 129 instance ApplyT Id a where
 130     type Apply Id a = a
 131     apply _ a = a
 132
 133 -- HAppendA
 134 data HAppendA = HAppendA
 135
 136 instance HAppendT a b => Apply2T HAppendA a b where
 137     type Apply2 HAppendA a b = a :++: b
 138     apply2 _ a b = a .++. b
 139
 140 -- HFoldrT
 141 class HFoldrT f v l where
 142     type HFoldr f v l
 143     hFoldr :: f -> v -> l -> HFoldr f v l
 144
 145 instance HFoldrT f v HNil where
 146     type HFoldr f v HNil = v
 147     hFoldr _ v _ = v
 148
 149 instance ( HFoldrT f v l
 150          , Apply2T f e (HFoldr f v l)
 151          ) => HFoldrT f v (HCons e l) where
 152     type HFoldr f v (HCons e l) = Apply2 f e (HFoldr f v l)
 153     hFoldr f v (HCons e l) = apply2 f e (hFoldr f v l)
 154
 155 -- HConcatT
 156 class HConcatT ls where
 157     type HConcat ls
 158     hConcat :: ls -> HConcat ls
 159
 160 instance HFoldrT HAppendA HNil ls => HConcatT ls where
 161     type HConcat ls = HFoldr HAppendA HNil ls
 162     hConcat ls = hFoldr HAppendA hNil ls
 163
 164 -- HMapT
 165 class HMapT f l where
 166     type HMap f l
 167     hMap :: f -> l -> HMap f l
 168
 169 instance HMapT f HNil where
 170     type HMap f HNil = HNil
 171     hMap _ _ = hNil
 172
 173 instance ( ApplyT f x
 174          , HMapT f xs
 175          , HList (HMap f xs)
 176          ) => HMapT f (HCons x xs) where
 177     type HMap f (HCons x xs) = HCons (Apply f x) (HMap f xs)
 178     hMap f (HCons x xs) = hCons (apply f x) (hMap f xs)
 179
 180 -- HAll
 181 type family HAll f l
 182 type instance HAll f HNil         = True
 183 type instance HAll f (HCons x xs) = If (Apply f x) (HAll f xs) False
 184
 185 -- HLength
 186 type family HLength l
 187 type instance HLength HNil        = D0
 188 type instance HLength (HCons e l) = Succ (HLength l)
 189
 190 -- Fail
 191 class Fail a
 192
 193 -- HOccursMany (zero or more)
 194 class HOccursMany e l where
 195     hOccursMany :: l -> [e]
 196
 197 instance HOccursMany e HNil where
 198     hOccursMany _ = []
 199
 200 instance ( HList l
 201          , HOccursMany e l
 202          )
 203     => HOccursMany e (HCons e l)
 204     where
 205       hOccursMany (HCons e l) = e : hOccursMany l
 206
 207 instance ( HList l
 208          , HOccursMany e l
 209          )
 210     => HOccursMany e (HCons e' l)
 211     where
 212       hOccursMany (HCons _ l) = hOccursMany l
 213
 214 -- HOccursMany1 (one or more)
 215 class HOccursMany1 e l where
 216     hOccursMany1 :: l -> [e]
 217
 218 instance Fail (TypeNotFound e) => HOccursMany1 e HNil where
 219     hOccursMany1 _ = undefined
 220
 221 instance ( HList l
 222          , HOccursMany e l
 223          )
 224     => HOccursMany1 e (HCons e l)
 225     where
 226       hOccursMany1 (HCons e l) = e : hOccursMany l
 227
 228 instance ( HList l
 229          , HOccursMany1 e l
 230          )
 231     => HOccursMany1 e (HCons e' l)
 232     where
 233       hOccursMany1 (HCons _ l) = hOccursMany1 l
 234
 235 -- HOccursOpt (zero or one)
 236 class HOccursOpt e l where
 237     hOccursOpt :: l -> Maybe e
 238
 239 instance HOccursOpt e HNil where
 240     hOccursOpt _ = Nothing
 241
 242 instance HOccursNot e l => HOccursOpt e (HCons e l) where
 243     hOccursOpt (HCons e _) = Just e
 244
 245 instance HOccursOpt e l => HOccursOpt e (HCons e' l) where
 246     hOccursOpt (HCons _ l) = hOccursOpt l
 247
 248 -- HOccurs (one)
 249 class HOccurs e l where
 250     hOccurs :: l -> e
 251
 252 data TypeNotFound e
 253
 254 instance Fail (TypeNotFound e) => HOccurs e HNil
 255     where
 256       hOccurs = undefined
 257
 258 instance ( HList l
 259          , HOccursNot e l
 260          )
 261     => HOccurs e (HCons e l)
 262     where
 263       hOccurs (HCons e _) = e
 264
 265 instance ( HList l
 266          , HOccurs e l
 267          )
 268     => HOccurs e (HCons e' l)
 269     where
 270       hOccurs (HCons _ l) = hOccurs l
 271
 272 -- HOccursNot (zero)
 273 data     TypeFound e
 274 class    HOccursNot e l
 275 instance HOccursNot e HNil
 276 instance Fail (TypeFound e) => HOccursNot e (HCons e  l)
 277 instance HOccursNot e l     => HOccursNot e (HCons e' l)
 278
 279 -- HNoDuplicates
 280 class    HNoDuplicates l
 281 instance HNoDuplicates HNil
 282 instance HOccursNot e l => HNoDuplicates (HCons e l)
 283
 284 {-
 285 {-
 286 "Strongly Typed Heterogeneous Collections"
 287    — August 26, 2004
 288        Oleg Kiselyov
 289        Ralf Lämmel
 290        Keean Schupke
 291 ==========================
 292 9 By chance or by design?
 293
 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.
 297
 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
 315 why both are useful.
 316  -}
 317 class    TypeEq x y b | x y -> b
 318 instance TypeEq x x True
 319 instance TypeCast False b =>
 320          TypeEq x y b
 321
 322 class TypeCast a b | a -> b, b -> a
 323     where
 324       typeCast :: a -> b
 325
 326 class TypeCast' t a b | t a -> b, t b -> a
 327     where
 328       typeCast' :: t -> a -> b
 329
 330 class TypeCast'' t a b | t a -> b, t b -> a
 331     where
 332       typeCast'' :: t -> a -> b
 333
 334 instance TypeCast' () a b => TypeCast a b
 335     where
 336       typeCast x = typeCast' () x
 337
 338 instance TypeCast'' t a b => TypeCast' t a b
 339     where
 340       typeCast' = typeCast''
 341
 342 instance TypeCast'' () a a
 343     where
 344       typeCast'' _ x = x
 345 -}