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 'Const_from'
 104 -- | Try to build a 'Const' from raw data.
 105 class Const_from raw cs where
 106         const_from
 107          :: raw -> (forall k c. Const cs (c::k) -> Maybe ret)
 108          -> Maybe ret
 109
 110 instance Const_from raw '[] where
 111         const_from _c _k = Nothing
 112
 113 -- TODO: move each of these to a dedicated module.
 114 instance Const_from Text cs => Const_from Text (Proxy Bounded ': cs) where
 115         const_from "Bounded" k = k (ConstZ kind)
 116         const_from s k = const_from s $ k . ConstS
 117 instance Const_from Text cs => Const_from Text (Proxy Enum ': cs) where
 118         const_from "Enum" k = k (ConstZ kind)
 119         const_from s k = const_from s $ k . ConstS
 120 instance Const_from Text cs => Const_from Text (Proxy Fractional ': cs) where
 121         const_from "Fractional" k = k (ConstZ kind)
 122         const_from s k = const_from s $ k . ConstS
 123 instance Const_from Text cs => Const_from Text (Proxy Real ': cs) where
 124         const_from "Real" k = k (ConstZ kind)
 125         const_from s k = const_from s $ k . ConstS
 126
 127 -- * Class 'Show_Const'
 128 class Show_Const cs where
 129         show_const :: Const cs c -> String
 130
 131 -- deriving instance Show (Const cs c)
 132 instance Show_Const cs => Show (Const cs c) where
 133         show = show_const
 134 instance Show_Const '[] where
 135         show_const = error "Show_Const unreachable pattern"
 136
 137 -- TODO: move each of these to a dedicated module.
 138 instance Show_Const cs => Show_Const (Proxy Bounded ': cs) where
 139         show_const ConstZ{} = "Bounded"
 140         show_const (ConstS c) = show_const c
 141 instance Show_Const cs => Show_Const (Proxy Enum ': cs) where
 142         show_const ConstZ{} = "Enum"
 143         show_const (ConstS c) = show_const c
 144 instance Show_Const cs => Show_Const (Proxy Fractional ': cs) where
 145         show_const ConstZ{} = "Fractional"
 146         show_const (ConstS c) = show_const c
 147 instance Show_Const cs => Show_Const (Proxy Real ': cs) where
 148         show_const ConstZ{} = "Real"
 149         show_const (ConstS c) = show_const c
 150
 151 -- * Type 'Constants'
 152 -- | Usual 'Const's.
 153 type Constants = Terms ++ Constraints
 154
 155 -- ** Type 'Terms'
 156 -- | Usual 'Const's of /terms constructors/.
 157 type Terms =
 158  [ Proxy ()
 159  , Proxy (,)
 160  , Proxy (->)
 161  , Proxy []
 162  , Proxy Bool
 163  , Proxy Char
 164  , Proxy Either
 165  , Proxy Int
 166  , Proxy Integer
 167  , Proxy Integral
 168  , Proxy IO
 169  , Proxy IO.Handle
 170  , Proxy IO.IOMode
 171  , Proxy Map.Map
 172  , Proxy Maybe
 173  , Proxy NonNull
 174  , Proxy Text
 175  ]
 176
 177 -- ** Type 'Constraints'
 178 -- | Usual 'Const's of /type constraint constructors/.
 179 type Constraints =
 180  [ Proxy Applicative
 181  , Proxy Bounded
 182  , Proxy Enum
 183  , Proxy Eq
 184  , Proxy Foldable
 185  , Proxy Functor
 186  , Proxy Monad
 187  , Proxy Monoid
 188  , Proxy MT.MonoFoldable
 189  , Proxy MT.MonoFunctor
 190  , Proxy Num
 191  , Proxy Ord
 192  , Proxy Real
 193  , Proxy Seqs.IsSequence
 194  , Proxy Seqs.SemiSequence
 195  , Proxy Show
 196  , Proxy Traversable
 197  ]