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