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