{-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE TypeInType #-} module Language.Symantic.Typing.Constant where import qualified Data.Kind as Kind import qualified Data.Map.Strict as Map import qualified Data.MonoTraversable as MT import qualified Data.Sequences as Seqs import Data.NonNull (NonNull) import Data.Proxy import Data.Text (Text) import Data.Type.Equality import GHC.Exts (Constraint) import qualified System.IO as IO import Language.Symantic.Lib.Data.Type.List import Language.Symantic.Lib.Data.Type.Peano import Language.Symantic.Typing.Kind -- * Type 'Const' -- | A /type constant/, -- indexed at the Haskell type and term level amongst a list of them. -- When used, @c@ is actually wrapped within a 'Proxy' -- to be able to handle constants of different 'Kind's. data Const (cs::[Kind.Type]) (c::k) where ConstZ :: SKind k -> Const (Proxy c ': cs) (c::k) ConstS :: Const cs c -> Const (not_c ': cs) c infixr 5 `ConstS` eq_kind_const :: Const cs (x::kx) -> Const cs (y::ky) -> Maybe (kx:~:ky) eq_kind_const x y = eq_skind (kind_of_const x) (kind_of_const y) instance TestEquality (Const cs) where testEquality ConstZ{} ConstZ{} = Just Refl testEquality (ConstS x) (ConstS y) = testEquality x y testEquality _ _ = Nothing kind_of_const :: Const cs (h::k) -> SKind k kind_of_const (ConstZ ki) = ki kind_of_const (ConstS c) = kind_of_const c -- * Type 'Inj_Const' -- | Convenient type synonym wrapping 'Inj_ConstP' -- applied on the correct 'Index'. type Inj_Const cs c = Inj_ConstP (Index cs (Proxy c)) cs c -- | Inject a given /type constant/ @c@ into a list of them, -- by returning a proof that 'Proxy'@ c@ is in @cs@. inj_const :: forall cs c. Inj_Const cs c => Const cs c inj_const = inj_constP (Proxy::Proxy (Index cs (Proxy c))) -- ** Class 'Inj_ConstP' class Inj_ConstP p cs c where inj_constP :: Proxy p -> Const cs c {- NOTE: using this commented instance fails very badly due to GHC-8.0.1's bug #12933 which makes it fail to calculate the right kind, it seems to wrongly reuse the kind of the first use (sic)… instance IKind k => Inj_ConstP Zero (Proxy c ': cs) (c::k) where inj_constP _ = ConstZ kind -} instance ( IKindP (Ty_of_Type k) , Type_of_Ty (Ty_of_Type k) ~ k ) => Inj_ConstP Zero (Proxy c ': cs) (c::k) where inj_constP _ = ConstZ (kindP (Proxy :: Proxy (Ty_of_Type k))) instance Inj_ConstP p cs c => Inj_ConstP (Succ p) (not_c ': cs) c where inj_constP _p = ConstS (inj_constP (Proxy::Proxy p)) -- * Class 'Proj_Const' -- | Convenient type synonym wrapping 'Proj_ConstP' -- applied on the correct 'Index'. type Proj_Const cs c = Proj_ConstP (Index cs (Proxy c)) cs c -- | Project a 'Const' onto a Haskell type level /type constant/ @c@, -- returning a proof that the 'Const' indexes @c@ iif. it's the case. proj_const :: forall cs k (c::k) (u::k). Proj_Const cs c => Const cs u -> Proxy c -> Maybe (c :~: u) proj_const = proj_constP (Proxy::Proxy (Index cs (Proxy c))) (=?) :: forall cs c u. Proj_Const cs c => Const cs u -> Proxy c -> Maybe (c :~: u) (=?) = proj_constP (Proxy::Proxy (Index cs (Proxy c))) -- ** Type 'Proj_ConstP' class Proj_ConstP p cs c where proj_constP :: Proxy p -> Const cs u -> Proxy c -> Maybe (c :~: u) instance Proj_ConstP Zero (Proxy c ': cs) c where proj_constP _p ConstZ{} _c = Just Refl proj_constP _p ConstS{} _c = Nothing instance Proj_ConstP p cs c => Proj_ConstP (Succ p) (not_c ': cs) c where proj_constP _p ConstZ{} _c = Nothing proj_constP _p (ConstS u) c = proj_constP (Proxy::Proxy p) u c -- ** Type 'Proj_Consts' type Proj_Consts cs cs_to_proj = Concat_Constraints (Proj_ConstsR cs cs_to_proj) -- *** Type family 'Proj_ConstsR' type family Proj_ConstsR cs cs_to_proj :: [Constraint] where Proj_ConstsR cs '[] = '[] Proj_ConstsR cs (Proxy x ': xs) = Proj_Const cs x ': Proj_ConstsR cs xs -- * Class 'Show_Const' class Show_Const cs where show_const :: Const cs c -> String -- deriving instance Show (Const cs c) instance Show_Const cs => Show (Const cs c) where show = show_const instance Show_Const '[] where show_const = error "Show_Const unreachable pattern" -- TODO: move each of these to a dedicated module. instance Show_Const cs => Show_Const (Proxy Bounded ': cs) where show_const ConstZ{} = "Bounded" show_const (ConstS c) = show_const c instance Show_Const cs => Show_Const (Proxy Enum ': cs) where show_const ConstZ{} = "Enum" show_const (ConstS c) = show_const c instance Show_Const cs => Show_Const (Proxy Fractional ': cs) where show_const ConstZ{} = "Fractional" show_const (ConstS c) = show_const c instance Show_Const cs => Show_Const (Proxy Real ': cs) where show_const ConstZ{} = "Real" show_const (ConstS c) = show_const c -- * Type 'Constants' -- | Usual 'Const's. type Constants = Terms ++ Constraints -- ** Type 'Terms' -- | Usual 'Const's of /terms constructors/. type Terms = [ Proxy () , Proxy (,) , Proxy (->) , Proxy [] , Proxy Bool , Proxy Char , Proxy Either , Proxy Int , Proxy Integer , Proxy Integral , Proxy IO , Proxy IO.Handle , Proxy IO.IOMode , Proxy Map.Map , Proxy Maybe , Proxy NonNull , Proxy Text ] -- ** Type 'Constraints' -- | Usual 'Const's of /type constraint constructors/. type Constraints = [ Proxy Applicative , Proxy Bounded , Proxy Enum , Proxy Eq , Proxy Foldable , Proxy Functor , Proxy Monad , Proxy Monoid , Proxy MT.MonoFoldable , Proxy MT.MonoFunctor , Proxy Num , Proxy Ord , Proxy Real , Proxy Seqs.IsSequence , Proxy Seqs.SemiSequence , Proxy Show , Proxy Traversable ]