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     ( List
  16
  17     , Nil(..)
  18     , hNil
  19
  20     , Cons(..)
  21     , hCons
  22
  23     , ExtendT(..)
  24     , AppendT(..)
  25
  26     , ApplyT(..)
  27     , Apply2T(..)
  28
  29     , Id(..)
  30     , AppendA(..)
  31
  32     , FoldrT(..)
  33     , ConcatT(..)
  34     , MapT(..)
  35
  36     , All
  37     , Length
  38
  39     , Fail
  40     , TypeFound
  41     , TypeNotFound
  42     , OccursMany(..)
  43     , OccursMany1(..)
  44     , OccursOpt(..)
  45     , Occurs(..)
  46     , OccursNot
  47
  48     , NoDuplicates
  49     )
  50     where
  51
  52 import Data.Typeable
  53 import Types.Data.Bool
  54 import Types.Data.Num hiding ((:*:))
  55
  56
  57 -- List
  58 class List l
  59
  60 -- Nil
  61 data Nil
  62     = Nil
  63       deriving (Show, Eq, Ord, Read, Typeable)
  64
  65 instance List Nil
  66
  67 hNil :: Nil
  68 hNil = Nil
  69
  70 -- Cons
  71 data Cons e l
  72     = Cons e l
  73       deriving (Show, Eq, Ord, Read, Typeable)
  74
  75 instance List l => List (Cons e l)
  76
  77 hCons :: List l => e -> l -> Cons e l
  78 hCons = Cons
  79
  80 -- ExtendT
  81 infixr 2 :&:
  82 infixr 2 .&.
  83
  84 class ExtendT e l where
  85     type e :&: l
  86     (.&.) :: e -> l -> e :&: l
  87
  88 instance ExtendT e Nil where
  89     type e :&: Nil = Cons e Nil
  90     e .&. nil = hCons e nil
  91
  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)
  95
  96 -- AppendT
  97 infixr 1 :++:
  98 infixr 1 .++.
  99
 100 class AppendT l l' where
 101     type l :++: l'
 102     (.++.) :: l -> l' -> l :++: l'
 103
 104 instance List l => AppendT Nil l where
 105     type Nil :++: l = l
 106     _ .++. l = l
 107
 108 instance ( List (l :++: l')
 109          , AppendT 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')
 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 -- AppendA
 134 data AppendA = AppendA
 135
 136 instance AppendT a b => Apply2T AppendA a b where
 137     type Apply2 AppendA a b = a :++: b
 138     apply2 _ a b = a .++. b
 139
 140 -- FoldrT
 141 class FoldrT f v l where
 142     type Foldr f v l
 143     hFoldr :: f -> v -> l -> Foldr f v l
 144
 145 instance FoldrT f v Nil where
 146     type Foldr f v Nil = v
 147     hFoldr _ v _ = v
 148
 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)
 154
 155 -- ConcatT
 156 class ConcatT ls where
 157     type Concat ls
 158     hConcat :: ls -> Concat ls
 159
 160 instance FoldrT AppendA Nil ls => ConcatT ls where
 161     type Concat ls = Foldr AppendA Nil ls
 162     hConcat ls = hFoldr AppendA hNil ls
 163
 164 -- MapT
 165 class MapT f l where
 166     type Map f l
 167     hMap :: f -> l -> Map f l
 168
 169 instance MapT f Nil where
 170     type Map f Nil = Nil
 171     hMap _ _ = hNil
 172
 173 instance ( ApplyT f x
 174          , MapT f xs
 175          , List (Map f xs)
 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)
 179
 180 -- All
 181 type family All f l
 182 type instance All f Nil         = True
 183 type instance All f (Cons x xs) = If (Apply f x) (All f xs) False
 184
 185 -- Length
 186 type family Length l
 187 type instance Length Nil        = D0
 188 type instance Length (Cons e l) = Succ (Length l)
 189
 190 -- Fail
 191 class Fail a
 192
 193 -- OccursMany (zero or more)
 194 class OccursMany e l where
 195     hOccursMany :: l -> [e]
 196
 197 instance OccursMany e Nil where
 198     hOccursMany _ = []
 199
 200 instance ( List l
 201          , OccursMany e l
 202          )
 203     => OccursMany e (Cons e l)
 204     where
 205       hOccursMany (Cons e l) = e : hOccursMany l
 206
 207 instance ( List l
 208          , OccursMany e l
 209          )
 210     => OccursMany e (Cons e' l)
 211     where
 212       hOccursMany (Cons _ l) = hOccursMany l
 213
 214 -- OccursMany1 (one or more)
 215 class OccursMany1 e l where
 216     hOccursMany1 :: l -> [e]
 217
 218 instance Fail (TypeNotFound e) => OccursMany1 e Nil where
 219     hOccursMany1 _ = undefined
 220
 221 instance ( List l
 222          , OccursMany e l
 223          )
 224     => OccursMany1 e (Cons e l)
 225     where
 226       hOccursMany1 (Cons e l) = e : hOccursMany l
 227
 228 instance ( List l
 229          , OccursMany1 e l
 230          )
 231     => OccursMany1 e (Cons e' l)
 232     where
 233       hOccursMany1 (Cons _ l) = hOccursMany1 l
 234
 235 -- OccursOpt (zero or one)
 236 class OccursOpt e l where
 237     hOccursOpt :: l -> Maybe e
 238
 239 instance OccursOpt e Nil where
 240     hOccursOpt _ = Nothing
 241
 242 instance OccursNot e l => OccursOpt e (Cons e l) where
 243     hOccursOpt (Cons e _) = Just e
 244
 245 instance OccursOpt e l => OccursOpt e (Cons e' l) where
 246     hOccursOpt (Cons _ l) = hOccursOpt l
 247
 248 -- Occurs (one)
 249 class Occurs e l where
 250     hOccurs :: l -> e
 251
 252 data TypeNotFound e
 253
 254 instance Fail (TypeNotFound e) => Occurs e Nil
 255     where
 256       hOccurs = undefined
 257
 258 instance ( List l
 259          , OccursNot e l
 260          )
 261     => Occurs e (Cons e l)
 262     where
 263       hOccurs (Cons e _) = e
 264
 265 instance ( List l
 266          , Occurs e l
 267          )
 268     => Occurs e (Cons e' l)
 269     where
 270       hOccurs (Cons _ l) = hOccurs l
 271
 272 -- OccursNot (zero)
 273 data     TypeFound e
 274 class    OccursNot e 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)
 278
 279 -- NoDuplicates
 280 class    NoDuplicates l
 281 instance NoDuplicates Nil
 282 instance OccursNot e l => NoDuplicates (Cons 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 -}