Language/Symantic/Typing/Constraint.hs

   1 {-# LANGUAGE ConstraintKinds #-}
   2 {-# LANGUAGE GADTs #-}
   3 {-# LANGUAGE PolyKinds #-}
   4 {-# LANGUAGE UndecidableInstances #-}
   5 {-# OPTIONS_GHC -fconstraint-solver-iterations=7 #-}
   6 module Language.Symantic.Typing.Constraint where
   7
   8 import Control.Applicative ((<|>))
   9 import Data.Proxy
  10
  11 import Language.Symantic.Typing.Type
  12
  13 -- * Type 'Con'
  14 -- | Captures the proof of a 'Constraint'
  15 -- (and its dictionary for a type class):
  16 -- pattern matching on the 'Con' constructor
  17 -- brings the 'Constraint' into scope.
  18 data Con c where
  19         Con :: c => Con c
  20
  21 -- * Type family 'Consts_imported_by'
  22 -- | Return the /type constant/s that a given /type constant/
  23 -- wants to be part of the final list of /type constants/.
  24 type family Consts_imported_by (c::k) :: [*]
  25 type instance Consts_imported_by Bounded = '[]
  26 type instance Consts_imported_by Enum = '[]
  27 type instance Consts_imported_by Real = '[]
  28
  29 -- * Type 'Proj_Con'
  30 -- | Convenient type synonym wrapping 'Proj_ConR'
  31 -- to initiate its recursion.
  32 type Proj_Con cs = Proj_ConR cs cs
  33
  34 -- | Project the 'Constraint' indexed by the given 'Type'
  35 -- onto its proof, captured by 'Con' when it holds.
  36 proj_con
  37  :: forall cs q. Proj_Con cs
  38  => Type cs q
  39  -> Maybe (Con q)
  40 proj_con = proj_conR (Proxy @cs)
  41
  42 -- ** Class 'Proj_ConR'
  43 -- | Intermediate type class to construct an instance of 'Proj_Con'
  44 -- from many instances of 'Proj_ConC', one for each item of @cs@.
  45 --
  46 -- * @cs@: starting  list of /type constants/.
  47 -- * @rs@: remaining list of /type constants/.
  48 class Proj_ConR cs rs where
  49         proj_conR :: Proxy rs -> Type cs q -> Maybe (Con q)
  50         proj_conR _rs _q = Nothing
  51
  52 -- | Test whether @c@ handles the work of 'Proj_Con' or not,
  53 -- or recurse on @rs@, preserving the starting list of /type constants/.
  54 instance
  55  ( Proj_ConC cs c
  56  , Proj_ConR cs rs
  57  ) => Proj_ConR cs (c ': rs) where
  58         proj_conR _rs q =
  59                 proj_conC (Proxy @c)  q <|>
  60                 proj_conR (Proxy @rs) q
  61 -- | End the recursion.
  62 instance Proj_ConR cs '[]
  63
  64 -- ** Class 'Proj_ConC'
  65 -- | Handle the work of 'Proj_Con' for a given /type constant/ @c@,
  66 -- that is: maybe it handles the given 'Constraint',
  67 -- and if so, maybe the 'Constraint' holds.
  68 class Proj_ConC cs c where
  69         proj_conC :: Proxy c -> Type cs q -> Maybe (Con q)
  70         proj_conC _c _q = Nothing
  71
  72 instance Proj_ConC cs (Proxy Bounded)
  73 instance Proj_ConC cs (Proxy Enum)
  74 instance Proj_ConC cs (Proxy Real)