Language/Symantic/Typing/Constant.hs

   1 {-# LANGUAGE GADTs #-}
   2 {-# LANGUAGE TypeInType #-}
   3 module Language.Symantic.Typing.Constant where
   4
   5 import qualified Data.Kind as Kind
   6 import qualified Data.Map.Strict as Map
   7 import qualified Data.MonoTraversable as MT
   8 import qualified Data.Sequences as Seqs
   9 import Data.NonNull (NonNull)
  10 import Data.Proxy
  11 import Data.Text (Text)
  12 import Data.Type.Equality
  13 import GHC.Exts (Constraint)
  14 import qualified System.IO as IO
  15
  16 import Language.Symantic.Lib.Data.Type.List
  17 import Language.Symantic.Lib.Data.Type.Peano
  18 import Language.Symantic.Typing.Kind
  19
  20 -- * Type 'Const'
  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 Const (cs::[Kind.Type]) (c::k) where
  26         ConstZ :: SKind k -> Const (Proxy c ': cs) (c::k)
  27         ConstS :: Const cs c -> Const (not_c ': cs) c
  28 infixr 5 `ConstS`
  29
  30 eq_kind_const :: Const cs (x::kx) -> Const cs (y::ky) -> Maybe (kx:~:ky)
  31 eq_kind_const x y = eq_skind (kind_of_const x) (kind_of_const y)
  32
  33 instance TestEquality (Const cs) where
  34         testEquality ConstZ{} ConstZ{}     = Just Refl
  35         testEquality (ConstS x) (ConstS y) = testEquality x y
  36         testEquality _ _                   = Nothing
  37
  38 kind_of_const :: Const cs (h::k) -> SKind k
  39 kind_of_const (ConstZ ki) = ki
  40 kind_of_const (ConstS c)  = kind_of_const c
  41
  42 -- * Type 'Inj_Const'
  43 -- | Convenient type synonym wrapping 'Inj_ConstP'
  44 -- applied on the correct 'Index'.
  45 type Inj_Const cs c = Inj_ConstP (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_const :: forall cs c. Inj_Const cs c => Const cs c
  50 inj_const = inj_constP (Proxy::Proxy (Index cs (Proxy c)))
  51
  52 -- ** Class 'Inj_ConstP'
  53 class Inj_ConstP p cs c where
  54         inj_constP :: Proxy p -> Const 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_ConstP Zero (Proxy c ': cs) (c::k) where
  59         inj_constP _ = ConstZ kind
  60 -}
  61 instance
  62  ( IKindP (Ty_of_Type k)
  63  , Type_of_Ty (Ty_of_Type k) ~ k
  64  ) => Inj_ConstP Zero (Proxy c ': cs) (c::k) where
  65         inj_constP _ = ConstZ (kindP (Proxy :: Proxy (Ty_of_Type k)))
  66 instance Inj_ConstP p cs c => Inj_ConstP (Succ p) (not_c ': cs) c where
  67         inj_constP _p = ConstS (inj_constP (Proxy::Proxy p))
  68
  69 -- * Class 'Proj_Const'
  70 -- | Convenient type synonym wrapping 'Proj_ConstP'
  71 -- applied on the correct 'Index'.
  72 type Proj_Const cs c = Proj_ConstP (Index cs (Proxy c)) cs c
  73
  74 -- | Project a 'Const' onto a Haskell type level /type constant/ @c@,
  75 -- returning a proof that the 'Const' indexes @c@ iif. it's the case.
  76 proj_const :: forall cs k (c::k) (u::k).
  77  Proj_Const cs c => Const cs u -> Proxy c -> Maybe (c :~: u)
  78 proj_const = proj_constP (Proxy::Proxy (Index cs (Proxy c)))
  79
  80 (=?) :: forall cs c u. Proj_Const cs c => Const cs u -> Proxy c -> Maybe (c :~: u)
  81 (=?) = proj_constP (Proxy::Proxy (Index cs (Proxy c)))
  82
  83 -- ** Type 'Proj_ConstP'
  84 class Proj_ConstP p cs c where
  85         proj_constP :: Proxy p -> Const cs u -> Proxy c -> Maybe (c :~: u)
  86 instance Proj_ConstP Zero (Proxy c ': cs) c where
  87         proj_constP _p ConstZ{} _c = Just Refl
  88         proj_constP _p ConstS{} _c = Nothing
  89 instance Proj_ConstP p cs c => Proj_ConstP (Succ p) (not_c ': cs) c where
  90         proj_constP _p ConstZ{} _c  = Nothing
  91         proj_constP _p (ConstS u) c = proj_constP (Proxy::Proxy p) u c
  92
  93 -- ** Type 'Proj_Consts'
  94 type Proj_Consts cs cs_to_proj
  95  = Concat_Constraints (Proj_ConstsR cs cs_to_proj)
  96
  97 -- *** Type family 'Proj_ConstsR'
  98 type family Proj_ConstsR cs cs_to_proj :: [Constraint] where
  99  Proj_ConstsR cs '[] = '[]
 100  Proj_ConstsR cs (Proxy x ': xs) = Proj_Const cs x ': Proj_ConstsR cs xs
 101
 102 -- * Class 'Const_from'
 103 -- | Try to build a 'Const' from raw data.
 104 class Const_from raw cs where
 105         const_from
 106          :: raw -> (forall k c. Const cs (c::k) -> Maybe ret)
 107          -> Maybe ret
 108
 109 instance Const_from raw '[] where
 110         const_from _c _k = Nothing
 111
 112 -- TODO: move each of these to a dedicated module.
 113 instance Const_from Text cs => Const_from Text (Proxy Bounded ': cs) where
 114         const_from "Bounded" k = k (ConstZ kind)
 115         const_from s k = const_from s $ k . ConstS
 116 instance Const_from Text cs => Const_from Text (Proxy Enum ': cs) where
 117         const_from "Enum" k = k (ConstZ kind)
 118         const_from s k = const_from s $ k . ConstS
 119 instance Const_from Text cs => Const_from Text (Proxy Fractional ': cs) where
 120         const_from "Fractional" k = k (ConstZ kind)
 121         const_from s k = const_from s $ k . ConstS
 122 instance Const_from Text cs => Const_from Text (Proxy Real ': cs) where
 123         const_from "Real" k = k (ConstZ kind)
 124         const_from s k = const_from s $ k . ConstS
 125
 126 -- * Class 'Show_Const'
 127 class Show_Const cs where
 128         show_const :: Const cs c -> String
 129
 130 -- deriving instance Show (Const cs c)
 131 instance Show_Const cs => Show (Const cs c) where
 132         show = show_const
 133 instance Show_Const '[] where
 134         show_const = error "Show_Const unreachable pattern"
 135
 136 -- TODO: move each of these to a dedicated module.
 137 instance Show_Const cs => Show_Const (Proxy Bounded ': cs) where
 138         show_const ConstZ{} = "Bounded"
 139         show_const (ConstS c) = show_const c
 140 instance Show_Const cs => Show_Const (Proxy Enum ': cs) where
 141         show_const ConstZ{} = "Enum"
 142         show_const (ConstS c) = show_const c
 143 instance Show_Const cs => Show_Const (Proxy Fractional ': cs) where
 144         show_const ConstZ{} = "Fractional"
 145         show_const (ConstS c) = show_const c
 146 instance Show_Const cs => Show_Const (Proxy Real ': cs) where
 147         show_const ConstZ{} = "Real"
 148         show_const (ConstS c) = show_const c
 149
 150 -- * Type 'Constants'
 151 -- | Usual 'Const's.
 152 type Constants = Terms ++ Constraints
 153
 154 -- ** Type 'Terms'
 155 -- | Usual 'Const's of /terms constructors/.
 156 type Terms =
 157  [ Proxy ()
 158  , Proxy (,)
 159  , Proxy (->)
 160  , Proxy []
 161  , Proxy Bool
 162  , Proxy Char
 163  , Proxy Either
 164  , Proxy Int
 165  , Proxy Integer
 166  , Proxy Integral
 167  , Proxy IO
 168  , Proxy IO.Handle
 169  , Proxy IO.IOMode
 170  , Proxy Map.Map
 171  , Proxy Maybe
 172  , Proxy NonNull
 173  , Proxy Text
 174  ]
 175
 176 -- ** Type 'Constraints'
 177 -- | Usual 'Const's of /type constraint constructors/.
 178 type Constraints =
 179  [ Proxy Applicative
 180  , Proxy Bounded
 181  , Proxy Enum
 182  , Proxy Eq
 183  , Proxy Foldable
 184  , Proxy Functor
 185  , Proxy Monad
 186  , Proxy Monoid
 187  , Proxy MT.MonoFoldable
 188  , Proxy MT.MonoFunctor
 189  , Proxy Num
 190  , Proxy Ord
 191  , Proxy Real
 192  , Proxy Seqs.IsSequence
 193  , Proxy Seqs.SemiSequence
 194  , Proxy Show
 195  , Proxy Traversable
 196  ]