Language/Symantic/Typing/Constant.hs

   1 {-# LANGUAGE ConstraintKinds #-}
   2 {-# LANGUAGE GADTs #-}
   3 {-# LANGUAGE TypeInType #-}
   4 module Language.Symantic.Typing.Constant where
   5
   6 import qualified Data.Kind as Kind
   7 import qualified Data.Map.Strict as Map
   8 import qualified Data.MonoTraversable as MT
   9 import qualified Data.Sequences as Seqs
  10 import Data.NonNull (NonNull)
  11 import Data.Proxy
  12 import Data.Text (Text)
  13 import Data.Type.Equality
  14 import GHC.Exts (Constraint)
  15 import qualified System.IO as IO
  16
  17 import Language.Symantic.Lib.Data.Type.List
  18 import Language.Symantic.Lib.Data.Type.Peano
  19 import Language.Symantic.Typing.Kind
  20
  21 -- * Type 'Const'
  22 -- | A /type constant/,
  23 -- indexed at the Haskell type and term level amongst a list of them.
  24 -- When used, @c@ is actually wrapped within a 'Proxy'
  25 -- to be able to handle constants of different 'Kind's.
  26 data Const (cs::[Kind.Type]) (c::k) where
  27         ConstZ :: SKind k -> Const (Proxy c ': cs) (c::k)
  28         ConstS :: Const cs c -> Const (not_c ': cs) c
  29 infixr 5 `ConstS`
  30
  31 eq_kind_const :: Const cs (x::kx) -> Const cs (y::ky) -> Maybe (kx:~:ky)
  32 eq_kind_const x y = eq_skind (kind_of_const x) (kind_of_const y)
  33
  34 instance TestEquality (Const cs) where
  35         testEquality ConstZ{} ConstZ{}     = Just Refl
  36         testEquality (ConstS x) (ConstS y) = testEquality x y
  37         testEquality _ _                   = Nothing
  38
  39 kind_of_const :: Const cs (h::k) -> SKind k
  40 kind_of_const (ConstZ ki) = ki
  41 kind_of_const (ConstS c)  = kind_of_const c
  42
  43 -- * Type 'Inj_Const'
  44 -- | Convenient type synonym wrapping 'Inj_ConstP'
  45 -- applied on the correct 'Index'.
  46 type Inj_Const cs c = Inj_ConstP (Index cs (Proxy c)) cs c
  47
  48 -- | Inject a given /type constant/ @c@ into a list of them,
  49 -- by returning a proof that 'Proxy'@ c@ is in @cs@.
  50 inj_const :: forall cs c. Inj_Const cs c => Const cs c
  51 inj_const = inj_constP (Proxy::Proxy (Index cs (Proxy c)))
  52
  53 -- ** Class 'Inj_ConstP'
  54 class Inj_ConstP p cs c where
  55         inj_constP :: Proxy p -> Const cs c
  56 {- NOTE: using this commented instance fails very badly due to GHC-8.0.1's bug #12933
  57          which makes it fail to calculate the right kind,
  58          it seems to wrongly reuse the kind of the first use (sic)…
  59 instance IKind k => Inj_ConstP Zero (Proxy c ': cs) (c::k) where
  60         inj_constP _ = ConstZ kind
  61 -}
  62 instance
  63  ( IKindP (Ty_of_Type k)
  64  , Type_of_Ty (Ty_of_Type k) ~ k
  65  ) => Inj_ConstP Zero (Proxy c ': cs) (c::k) where
  66         inj_constP _ = ConstZ (kindP (Proxy :: Proxy (Ty_of_Type k)))
  67 instance Inj_ConstP p cs c => Inj_ConstP (Succ p) (not_c ': cs) c where
  68         inj_constP _p = ConstS (inj_constP (Proxy::Proxy p))
  69
  70 -- * Class 'Proj_Const'
  71 -- | Convenient type synonym wrapping 'Proj_ConstP'
  72 -- applied on the correct 'Index'.
  73 type Proj_Const cs c = Proj_ConstP (Index cs (Proxy c)) cs c
  74
  75 -- | Project a 'Const' onto a Haskell type level /type constant/ @c@,
  76 -- returning a proof that the 'Const' indexes @c@ iif. it's the case.
  77 proj_const :: forall cs k (c::k) (u::k).
  78  Proj_Const cs c => Const cs u -> Proxy c -> Maybe (c :~: u)
  79 proj_const = proj_constP (Proxy::Proxy (Index cs (Proxy c)))
  80
  81 (=?) :: forall cs c u. Proj_Const cs c => Const cs u -> Proxy c -> Maybe (c :~: u)
  82 (=?) = proj_constP (Proxy::Proxy (Index cs (Proxy c)))
  83
  84 -- ** Type 'Proj_ConstP'
  85 class Proj_ConstP p cs c where
  86         proj_constP :: Proxy p -> Const cs u -> Proxy c -> Maybe (c :~: u)
  87 instance Proj_ConstP Zero (Proxy c ': cs) c where
  88         proj_constP _p ConstZ{} _c = Just Refl
  89         proj_constP _p ConstS{} _c = Nothing
  90 instance Proj_ConstP p cs c => Proj_ConstP (Succ p) (not_c ': cs) c where
  91         proj_constP _p ConstZ{} _c  = Nothing
  92         proj_constP _p (ConstS u) c = proj_constP (Proxy::Proxy p) u c
  93
  94 -- ** Type 'Proj_Consts'
  95 type Proj_Consts cs cs_to_proj
  96  = Concat_Constraints (Proj_ConstsR cs cs_to_proj)
  97
  98 -- *** Type family 'Proj_ConstsR'
  99 type family Proj_ConstsR cs cs_to_proj :: [Constraint] where
 100  Proj_ConstsR cs '[] = '[]
 101  Proj_ConstsR cs (Proxy x ': xs) = Proj_Const cs x ': Proj_ConstsR cs xs
 102
 103 -- * Class 'Show_Const'
 104 class Show_Const cs where
 105         show_const :: Const cs c -> String
 106
 107 -- deriving instance Show (Const cs c)
 108 instance Show_Const cs => Show (Const cs c) where
 109         show = show_const
 110 instance Show_Const '[] where
 111         show_const = error "Show_Const unreachable pattern"
 112
 113 -- TODO: move each of these to a dedicated module.
 114 instance Show_Const cs => Show_Const (Proxy Bounded ': cs) where
 115         show_const ConstZ{} = "Bounded"
 116         show_const (ConstS c) = show_const c
 117 instance Show_Const cs => Show_Const (Proxy Enum ': cs) where
 118         show_const ConstZ{} = "Enum"
 119         show_const (ConstS c) = show_const c
 120 instance Show_Const cs => Show_Const (Proxy Fractional ': cs) where
 121         show_const ConstZ{} = "Fractional"
 122         show_const (ConstS c) = show_const c
 123 instance Show_Const cs => Show_Const (Proxy Real ': cs) where
 124         show_const ConstZ{} = "Real"
 125         show_const (ConstS c) = show_const c
 126
 127 -- * Type 'Constants'
 128 -- | Usual 'Const's.
 129 type Constants = Terms ++ Constraints
 130
 131 -- ** Type 'Terms'
 132 -- | Usual 'Const's of /terms constructors/.
 133 type Terms =
 134  [ Proxy ()
 135  , Proxy (,)
 136  , Proxy (->)
 137  , Proxy []
 138  , Proxy Bool
 139  , Proxy Char
 140  , Proxy Either
 141  , Proxy Int
 142  , Proxy Integer
 143  , Proxy Integral
 144  , Proxy IO
 145  , Proxy IO.Handle
 146  , Proxy IO.IOMode
 147  , Proxy Map.Map
 148  , Proxy Maybe
 149  , Proxy NonNull
 150  , Proxy Text
 151  ]
 152
 153 -- ** Type 'Constraints'
 154 -- | Usual 'Const's of /type constraint constructors/.
 155 type Constraints =
 156  [ Proxy Applicative
 157  , Proxy Bounded
 158  , Proxy Enum
 159  , Proxy Eq
 160  , Proxy Foldable
 161  , Proxy Functor
 162  , Proxy Monad
 163  , Proxy Monoid
 164  , Proxy MT.MonoFoldable
 165  , Proxy MT.MonoFunctor
 166  , Proxy Num
 167  , Proxy Ord
 168  , Proxy Real
 169  , Proxy Seqs.IsSequence
 170  , Proxy Seqs.SemiSequence
 171  , Proxy Show
 172  , Proxy Traversable
 173  ]