Language/Symantic/Typing/Constraint.hs

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