]> Git — Sourcephile - haskell/symantic.git/blob - symantic/Language/Symantic/Typing/Family.hs
Add IsString instances.
[haskell/symantic.git] / symantic / Language / Symantic / Typing / Family.hs
1 {-# LANGUAGE ConstraintKinds #-}
2 {-# LANGUAGE PolyKinds #-}
3 module Language.Symantic.Typing.Family where
4
5 import Control.Applicative ((<|>))
6 import Data.Proxy
7 import Data.Text (Text)
8
9 import Language.Symantic.Typing.Type
10
11 -- * Type family 'TyFam'
12 -- | Apply the /type family/ selected by @fam@
13 -- to a list of types (within a 'Proxy').
14 type family TyFam fam (hs::[*]) :: *
15
16 -- * Type 'TyFamName'
17 type TyFamName = Text
18
19 -- * Type 'Proj_TyFam'
20 -- | Convenient type synonym wrapping 'Proj_TyFamR'
21 -- to initiate its recursion.
22 type Proj_TyFam cs = Proj_TyFamR cs cs
23
24 -- | Project the 'Constraint' indexed by the given 'Type'
25 -- onto its proof, captured by 'TyCon' when it holds.
26 proj_TyFam
27 :: forall fam cs hs. Proj_TyFam cs fam
28 => fam -> Types cs hs -> Maybe (Type cs (TyFam fam hs))
29 proj_TyFam = proj_TyFamR (Proxy @cs)
30
31 -- ** Class 'Proj_TyFamR'
32 -- | Intermediate type class to construct an instance of 'Proj_TyFam'
33 -- from many instances of 'Proj_TyFamC', one for each item of @cs@.
34 --
35 -- * @cs@: starting list of /type constants/.
36 -- * @rs@: remaining list of /type constants/.
37 class Proj_TyFamR (cs::[*]) (rs::[*]) fam where
38 proj_TyFamR
39 :: Proxy rs -> fam -> Types cs hs
40 -> Maybe (Type cs (TyFam fam hs))
41 proj_TyFamR _rs _fam _ty = Nothing
42
43 -- | Test whether @c@ handles the work of 'Proj_TyFam' or not,
44 -- or recurse on @rs@, preserving the starting list of /type constants/.
45 instance
46 ( Proj_TyFamC cs fam c
47 , Proj_TyFamR cs rs fam
48 ) => Proj_TyFamR cs (Proxy c ': rs) fam where
49 proj_TyFamR _rs fam typ =
50 proj_TyFamC (Proxy @c) fam typ <|>
51 proj_TyFamR (Proxy @rs) fam typ
52 -- | End the recursion.
53 instance Proj_TyFamR cs '[] fam
54
55 -- ** Class 'Proj_TyFamC'
56 -- | Handle the work of 'Proj_TyFam' for a given /type family/ @fam@ and /type constant/ @c@,
57 -- that is: maybe it handles the given /type family/,
58 -- and if so, maybe the /type family/ has an instance for the given 'Type'.
59 class Proj_TyFamC cs fam (c::kc) where
60 proj_TyFamC
61 :: Proxy c -> fam -> Types cs hs
62 -> Maybe (Type cs (TyFam fam hs))
63 proj_TyFamC _c _fam _ty = Nothing