Language/Symantic/Typing/Constraint.hs

   1 {-# LANGUAGE DataKinds #-}
   2 {-# LANGUAGE PolyKinds #-}
   3 {-# LANGUAGE ConstraintKinds #-}
   4 {-# LANGUAGE FlexibleContexts #-}
   5 {-# LANGUAGE FlexibleInstances #-}
   6 {-# LANGUAGE GADTs #-}
   7 {-# LANGUAGE MultiParamTypeClasses #-}
   8 {-# LANGUAGE ScopedTypeVariables #-}
   9 {-# LANGUAGE TypeFamilies #-}
  10 {-# LANGUAGE TypeOperators #-}
  11 {-# LANGUAGE UndecidableInstances #-}
  12 module Language.Symantic.Typing.Constraint where
  13
  14 import Data.Maybe (fromMaybe)
  15 import Data.Proxy
  16 import Data.Type.Equality
  17 import GHC.Prim (Constraint)
  18
  19 import Language.Symantic.Typing.Kind
  20 import Language.Symantic.Typing.Constant
  21 import Language.Symantic.Typing.Type
  22
  23 -- * Type 'Dict'
  24 -- | 'Dict' captures the dictionary of a 'Constraint':
  25 -- pattern matching on the 'Dict' constructor
  26 -- brings the 'Constraint' into scope.
  27 data Dict :: Constraint -> * where
  28         Dict :: c => Dict c
  29
  30 -- * Type family 'Consts_imported_by'
  31 -- | Return the /type constant/s that a given /type constant/
  32 -- wants to be part of the final list of /type constants/.
  33 type family Consts_imported_by (c::k) :: [*]
  34 type instance Consts_imported_by [] =
  35  [ Proxy Applicative
  36  , Proxy Eq
  37  , Proxy Foldable
  38  , Proxy Functor
  39  , Proxy Monad
  40  , Proxy Monoid
  41  , Proxy Ord
  42  , Proxy Traversable
  43  ]
  44 type instance Consts_imported_by (->) =
  45  [ Proxy Applicative
  46  , Proxy Functor
  47  , Proxy Monad
  48  , Proxy Monoid
  49  ]
  50 type instance Consts_imported_by Applicative = '[]
  51 type instance Consts_imported_by Bool =
  52  [ Proxy Bounded
  53  , Proxy Enum
  54  , Proxy Eq
  55  , Proxy Ord
  56  ]
  57 type instance Consts_imported_by Bounded = '[]
  58 type instance Consts_imported_by Eq = '[]
  59 type instance Consts_imported_by Enum = '[]
  60 type instance Consts_imported_by Foldable = '[]
  61 type instance Consts_imported_by Functor = '[]
  62 type instance Consts_imported_by Int =
  63  [ Proxy Bounded
  64  , Proxy Enum
  65  , Proxy Eq
  66  , Proxy Integral
  67  , Proxy Num
  68  , Proxy Ord
  69  , Proxy Real
  70  ]
  71 type instance Consts_imported_by Integer =
  72  [ Proxy Enum
  73  , Proxy Eq
  74  , Proxy Integral
  75  , Proxy Num
  76  , Proxy Ord
  77  , Proxy Real
  78  ]
  79 type instance Consts_imported_by Integral =
  80  [ Proxy Enum
  81  , Proxy Real
  82  ]
  83 type instance Consts_imported_by IO =
  84  [ Proxy Applicative
  85  , Proxy Functor
  86  , Proxy Monad
  87  ]
  88 type instance Consts_imported_by Maybe =
  89  [ Proxy Applicative
  90  , Proxy Eq
  91  , Proxy Foldable
  92  , Proxy Functor
  93  , Proxy Monad
  94  , Proxy Monoid
  95  , Proxy Traversable
  96  ]
  97 type instance Consts_imported_by Monad = '[]
  98 type instance Consts_imported_by Monoid = '[]
  99 type instance Consts_imported_by Num = '[]
 100 type instance Consts_imported_by Ord = '[]
 101 type instance Consts_imported_by Real = '[]
 102 type instance Consts_imported_by Traversable = '[]
 103
 104 -- * Type 'Proj_Con'
 105 -- | Convenient type synonym wrapping 'Proj_ConR'
 106 -- initiating its recursion.
 107 type Proj_Con cs = Proj_ConR cs cs
 108
 109 -- | Project a /type class/ constructor
 110 -- applied to a parameter onto a 'Constraint'.
 111 proj_con
 112  :: forall cs q x ki_x. Proj_Con cs
 113  => Type cs (ki_x ':> 'KiCon) q -- ^ 'Constraint' constructor.
 114  -> Type cs ki_x x -- ^ Parameter for the 'Constraint' constructor.
 115  -> Maybe (Dict (Con q x)) -- ^ 'Constraint' projected onto.
 116 proj_con = proj_conR (Proxy::Proxy cs)
 117
 118 -- ** Class 'Proj_ConR'
 119 -- | Intermediate type class to construct an instance of 'Proj_Con'
 120 -- from many instances of 'Proj_ConC', one for each 'Const' of @cs@.
 121 --
 122 -- * @cs@: starting  list of /type constants/.
 123 -- * @rs@: remaining list of /type constants/.
 124 class Proj_ConR cs rs where
 125         proj_conR
 126          :: Proxy rs
 127          -> Type cs (ki_x ':> 'KiCon) q
 128          -> Type cs ki_x x
 129          -> Maybe (Dict (Con q x))
 130         proj_conR _c _x _y = Nothing
 131
 132 -- | Test whether @c@ handles the work of 'Proj_Con' or not,
 133 -- or recurse on @rs@, preserving the starting list of /type constants/.
 134 instance
 135  ( Proj_ConC cs c
 136  , Proj_ConR cs rs
 137  ) => Proj_ConR cs (c ': rs) where
 138         proj_conR _cs x y =
 139                 proj_conR (Proxy::Proxy rs) x y `fromMaybe`
 140                 proj_conC (Proxy::Proxy c)  x y
 141 -- | End the recursion.
 142 instance Proj_ConR cs '[] where
 143         proj_conR _cs _x _y = Nothing
 144
 145 -- ** Class 'Proj_ConC'
 146 class Proj_ConC cs c where
 147         proj_conC
 148          :: Proxy c
 149          -> Type cs (ki_x ':> 'KiCon) q
 150          -> Type cs ki_x x
 151          -> Maybe (Maybe (Dict (Con q x)))
 152         proj_conC _c _x _y = Nothing
 153
 154 instance -- []
 155  ( Proj_Const cs (Proxy [])
 156  , Proj_Consts cs (Consts_imported_by [])
 157  , Proj_Con cs
 158  ) => Proj_ConC cs (Proxy []) where
 159         proj_conC _ x (TyConst c)
 160          | Just Refl <- proj_const c (Proxy::Proxy [])
 161          = Just $ case x of
 162                  TyConst q
 163                   | Just Refl <- proj_const q (Proxy::Proxy Applicative) -> Just Dict
 164                   | Just Refl <- proj_const q (Proxy::Proxy Foldable)    -> Just Dict
 165                   | Just Refl <- proj_const q (Proxy::Proxy Functor)     -> Just Dict
 166                   | Just Refl <- proj_const q (Proxy::Proxy Monad)       -> Just Dict
 167                   | Just Refl <- proj_const q (Proxy::Proxy Traversable) -> Just Dict
 168                  _ -> Nothing
 169         proj_conC _ x (TyConst c :$ a)
 170          | Just Refl <- proj_const c (Proxy::Proxy [])
 171          = Just $ case x of
 172                  t@(TyConst q)
 173                   | Just Refl <- proj_const q (Proxy::Proxy Eq)
 174                   , Just Dict <- proj_con t a -> Just Dict
 175                  t@(TyConst q)
 176                   | Just Refl <- proj_const q (Proxy::Proxy Monoid)
 177                   , Just Dict <- proj_con t a -> Just Dict
 178                  t@(TyConst q)
 179                   | Just Refl <- proj_const q (Proxy::Proxy Ord)
 180                   , Just Dict <- proj_con t a -> Just Dict
 181                  _ -> Nothing
 182         proj_conC _ _ _ = Nothing
 183 instance -- (->)
 184  ( Proj_Const cs (Proxy (->))
 185  , Proj_Consts cs (Consts_imported_by (->))
 186  , Proj_Con cs
 187  ) => Proj_ConC cs (Proxy (->)) where
 188         proj_conC _ x (TyConst c :$ _r)
 189          | Just Refl <- proj_const c (Proxy::Proxy (->))
 190          = Just $ case x of
 191                  (TyConst q)
 192                   | Just Refl <- proj_const q (Proxy::Proxy Functor)     -> Just Dict
 193                   | Just Refl <- proj_const q (Proxy::Proxy Applicative) -> Just Dict
 194                   | Just Refl <- proj_const q (Proxy::Proxy Monad)       -> Just Dict
 195                  _ -> Nothing
 196         proj_conC _ x (TyConst c :$ _a :$ b)
 197          | Just Refl <- proj_const c (Proxy::Proxy (->))
 198          = Just $ case x of
 199                  t@(TyConst q)
 200                   | Just Refl <- proj_const q (Proxy::Proxy Monoid)
 201                   , Just Dict <- proj_con t b
 202                   -> Just Dict
 203                  _ -> Nothing
 204         proj_conC _ _ _ = Nothing
 205 instance -- Applicative
 206  ( Proj_Const cs (Proxy Applicative)
 207  , Proj_Consts cs (Consts_imported_by Applicative)
 208  ) => Proj_ConC cs (Proxy Applicative)
 209 instance -- Bool
 210  ( Proj_Const cs (Proxy Bool)
 211  , Proj_Consts cs (Consts_imported_by Bool)
 212  ) => Proj_ConC cs (Proxy Bool) where
 213         proj_conC _ x (TyConst c)
 214          | Just Refl <- proj_const c (Proxy::Proxy Bool)
 215          = Just $ case x of
 216                  TyConst q
 217                   | Just Refl <- proj_const q (Proxy::Proxy Bounded) -> Just Dict
 218                   | Just Refl <- proj_const q (Proxy::Proxy Enum)    -> Just Dict
 219                   | Just Refl <- proj_const q (Proxy::Proxy Eq)      -> Just Dict
 220                   | Just Refl <- proj_const q (Proxy::Proxy Ord)     -> Just Dict
 221                  _ -> Nothing
 222         proj_conC _ _ _ = Nothing
 223 instance -- Bounded
 224  ( Proj_Const cs (Proxy Bounded)
 225  , Proj_Consts cs (Consts_imported_by Bounded)
 226  ) => Proj_ConC cs (Proxy Bounded)
 227 instance -- Enum
 228  ( Proj_Const cs (Proxy Enum)
 229  , Proj_Consts cs (Consts_imported_by Enum)
 230  ) => Proj_ConC cs (Proxy Enum)
 231 instance -- Eq
 232  ( Proj_Const cs (Proxy Eq)
 233  , Proj_Consts cs (Consts_imported_by Eq)
 234  ) => Proj_ConC cs (Proxy Eq)
 235 instance -- Foldable
 236  ( Proj_Const cs (Proxy Foldable)
 237  , Proj_Consts cs (Consts_imported_by Foldable)
 238  ) => Proj_ConC cs (Proxy Foldable)
 239 instance -- Functor
 240  ( Proj_Const cs (Proxy Functor)
 241  , Proj_Consts cs (Consts_imported_by Functor)
 242  ) => Proj_ConC cs (Proxy Functor)
 243 instance -- Int
 244  ( Proj_Const cs (Proxy Int)
 245  , Proj_Consts cs (Consts_imported_by Int)
 246  ) => Proj_ConC cs (Proxy Int) where
 247         proj_conC _ x (TyConst c)
 248          | Just Refl <- proj_const c (Proxy::Proxy Int)
 249          = Just $ case x of
 250                  TyConst q
 251                   | Just Refl <- proj_const q (Proxy::Proxy Bounded)  -> Just Dict
 252                   | Just Refl <- proj_const q (Proxy::Proxy Enum)     -> Just Dict
 253                   | Just Refl <- proj_const q (Proxy::Proxy Eq)       -> Just Dict
 254                   | Just Refl <- proj_const q (Proxy::Proxy Integral) -> Just Dict
 255                   | Just Refl <- proj_const q (Proxy::Proxy Num)      -> Just Dict
 256                   | Just Refl <- proj_const q (Proxy::Proxy Ord)      -> Just Dict
 257                   | Just Refl <- proj_const q (Proxy::Proxy Real)     -> Just Dict
 258                  _ -> Nothing
 259         proj_conC _ _ _ = Nothing
 260 instance -- Integer
 261  ( Proj_Const cs (Proxy Integer)
 262  , Proj_Consts cs (Consts_imported_by Integer)
 263  ) => Proj_ConC cs (Proxy Integer) where
 264         proj_conC _ x (TyConst c)
 265          | Just Refl <- proj_const c (Proxy::Proxy Integer)
 266          = Just $ case x of
 267                  TyConst q
 268                   | Just Refl <- proj_const q (Proxy::Proxy Enum)     -> Just Dict
 269                   | Just Refl <- proj_const q (Proxy::Proxy Eq)       -> Just Dict
 270                   | Just Refl <- proj_const q (Proxy::Proxy Integral) -> Just Dict
 271                   | Just Refl <- proj_const q (Proxy::Proxy Num)      -> Just Dict
 272                   | Just Refl <- proj_const q (Proxy::Proxy Ord)      -> Just Dict
 273                   | Just Refl <- proj_const q (Proxy::Proxy Real)     -> Just Dict
 274                  _ -> Nothing
 275         proj_conC _ _ _ = Nothing
 276 instance -- Integral
 277  ( Proj_Const cs (Proxy Integral)
 278  , Proj_Consts cs (Consts_imported_by Integral)
 279  ) => Proj_ConC cs (Proxy Integral)
 280 instance -- IO
 281  ( Proj_Const cs (Proxy IO)
 282  , Proj_Consts cs (Consts_imported_by IO)
 283  ) => Proj_ConC cs (Proxy IO) where
 284         proj_conC _ x (TyConst c)
 285          | Just Refl <- proj_const c (Proxy::Proxy IO)
 286          = Just $ case x of
 287                  TyConst q
 288                   | Just Refl <- proj_const q (Proxy::Proxy Applicative) -> Just Dict
 289                   | Just Refl <- proj_const q (Proxy::Proxy Functor)     -> Just Dict
 290                   | Just Refl <- proj_const q (Proxy::Proxy Monad)       -> Just Dict
 291                  _ -> Nothing
 292         proj_conC _ _ _ = Nothing
 293 instance -- Maybe
 294  ( Proj_Const cs (Proxy Maybe)
 295  , Proj_Consts cs (Consts_imported_by Maybe)
 296  , Proj_Con cs
 297  ) => Proj_ConC cs (Proxy Maybe) where
 298         proj_conC _ x (TyConst c)
 299          | Just Refl <- proj_const c (Proxy::Proxy Maybe)
 300          = Just $ case x of
 301                  TyConst q
 302                   | Just Refl <- proj_const q (Proxy::Proxy Applicative) -> Just Dict
 303                   | Just Refl <- proj_const q (Proxy::Proxy Foldable)    -> Just Dict
 304                   | Just Refl <- proj_const q (Proxy::Proxy Functor)     -> Just Dict
 305                   | Just Refl <- proj_const q (Proxy::Proxy Monad)       -> Just Dict
 306                   | Just Refl <- proj_const q (Proxy::Proxy Traversable) -> Just Dict
 307                  _ -> Nothing
 308         proj_conC _ x (TyConst c :$ a)
 309          | Just Refl <- proj_const c (Proxy::Proxy Maybe)
 310          = Just $ case x of
 311                  t@(TyConst q)
 312                   | Just Refl <- proj_const q (Proxy::Proxy Eq)
 313                   , Just Dict <- proj_con t a -> Just Dict
 314                  t@(TyConst q)
 315                   | Just Refl <- proj_const q (Proxy::Proxy Monoid)
 316                   , Just Dict <- proj_con t a -> Just Dict
 317                  _ -> Nothing
 318         proj_conC _ _ _ = Nothing
 319 instance -- Monad
 320  ( Proj_Const cs (Proxy Monad)
 321  , Proj_Consts cs (Consts_imported_by Monad)
 322  ) => Proj_ConC cs (Proxy Monad)
 323 instance -- Monoid
 324  ( Proj_Const cs (Proxy Monoid)
 325  , Proj_Consts cs (Consts_imported_by Monoid)
 326  ) => Proj_ConC cs (Proxy Monoid)
 327 instance -- Num
 328  ( Proj_Const cs (Proxy Num)
 329  , Proj_Consts cs (Consts_imported_by Num)
 330  ) => Proj_ConC cs (Proxy Num)
 331 instance -- Ord
 332  ( Proj_Const cs (Proxy Ord)
 333  , Proj_Consts cs (Consts_imported_by Ord)
 334  ) => Proj_ConC cs (Proxy Ord)
 335 instance -- Real
 336  ( Proj_Const cs (Proxy Real)
 337  , Proj_Consts cs (Consts_imported_by Real)
 338  ) => Proj_ConC cs (Proxy Real)
 339 instance -- Traversable
 340  ( Proj_Const cs (Proxy Traversable)
 341  , Proj_Consts cs (Consts_imported_by Traversable)
 342  ) => Proj_ConC cs (Proxy Traversable)