Language/Symantic/Typing/Constant.hs

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