Language/Symantic/Typing/Constant.hs

   1 {-# LANGUAGE DataKinds #-}
   2 {-# LANGUAGE ConstraintKinds #-}
   3 {-# LANGUAGE FlexibleContexts #-}
   4 {-# LANGUAGE FlexibleInstances #-}
   5 {-# LANGUAGE GADTs #-}
   6 {-# LANGUAGE MultiParamTypeClasses #-}
   7 {-# LANGUAGE PolyKinds #-}
   8 {-# LANGUAGE Rank2Types #-}
   9 {-# LANGUAGE ScopedTypeVariables #-}
  10 {-# LANGUAGE TypeFamilies #-}
  11 {-# LANGUAGE TypeOperators #-}
  12 {-# LANGUAGE UndecidableInstances #-}
  13 module Language.Symantic.Typing.Constant where
  14
  15 import Data.Proxy
  16 import Data.Type.Equality
  17 import GHC.Prim (Constraint)
  18
  19 import Language.Symantic.Lib.Data.Peano
  20 import Language.Symantic.Typing.Kind
  21
  22 -- * Type 'Const'
  23 -- | A /type constant/,
  24 -- indexed at the Haskell type and term level amongst a list of them.
  25 -- When used, @c@ is actually wrapped within a 'Proxy'
  26 -- to be able to handle constants of different 'Kind's.
  27 data Const (cs::[*]) (c:: *) where
  28         ConstZ :: SKind (Kind_of_Proxy c) -> Const (c ': cs) c
  29         ConstS :: Const cs c -> Const (not_c ': cs) c
  30 infixr 5 `ConstS`
  31
  32 instance TestEquality (Const cs) where
  33         testEquality ConstZ{} ConstZ{}     = Just Refl
  34         testEquality (ConstS x) (ConstS y) = testEquality x y
  35         testEquality _ _                   = Nothing
  36
  37 kind_of_const :: Const cs h -> SKind (Kind_of_Proxy h)
  38 kind_of_const (ConstZ ki) = ki
  39 kind_of_const (ConstS c)  = kind_of_const c
  40
  41 -- ** Type 'Const_of'
  42 -- | Convenient type synonym.
  43 type Const_of cs c = Const cs (Proxy c)
  44
  45 -- ** Type 'ConstP'
  46 -- | Return the position of a 'Const' within a list of them.
  47 -- This is useful to work around @OverlappingInstances@
  48 -- in 'Inj_ConstP' and 'Proj_ConstP'.
  49 type family ConstP cs c where
  50         ConstP (c  ': cs) c = Zero
  51         ConstP (nc ': cs) c = Succ (ConstP cs c)
  52
  53 -- ** Type 'Inj_Const'
  54 -- | Convenient type synonym wrapping 'Inj_ConstP'
  55 -- applied on the correct 'ConstP'.
  56 type Inj_Const cs c = Inj_ConstP (ConstP cs (Proxy c)) cs (Proxy c)
  57
  58 -- | Inject a given /type constant/ @c@ into a list of them,
  59 -- by returning a proof that 'Proxy'@ c@ is in @cs@.
  60 inj_const :: forall cs c. Inj_Const cs c => Const cs (Proxy c)
  61 inj_const = inj_constP (Proxy::Proxy (ConstP cs (Proxy c)))
  62
  63 -- ** Class 'Inj_ConstP'
  64 class Inj_ConstP p cs c where
  65         inj_constP :: Proxy p -> Const cs c
  66 instance IKind (Kind_of_Proxy c) => Inj_ConstP Zero (c ': cs) c where
  67         inj_constP _ = ConstZ kind
  68 instance Inj_ConstP p cs c => Inj_ConstP (Succ p) (not_c ': cs) c where
  69         inj_constP _p = ConstS (inj_constP (Proxy::Proxy p))
  70
  71 -- ** Class 'Proj_Const'
  72 -- | Convenient class synonym wrapping 'Proj_ConstP'
  73 -- applied on the correct 'ConstP'.
  74 --
  75 -- NOTE: using a /class synonym/ instead of a /type synonym/
  76 -- allows to use it partially applied, which is useful in 'Map_Consts'.
  77 class    Proj_ConstP (ConstP cs c) cs c => Proj_Const cs c
  78 instance Proj_ConstP (ConstP cs c) cs c => Proj_Const cs c
  79 -- type Proj_Const cs c = Proj_ConstP (ConstP cs c) cs c
  80
  81 -- | Project a 'Const' onto a Haskell type level /type constant/ @c@,
  82 -- returning a proof that the 'Const' indexes @c@ iif. it's the case.
  83 proj_const :: forall cs c u. Proj_Const cs c => Const cs u -> c -> Maybe (c :~: u)
  84 proj_const = proj_constP (Proxy::Proxy (ConstP cs c))
  85
  86 (=?) :: forall cs c u. Proj_Const cs c => Const cs u -> c -> Maybe (c :~: u)
  87 (=?) = proj_constP (Proxy::Proxy (ConstP cs c))
  88
  89 -- *** Type 'Proj_ConstP'
  90 class Proj_ConstP p cs c where
  91         proj_constP :: Proxy p -> Const cs u -> c -> Maybe (c :~: u)
  92 instance Proj_ConstP Zero (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 rs cs = Concat_Constraints (Map_Consts (Proj_Const rs) cs)
 101
 102 -- * Type 'Consts'
 103 -- | Usual 'Const's.
 104 type Consts = Terms ++ Constraints
 105
 106 -- ** Type 'Terms'
 107 -- | Usual 'Const's of /terms constructors/.
 108 type Terms =
 109  [ Proxy []
 110  , Proxy (->)
 111  , Proxy Bool
 112  , Proxy Int
 113  , Proxy Integral
 114  , Proxy IO
 115  , Proxy Maybe
 116  ]
 117
 118 -- ** Type 'Constraints'
 119 -- | Usual 'Const's of /type constraint constructors/.
 120 type Constraints =
 121  [ Proxy Applicative
 122  , Proxy Bounded
 123  , Proxy Enum
 124  , Proxy Eq
 125  , Proxy Foldable
 126  , Proxy Functor
 127  , Proxy Monad
 128  , Proxy Monoid
 129  , Proxy Num
 130  , Proxy Ord
 131  , Proxy Real
 132  , Proxy Traversable
 133  ]
 134
 135 -- * Class 'Const_from'
 136 -- | Try to build a 'Const' from raw data.
 137 class Const_from raw cs where
 138         const_from
 139          :: raw -> (forall c. Const cs c -> Maybe ret)
 140          -> Maybe ret
 141
 142 instance Const_from raw '[] where
 143         const_from _c _k = Nothing
 144
 145 instance Const_from String cs => Const_from String (Proxy [] ': cs) where
 146         const_from "[]" k = k (ConstZ kind)
 147         const_from s k = const_from s $ k . ConstS
 148 instance Const_from String cs => Const_from String (Proxy (->) ': cs) where
 149         const_from "(->)" k = k (ConstZ kind)
 150         const_from s k = const_from s $ k . ConstS
 151 instance Const_from String cs => Const_from String (Proxy Applicative ': cs) where
 152         const_from "Applicative" k = k (ConstZ kind)
 153         const_from s k = const_from s $ k . ConstS
 154 instance Const_from String cs => Const_from String (Proxy Bool ': cs) where
 155         const_from "Bool" k = k (ConstZ kind)
 156         const_from s k = const_from s $ k . ConstS
 157 instance Const_from String cs => Const_from String (Proxy Bounded ': cs) where
 158         const_from "Bounded" k = k (ConstZ kind)
 159         const_from s k = const_from s $ k . ConstS
 160 instance Const_from String cs => Const_from String (Proxy Char ': cs) where
 161         const_from "Char" k = k (ConstZ kind)
 162         const_from s k = const_from s $ k . ConstS
 163 instance Const_from String cs => Const_from String (Proxy Eq ': cs) where
 164         const_from "Eq" k = k (ConstZ kind)
 165         const_from s k = const_from s $ k . ConstS
 166 instance Const_from String cs => Const_from String (Proxy Enum ': cs) where
 167         const_from "Enum" k = k (ConstZ kind)
 168         const_from s k = const_from s $ k . ConstS
 169 instance Const_from String cs => Const_from String (Proxy Foldable ': cs) where
 170         const_from "Foldable" k = k (ConstZ kind)
 171         const_from s k = const_from s $ k . ConstS
 172 instance Const_from String cs => Const_from String (Proxy Fractional ': cs) where
 173         const_from "Fractional" k = k (ConstZ kind)
 174         const_from s k = const_from s $ k . ConstS
 175 instance Const_from String cs => Const_from String (Proxy Functor ': cs) where
 176         const_from "Functor" k = k (ConstZ kind)
 177         const_from s k = const_from s $ k . ConstS
 178 instance Const_from String cs => Const_from String (Proxy Int ': cs) where
 179         const_from "Int" k = k (ConstZ kind)
 180         const_from s k = const_from s $ k . ConstS
 181 instance Const_from String cs => Const_from String (Proxy Integer ': cs) where
 182         const_from "Integer" k = k (ConstZ kind)
 183         const_from s k = const_from s $ k . ConstS
 184 instance Const_from String cs => Const_from String (Proxy Integral ': cs) where
 185         const_from "Integral" k = k (ConstZ kind)
 186         const_from s k = const_from s $ k . ConstS
 187 instance Const_from String cs => Const_from String (Proxy IO ': cs) where
 188         const_from "IO" k = k (ConstZ kind)
 189         const_from s k = const_from s $ k . ConstS
 190 instance Const_from String cs => Const_from String (Proxy Maybe ': cs) where
 191         const_from "Maybe" k = k (ConstZ kind)
 192         const_from s k = const_from s $ k . ConstS
 193 instance Const_from String cs => Const_from String (Proxy Monad ': cs) where
 194         const_from "Monad" k = k (ConstZ kind)
 195         const_from s k = const_from s $ k . ConstS
 196 instance Const_from String cs => Const_from String (Proxy Monoid ': cs) where
 197         const_from "Monoid" k = k (ConstZ kind)
 198         const_from s k = const_from s $ k . ConstS
 199 instance Const_from String cs => Const_from String (Proxy Num ': cs) where
 200         const_from "Num" k = k (ConstZ kind)
 201         const_from s k = const_from s $ k . ConstS
 202 instance Const_from String cs => Const_from String (Proxy Ord ': cs) where
 203         const_from "Ord" k = k (ConstZ kind)
 204         const_from s k = const_from s $ k . ConstS
 205 instance Const_from String cs => Const_from String (Proxy Real ': cs) where
 206         const_from "Real" k = k (ConstZ kind)
 207         const_from s k = const_from s $ k . ConstS
 208 instance Const_from String cs => Const_from String (Proxy Traversable ': cs) where
 209         const_from "Traversable" k = k (ConstZ kind)
 210         const_from s k = const_from s $ k . ConstS
 211
 212 -- * Class 'Show_Const'
 213 class Show_Const cs where
 214         show_const :: Const cs c -> String
 215
 216 instance Show_Const cs => Show (Const cs c) where
 217         show = show_const
 218 instance Show_Const '[] where
 219         show_const = error "Show_Const unreachable pattern"
 220
 221 instance Show_Const cs => Show_Const (Proxy [] ': cs) where
 222         show_const ConstZ{} = "[]"
 223         show_const (ConstS c) = show_const c
 224 instance Show_Const cs => Show_Const (Proxy (->) ': cs) where
 225         show_const ConstZ{} = "(->)"
 226         show_const (ConstS c) = show_const c
 227 instance Show_Const cs => Show_Const (Proxy Applicative ': cs) where
 228         show_const ConstZ{} = "Applicative"
 229         show_const (ConstS c) = show_const c
 230 instance Show_Const cs => Show_Const (Proxy Bool ': cs) where
 231         show_const ConstZ{} = "Bool"
 232         show_const (ConstS c) = show_const c
 233 instance Show_Const cs => Show_Const (Proxy Bounded ': cs) where
 234         show_const ConstZ{} = "Bounded"
 235         show_const (ConstS c) = show_const c
 236 instance Show_Const cs => Show_Const (Proxy Char ': cs) where
 237         show_const ConstZ{} = "Char"
 238         show_const (ConstS c) = show_const c
 239 instance Show_Const cs => Show_Const (Proxy Enum ': cs) where
 240         show_const ConstZ{} = "Enum"
 241         show_const (ConstS c) = show_const c
 242 instance Show_Const cs => Show_Const (Proxy Eq ': cs) where
 243         show_const ConstZ{} = "Eq"
 244         show_const (ConstS c) = show_const c
 245 instance Show_Const cs => Show_Const (Proxy Foldable ': cs) where
 246         show_const ConstZ{} = "Foldable"
 247         show_const (ConstS c) = show_const c
 248 instance Show_Const cs => Show_Const (Proxy Fractional ': cs) where
 249         show_const ConstZ{} = "Fractional"
 250         show_const (ConstS c) = show_const c
 251 instance Show_Const cs => Show_Const (Proxy Functor ': cs) where
 252         show_const ConstZ{} = "Functor"
 253         show_const (ConstS c) = show_const c
 254 instance Show_Const cs => Show_Const (Proxy Int ': cs) where
 255         show_const ConstZ{} = "Int"
 256         show_const (ConstS c) = show_const c
 257 instance Show_Const cs => Show_Const (Proxy Integer ': cs) where
 258         show_const ConstZ{} = "Integer"
 259         show_const (ConstS c) = show_const c
 260 instance Show_Const cs => Show_Const (Proxy Integral ': cs) where
 261         show_const ConstZ{} = "Integral"
 262         show_const (ConstS c) = show_const c
 263 instance Show_Const cs => Show_Const (Proxy IO ': cs) where
 264         show_const ConstZ{} = "IO"
 265         show_const (ConstS c) = show_const c
 266 instance Show_Const cs => Show_Const (Proxy Maybe ': cs) where
 267         show_const ConstZ{} = "Maybe"
 268         show_const (ConstS c) = show_const c
 269 instance Show_Const cs => Show_Const (Proxy Monad ': cs) where
 270         show_const ConstZ{} = "Monad"
 271         show_const (ConstS c) = show_const c
 272 instance Show_Const cs => Show_Const (Proxy Monoid ': cs) where
 273         show_const ConstZ{} = "Monoid"
 274         show_const (ConstS c) = show_const c
 275 instance Show_Const cs => Show_Const (Proxy Num ': cs) where
 276         show_const ConstZ{} = "Num"
 277         show_const (ConstS c) = show_const c
 278 instance Show_Const cs => Show_Const (Proxy Ord ': cs) where
 279         show_const ConstZ{} = "Ord"
 280         show_const (ConstS c) = show_const c
 281 instance Show_Const cs => Show_Const (Proxy Real ': cs) where
 282         show_const ConstZ{} = "Real"
 283         show_const (ConstS c) = show_const c
 284 instance Show_Const cs => Show_Const (Proxy Traversable ': cs) where
 285         show_const ConstZ{} = "Traversable"
 286         show_const (ConstS c) = show_const c
 287
 288 -- * Type family @(++)@
 289 type family (++) xs ys where
 290         '[] ++ ys = ys
 291         (x ': xs) ++ ys = x ': xs ++ ys
 292 infixr 5 ++
 293
 294 -- * Type family 'Concat_Constraints'
 295 type family Concat_Constraints (cs::[Constraint]) :: Constraint where
 296         Concat_Constraints '[] = ()
 297         Concat_Constraints (c ': cs) = (c, Concat_Constraints cs)
 298
 299 -- * Type family 'Map_Consts'
 300 type family Map_Consts (f:: * -> k) (cs::[*]) :: [k] where
 301         Map_Consts f '[] = '[]
 302         Map_Consts f (c ': cs) = f c ': Map_Consts f cs
 303