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.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 @(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 @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 @(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 @(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 @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 where
  99  Proj_ConstsR cs '[] = '[]
 100  Proj_ConstsR cs (Proxy x ': xs) = Proj_Const cs x ': Proj_ConstsR cs xs
 101
 102 -- * Class 'Show_Const'
 103 class Show_Const cs where
 104         show_const :: Const cs c -> String
 105
 106 -- deriving instance Show (Const cs c)
 107 instance Show_Const cs => Show (Const cs c) where
 108         show = show_const
 109 instance Show_Const '[] where
 110         show_const = error "Show_Const unreachable pattern"
 111
 112 -- TODO: move each of these to a dedicated module.
 113 instance Show_Const cs => Show_Const (Proxy Bounded ': cs) where
 114         show_const ConstZ{} = "Bounded"
 115         show_const (ConstS c) = show_const c
 116 instance Show_Const cs => Show_Const (Proxy Enum ': cs) where
 117         show_const ConstZ{} = "Enum"
 118         show_const (ConstS c) = show_const c
 119 instance Show_Const cs => Show_Const (Proxy Fractional ': cs) where
 120         show_const ConstZ{} = "Fractional"
 121         show_const (ConstS c) = show_const c
 122 instance Show_Const cs => Show_Const (Proxy Real ': cs) where
 123         show_const ConstZ{} = "Real"
 124         show_const (ConstS c) = show_const c
 125
 126 -- * Type 'Constants'
 127 -- | Usual 'Const's.
 128 type Constants = Terms ++ Constraints
 129
 130 -- ** Type 'Terms'
 131 -- | Usual 'Const's of /terms constructors/.
 132 type 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 'Constraints'
 153 -- | Usual 'Const's of /type constraint constructors/.
 154 type 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  ]