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