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
  18 import Language.Symantic.Typing.Kind
  19 import Language.Symantic.Typing.Constant
  20 import Language.Symantic.Typing.Type
  21
  22 -- * Type 'Con'
  23 -- | Captures the proof of a 'Constraint'
  24 -- (and its dictionary for a type class):
  25 -- pattern matching on the 'Con' constructor
  26 -- brings the 'Constraint' into scope.
  27 data Con c where
  28         Con :: c => Con 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 -- to initiate its recursion.
 107 type Proj_Con cs = Proj_ConR cs cs
 108
 109 -- | Project the 'Constraint' indexed by the given 'Type'
 110 -- onto its proof, captured by 'Con' when it holds.
 111 proj_con
 112  :: forall cs q. Proj_Con cs
 113  => Type cs 'KiCon q
 114  -> Maybe (Con (UnProxy q))
 115 proj_con = proj_conR (Proxy::Proxy cs)
 116
 117 -- ** Class 'Proj_ConR'
 118 -- | Intermediate type class to construct an instance of 'Proj_Con'
 119 -- from many instances of 'Proj_ConC', one for each 'Const' of @cs@.
 120 --
 121 -- * @cs@: starting  list of /type constants/.
 122 -- * @rs@: remaining list of /type constants/.
 123 class Proj_ConR cs rs where
 124         proj_conR :: Proxy rs -> Type cs 'KiCon q -> Maybe (Con (UnProxy q))
 125         proj_conR _c _q = Nothing
 126
 127 -- | Test whether @c@ handles the work of 'Proj_Con' or not,
 128 -- or recurse on @rs@, preserving the starting list of /type constants/.
 129 instance
 130  ( Proj_ConC cs c
 131  , Proj_ConR cs rs
 132  ) => Proj_ConR cs (c ': rs) where
 133         proj_conR _cs q =
 134                 proj_conR (Proxy::Proxy rs) q `fromMaybe`
 135                 proj_conC (Proxy::Proxy c)  q
 136 -- | End the recursion.
 137 instance Proj_ConR cs '[] where
 138         proj_conR _cs _q = Nothing
 139
 140 -- ** Class 'Proj_ConC'
 141 -- | Handle the work of 'Proj_Con' for a given /type constant/ @c@,
 142 -- that is: maybe it handles the given 'Constraint',
 143 -- and if so, maybe the 'Constraint' holds.
 144 class Proj_ConC cs c where
 145         proj_conC :: Proxy c -> Type cs 'KiCon q -> Maybe (Maybe (Con (UnProxy q)))
 146         proj_conC _c _q = Nothing
 147
 148 instance -- []
 149  ( Proj_Const cs (Proxy [])
 150  , Proj_Consts cs (Consts_imported_by [])
 151  , Proj_Con cs
 152  ) => Proj_ConC cs (Proxy []) where
 153         proj_conC _ (TyConst q :$ TyConst c)
 154          | Just Refl <- proj_const c (Proxy::Proxy [])
 155          = Just $ case () of
 156                  _ | Just Refl <- proj_const q (Proxy::Proxy Applicative) -> Just Con
 157                    | Just Refl <- proj_const q (Proxy::Proxy Foldable)    -> Just Con
 158                    | Just Refl <- proj_const q (Proxy::Proxy Functor)     -> Just Con
 159                    | Just Refl <- proj_const q (Proxy::Proxy Monad)       -> Just Con
 160                    | Just Refl <- proj_const q (Proxy::Proxy Traversable) -> Just Con
 161                  _ -> Nothing
 162         proj_conC _ (t@(TyConst q) :$ (TyConst c :$ a))
 163          | Just Refl <- proj_const c (Proxy::Proxy [])
 164          = Just $ case () of
 165                  _ | Just Refl <- proj_const q (Proxy::Proxy Eq)
 166                    , Just Con <- proj_con (t :$ a) -> Just Con
 167                    | Just Refl <- proj_const q (Proxy::Proxy Monoid)
 168                    , Just Con <- proj_con (t :$ a) -> Just Con
 169                    | Just Refl <- proj_const q (Proxy::Proxy Ord)
 170                    , Just Con <- proj_con (t :$ a) -> Just Con
 171                  _ -> Nothing
 172         proj_conC _c _q = Nothing
 173 instance -- (->)
 174  ( Proj_Const cs (Proxy (->))
 175  , Proj_Consts cs (Consts_imported_by (->))
 176  , Proj_Con cs
 177  ) => Proj_ConC cs (Proxy (->)) where
 178         proj_conC _ (TyConst q :$ (TyConst c :$ _r))
 179          | Just Refl <- proj_const c (Proxy::Proxy (->))
 180          = Just $ case () of
 181                  _ | Just Refl <- proj_const q (Proxy::Proxy Functor)     -> Just Con
 182                    | Just Refl <- proj_const q (Proxy::Proxy Applicative) -> Just Con
 183                    | Just Refl <- proj_const q (Proxy::Proxy Monad)       -> Just Con
 184                  _ -> Nothing
 185         proj_conC _ (t@(TyConst q) :$ (TyConst c :$ _a :$ b))
 186          | Just Refl <- proj_const c (Proxy::Proxy (->))
 187          = Just $ case () of
 188                  _ | Just Refl <- proj_const q (Proxy::Proxy Monoid)
 189                    , Just Con <- proj_con (t :$ b) -> Just Con
 190                  _ -> Nothing
 191         proj_conC _c _q = Nothing
 192 instance -- Applicative
 193  ( Proj_Const cs (Proxy Applicative)
 194  , Proj_Consts cs (Consts_imported_by Applicative)
 195  ) => Proj_ConC cs (Proxy Applicative)
 196 instance -- Bool
 197  ( Proj_Const cs (Proxy Bool)
 198  , Proj_Consts cs (Consts_imported_by Bool)
 199  ) => Proj_ConC cs (Proxy Bool) where
 200         proj_conC _ (TyConst q :$ TyConst c)
 201          | Just Refl <- proj_const c (Proxy::Proxy Bool)
 202          = Just $ case () of
 203                  _ | Just Refl <- proj_const q (Proxy::Proxy Bounded) -> Just Con
 204                    | Just Refl <- proj_const q (Proxy::Proxy Enum)    -> Just Con
 205                    | Just Refl <- proj_const q (Proxy::Proxy Eq)      -> Just Con
 206                    | Just Refl <- proj_const q (Proxy::Proxy Ord)     -> Just Con
 207                  _ -> Nothing
 208         proj_conC _c _q = Nothing
 209 instance -- Bounded
 210  ( Proj_Const cs (Proxy Bounded)
 211  , Proj_Consts cs (Consts_imported_by Bounded)
 212  ) => Proj_ConC cs (Proxy Bounded)
 213 instance -- Enum
 214  ( Proj_Const cs (Proxy Enum)
 215  , Proj_Consts cs (Consts_imported_by Enum)
 216  ) => Proj_ConC cs (Proxy Enum)
 217 instance -- Eq
 218  ( Proj_Const cs (Proxy Eq)
 219  , Proj_Consts cs (Consts_imported_by Eq)
 220  ) => Proj_ConC cs (Proxy Eq)
 221 instance -- Foldable
 222  ( Proj_Const cs (Proxy Foldable)
 223  , Proj_Consts cs (Consts_imported_by Foldable)
 224  ) => Proj_ConC cs (Proxy Foldable)
 225 instance -- Functor
 226  ( Proj_Const cs (Proxy Functor)
 227  , Proj_Consts cs (Consts_imported_by Functor)
 228  ) => Proj_ConC cs (Proxy Functor)
 229 instance -- Int
 230  ( Proj_Const cs (Proxy Int)
 231  , Proj_Consts cs (Consts_imported_by Int)
 232  ) => Proj_ConC cs (Proxy Int) where
 233         proj_conC _ (TyConst q :$ TyConst c)
 234          | Just Refl <- proj_const c (Proxy::Proxy Int)
 235          = Just $ case () of
 236                  _ | Just Refl <- proj_const q (Proxy::Proxy Bounded)  -> Just Con
 237                    | Just Refl <- proj_const q (Proxy::Proxy Enum)     -> Just Con
 238                    | Just Refl <- proj_const q (Proxy::Proxy Eq)       -> Just Con
 239                    | Just Refl <- proj_const q (Proxy::Proxy Integral) -> Just Con
 240                    | Just Refl <- proj_const q (Proxy::Proxy Num)      -> Just Con
 241                    | Just Refl <- proj_const q (Proxy::Proxy Ord)      -> Just Con
 242                    | Just Refl <- proj_const q (Proxy::Proxy Real)     -> Just Con
 243                  _ -> Nothing
 244         proj_conC _c _q = Nothing
 245 instance -- Integer
 246  ( Proj_Const cs (Proxy Integer)
 247  , Proj_Consts cs (Consts_imported_by Integer)
 248  ) => Proj_ConC cs (Proxy Integer) where
 249         proj_conC _ (TyConst q :$ TyConst c)
 250          | Just Refl <- proj_const c (Proxy::Proxy Integer)
 251          = Just $ case () of
 252                  _ | Just Refl <- proj_const q (Proxy::Proxy Enum)     -> Just Con
 253                    | Just Refl <- proj_const q (Proxy::Proxy Eq)       -> Just Con
 254                    | Just Refl <- proj_const q (Proxy::Proxy Integral) -> Just Con
 255                    | Just Refl <- proj_const q (Proxy::Proxy Num)      -> Just Con
 256                    | Just Refl <- proj_const q (Proxy::Proxy Ord)      -> Just Con
 257                    | Just Refl <- proj_const q (Proxy::Proxy Real)     -> Just Con
 258                  _ -> Nothing
 259         proj_conC _c _q = Nothing
 260 instance -- Integral
 261  ( Proj_Const cs (Proxy Integral)
 262  , Proj_Consts cs (Consts_imported_by Integral)
 263  ) => Proj_ConC cs (Proxy Integral)
 264 instance -- IO
 265  ( Proj_Const cs (Proxy IO)
 266  , Proj_Consts cs (Consts_imported_by IO)
 267  ) => Proj_ConC cs (Proxy IO) where
 268         proj_conC _ (TyConst q :$ TyConst c)
 269          | Just Refl <- proj_const c (Proxy::Proxy IO)
 270          = Just $ case () of
 271                  _ | Just Refl <- proj_const q (Proxy::Proxy Applicative) -> Just Con
 272                    | Just Refl <- proj_const q (Proxy::Proxy Functor)     -> Just Con
 273                    | Just Refl <- proj_const q (Proxy::Proxy Monad)       -> Just Con
 274                  _ -> Nothing
 275         proj_conC _c _q = Nothing
 276 instance -- Maybe
 277  ( Proj_Const cs (Proxy Maybe)
 278  , Proj_Consts cs (Consts_imported_by Maybe)
 279  , Proj_Con cs
 280  ) => Proj_ConC cs (Proxy Maybe) where
 281         proj_conC _ (TyConst q :$ TyConst c)
 282          | Just Refl <- proj_const c (Proxy::Proxy Maybe)
 283          = Just $ case () of
 284                  _ | Just Refl <- proj_const q (Proxy::Proxy Applicative) -> Just Con
 285                    | Just Refl <- proj_const q (Proxy::Proxy Foldable)    -> Just Con
 286                    | Just Refl <- proj_const q (Proxy::Proxy Functor)     -> Just Con
 287                    | Just Refl <- proj_const q (Proxy::Proxy Monad)       -> Just Con
 288                    | Just Refl <- proj_const q (Proxy::Proxy Traversable) -> Just Con
 289                  _ -> Nothing
 290         proj_conC _ (t@(TyConst q) :$ (TyConst c :$ a))
 291          | Just Refl <- proj_const c (Proxy::Proxy Maybe)
 292          = Just $ case () of
 293                  _ | Just Refl <- proj_const q (Proxy::Proxy Eq)
 294                    , Just Con <- proj_con (t :$ a) -> Just Con
 295                    | Just Refl <- proj_const q (Proxy::Proxy Monoid)
 296                    , Just Con <- proj_con (t :$ a) -> Just Con
 297                  _ -> Nothing
 298         proj_conC _c _q = Nothing
 299 instance -- Monad
 300  ( Proj_Const cs (Proxy Monad)
 301  , Proj_Consts cs (Consts_imported_by Monad)
 302  ) => Proj_ConC cs (Proxy Monad)
 303 instance -- Monoid
 304  ( Proj_Const cs (Proxy Monoid)
 305  , Proj_Consts cs (Consts_imported_by Monoid)
 306  ) => Proj_ConC cs (Proxy Monoid)
 307 instance -- Num
 308  ( Proj_Const cs (Proxy Num)
 309  , Proj_Consts cs (Consts_imported_by Num)
 310  ) => Proj_ConC cs (Proxy Num)
 311 instance -- Ord
 312  ( Proj_Const cs (Proxy Ord)
 313  , Proj_Consts cs (Consts_imported_by Ord)
 314  ) => Proj_ConC cs (Proxy Ord)
 315 instance -- Real
 316  ( Proj_Const cs (Proxy Real)
 317  , Proj_Consts cs (Consts_imported_by Real)
 318  ) => Proj_ConC cs (Proxy Real)
 319 instance -- Traversable
 320  ( Proj_Const cs (Proxy Traversable)
 321  , Proj_Consts cs (Consts_imported_by Traversable)
 322  ) => Proj_ConC cs (Proxy Traversable)