Language/Symantic/Typing/Family.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 {-# OPTIONS_GHC -fconstraint-solver-iterations=7 #-}
  13 module Language.Symantic.Typing.Family where
  14
  15 import Control.Applicative ((<|>))
  16 import Data.Proxy
  17
  18 import Language.Symantic.Typing.Type
  19
  20 -- * Type family 'Fam'
  21 -- | Apply the /type family/ selected by @fam@
  22 -- to a list of types (within a 'Proxy').
  23 type family Fam fam (hs::[*]) :: *
  24
  25 -- * Type 'Proj_Fam'
  26 -- | Convenient type synonym wrapping 'Proj_FamR'
  27 -- to initiate its recursion.
  28 type Proj_Fam cs = Proj_FamR cs cs
  29
  30 -- | Project the 'Constraint' indexed by the given 'Type'
  31 -- onto its proof, captured by 'Con' when it holds.
  32 proj_fam
  33  :: forall fam cs hs. Proj_Fam cs fam
  34  => fam -> Types cs hs -> Maybe (Type cs (Fam fam hs))
  35 proj_fam = proj_famR (Proxy::Proxy cs)
  36
  37 -- ** Class 'Proj_FamR'
  38 -- | Intermediate type class to construct an instance of 'Proj_Fam'
  39 -- from many instances of 'Proj_FamC', one for each item of @cs@.
  40 --
  41 -- * @cs@: starting  list of /type constants/.
  42 -- * @rs@: remaining list of /type constants/.
  43 class Proj_FamR cs rs fam where
  44         proj_famR
  45          :: Proxy rs -> fam -> Types cs hs
  46          -> Maybe (Type cs (Fam fam hs))
  47         proj_famR _rs _fam _ty = Nothing
  48
  49 -- | Test whether @c@ handles the work of 'Proj_Fam' or not,
  50 -- or recurse on @rs@, preserving the starting list of /type constants/.
  51 instance
  52  ( Proj_FamC cs    fam c
  53  , Proj_FamR cs rs fam
  54  ) => Proj_FamR cs (Proxy c ': rs) fam where
  55         proj_famR _rs fam ty =
  56                 proj_famC (Proxy::Proxy c)  fam ty <|>
  57                 proj_famR (Proxy::Proxy rs) fam ty
  58 -- | End the recursion.
  59 instance Proj_FamR cs '[] fam
  60
  61 -- ** Class 'Proj_FamC'
  62 -- | Handle the work of 'Proj_Fam' for a given /type family/ @fam@ and /type constant/ @c@,
  63 -- that is: maybe it handles the given /type family/,
  64 -- and if so, maybe the /type family/ has an instance for the given 'Type'.
  65 class Proj_FamC cs fam c where
  66         proj_famC
  67          :: Proxy c -> fam -> Types cs hs
  68          -> Maybe (Type cs (Fam fam hs))
  69         proj_famC _c _fam _ty = Nothing