symantic/Language/Symantic/Typing/Type.hs

   1 {-# LANGUAGE ConstraintKinds #-}
   2 {-# LANGUAGE GADTs #-}
   3 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
   4 {-# LANGUAGE TypeInType #-}
   5 {-# LANGUAGE UndecidableInstances #-}
   6 {-# LANGUAGE ViewPatterns #-}
   7 {-# OPTIONS_GHC -fno-warn-orphans #-}
   8 module Language.Symantic.Typing.Type where
   9
  10 import Control.Applicative (Applicative(..))
  11 import qualified Data.Char as Char
  12 import Data.Monoid ((<>))
  13 import Data.Proxy
  14 import Data.Maybe (fromMaybe, isJust)
  15 import Data.String (IsString(..))
  16 import Data.Text (Text)
  17 import qualified Data.Text as Text
  18 import Data.Type.Equality
  19 import qualified Data.Kind as K
  20
  21 import Language.Symantic.Typing.Kind
  22 import Language.Symantic.Typing.Constant
  23 import Language.Symantic.Parsing
  24
  25 -- * Type 'Type'
  26
  27 -- | /Type of terms/.
  28 --
  29 -- * @cs@: /type constants/, fixed at compile time.
  30 -- * @h@: indexed Haskell type.
  31 --
  32 -- * 'TyConst': /type constant/, selected amongst @cs@.
  33 -- * @(:$)@: /type application/.
  34 --
  35 -- See also: https://ghc.haskell.org/trac/ghc/wiki/Typeable
  36 -- Which currently concludes:
  37 -- "Why kind equalities, then? Given the fact that Richard's branch
  38 -- doesn't solve this problem, what is it good for?
  39 -- It still works wonders in the mono-kinded case,
  40 -- such as for decomposing ->.
  41 -- It's just that poly-kinded constructors are still a pain."
  42 data Type (cs::[K.Type]) (h::k) where
  43         TyConst :: TyConst cs c -> Type cs c
  44         (:$) :: Type cs f -> Type cs x -> Type cs (f x)
  45         -- TODO: TyVar :: SKind k -> Type cs (v::k)
  46 infixl 9 :$
  47
  48 -- | 'Type' constructor to be used
  49 -- with @TypeApplications@
  50 -- and @NoMonomorphismRestriction@.
  51 ty :: forall c cs. Inj_TyConst cs c => Type cs c
  52 ty = TyConst inj_TyConst
  53  -- NOTE: The forall brings @c@ first in the type variables,
  54  -- which is convenient to use @TypeApplications@.
  55
  56 instance TestEquality (Type cs) where
  57         testEquality = eq_Type
  58 instance Eq (Type cs h) where
  59         _x == _y = True
  60 instance Show_TyConst cs => Show (Type cs h) where
  61         show = show_Type
  62 -- deriving instance Show_TyConst cs => Show (Type cs h)
  63
  64 kind_of :: Type cs (h::k) -> SKind k
  65 kind_of t =
  66         case t of
  67          TyConst c -> kind_of_TyConst c
  68          f :$ _x ->
  69                 case kind_of f of
  70                  _kx `SKiArrow` kf -> kf
  71
  72 eq_Type
  73  :: Type cs (x::k) -> Type cs (y::k) -> Maybe (x:~:y)
  74 eq_Type (TyConst x) (TyConst y)
  75  | Just Refl <- testEquality x y
  76  = Just Refl
  77 eq_Type (xf :$ xx) (yf :$ yx)
  78  | Just Refl <- eq_skind (kind_of xf) (kind_of yf)
  79  , Just Refl <- eq_Type xf yf
  80  , Just Refl <- eq_Type xx yx
  81  = Just Refl
  82 eq_Type _ _ = Nothing
  83
  84 eq_Kind_Type
  85  :: Type cs (x::kx) -> Type cs (y::ky) -> Maybe (kx:~:ky)
  86 eq_Kind_Type (TyConst x) (TyConst y)
  87  | Just Refl <- eq_Kind_TyConst x y
  88  = Just Refl
  89 eq_Kind_Type (xf :$ xx) (yf :$ yx)
  90  | Just Refl <- eq_Kind_Type xf yf
  91  , Just Refl <- eq_Kind_Type xx yx
  92  = Just Refl
  93 eq_Kind_Type _x _y = Nothing
  94
  95 show_Type :: Show_TyConst cs => Type cs h -> String
  96 show_Type (TyConst c) = show c
  97 show_Type (f@(:$){} :$ a@(:$){}) = "(" <> show_Type f <> ") (" <> show_Type a <> ")"
  98 show_Type (f@(:$){} :$ a) = "(" <> show_Type f <> ") " <> show_Type a
  99 show_Type (f :$ a@(:$){}) = show_Type f <> " (" <> show_Type a <> ")"
 100 show_Type (f :$ a) = show_Type f <> " " <> show_Type a
 101 -- show_Type (TyVar v) = "t" <> show (integral_from_peano v::Integer)
 102
 103 -- | Cons a @new_c@ to @cs@.
 104 lift_Type :: Type cs c -> Type (new_c ': cs) c
 105 lift_Type (TyConst c) = TyConst (TyConstS c)
 106 lift_Type (f :$ a) = lift_Type f :$ lift_Type a
 107
 108 -- * Type 'EType'
 109 -- | Existential for 'Type'.
 110 data EType cs = forall h. EType (Type cs h)
 111
 112 instance Eq (EType cs) where
 113         EType x == EType y
 114          | Just Refl <- eq_Kind_Type x y
 115          = isJust $ eq_Type x y
 116         _x == _y = False
 117 instance Show_TyConst cs => Show (EType cs) where
 118         show (EType t) = show t
 119
 120 -- * Type 'KType'
 121 -- | Existential for 'Type' of a known 'Kind'.
 122 data KType cs k = forall (h::k). KType (Type cs h)
 123
 124 instance Eq (KType cs ki) where
 125         KType x == KType y = isJust $ eq_Type x y
 126 instance Show_TyConst cs => Show (KType cs ki) where
 127         show (KType t) = show_Type t
 128
 129 -- * Type 'Token_Type'
 130 type Token_Type = Type '[] ()
 131
 132 -- * Type 'TyName'
 133 newtype TyName = TyName Text
 134  deriving (Eq, Ord, Show)
 135 instance IsString TyName where
 136         fromString = TyName . fromString
 137
 138 data instance TokenT meta ts (Proxy Token_Type)
 139  = Token_Type TyName [EToken meta ts]
 140 deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy Token_Type))
 141 deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy Token_Type))
 142
 143 instance
 144  ( Read_TyNameR TyName cs rs
 145  , Inj_TyConst cs Token_Type
 146  ) => Read_TyNameR TyName cs (Proxy Token_Type ': rs) where
 147         read_TyNameR _rs (TyName "Type") k = k (ty @Token_Type)
 148         read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
 149 instance Show_TyConst cs => Show_TyConst (Proxy Token_Type ': cs) where
 150         show_TyConst TyConstZ{} = "Type"
 151         show_TyConst (TyConstS c) = show_TyConst c
 152
 153 -- * Class 'Compile_Type'
 154 -- | Try to build a 'Type' from name data.
 155 class Compile_Type ts cs where
 156         compile_Type
 157          :: ( MonoLift (Error_Type meta ts) err
 158             , MonoLift (Con_Kind meta ts) err )
 159          => EToken meta ts
 160          -> (forall k h. Type cs (h::k) -> Either err ret)
 161          -> Either err ret
 162
 163 compile_EType
 164  :: Read_TyName TyName cs
 165  => EToken meta '[Proxy Token_Type]
 166  -> Either (Error_Type meta '[Proxy Token_Type]) (EType cs)
 167 compile_EType tok = compile_Type tok (Right . EType)
 168
 169 -- ** Type 'Con_Kind'
 170 data Con_Kind meta ts
 171  =   Con_Kind_Eq    (At meta ts EKind) (At meta ts EKind)
 172  |   Con_Kind_Arrow (At meta ts EKind)
 173 deriving instance (Eq_TokenR meta ts ts) => Eq (Con_Kind meta ts)
 174 deriving instance (Show_TokenR meta ts ts) => Show (Con_Kind meta ts)
 175
 176 check_Kind
 177  :: MonoLift (Con_Kind meta ts) err
 178  => At meta ts (SKind x)
 179  -> At meta ts (SKind y)
 180  -> ((x :~: y) -> Either err ret) -> Either err ret
 181 check_Kind x y k =
 182         case unAt x `eq_skind` unAt y of
 183          Just Refl -> k Refl
 184          Nothing -> Left $ olift $
 185                 Con_Kind_Eq (EKind <$> x) (EKind <$> y)
 186
 187 check_Kind_arrow
 188  :: MonoLift (Con_Kind meta ts) err
 189  => At meta ts (SKind x)
 190  -> (forall a b. (x :~: (a -> b)) -> SKind a -> SKind b -> Either err ret)
 191  -> Either err ret
 192 check_Kind_arrow x k =
 193         case unAt x of
 194          a `SKiArrow` b -> k Refl a b
 195          _ -> Left $ olift $
 196                 Con_Kind_Arrow (EKind <$> x)
 197
 198 -- ** Type 'Error_Type'
 199 data Error_Type meta ts
 200  =   Error_Type_Token_invalid    (EToken meta ts)
 201  |   Error_Type_Constant_unknown (At meta ts TyName)
 202  |   Error_Type_Con_Kind  (Con_Kind meta ts)
 203 deriving instance (Eq_TokenR meta ts ts) => Eq (Error_Type meta ts)
 204 deriving instance (Show_TokenR meta ts ts) => Show (Error_Type meta ts)
 205
 206 -- * Class 'Read_TyName'
 207 type Read_TyName raw cs = Read_TyNameR raw cs cs
 208
 209 read_TyName
 210  :: forall raw cs ret.
 211  Read_TyNameR raw cs cs
 212  => raw -> (forall k c. Type cs (c::k) -> Maybe ret)
 213  -> Maybe ret
 214 read_TyName = read_TyNameR (Proxy @cs)
 215
 216 -- ** Class 'Read_TyNameR'
 217 class Read_TyNameR raw cs rs where
 218         read_TyNameR
 219          :: Proxy rs -> raw -> (forall k c. Type cs (c::k) -> Maybe ret)
 220          -> Maybe ret
 221
 222 instance Read_TyNameR raw cs '[] where
 223         read_TyNameR _cs _c _k = Nothing
 224
 225 -- TODO: move each of these to a dedicated module.
 226 instance
 227  ( Read_TyNameR TyName cs rs
 228  , Inj_TyConst cs Fractional
 229  ) => Read_TyNameR TyName cs (Proxy Fractional ': rs) where
 230         read_TyNameR _cs (TyName "Fractional") k = k (ty @Fractional)
 231         read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
 232 instance
 233  ( Read_TyNameR TyName cs rs
 234  , Inj_TyConst cs []
 235  , Inj_TyConst cs Char
 236  ) => Read_TyNameR TyName cs (Proxy String ': rs) where
 237         read_TyNameR _cs (TyName "String") k = k (ty @[] :$ ty @Char)
 238         read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
 239
 240 instance
 241  ( Read_TyName TyName cs
 242  , Proj_Token ts Token_Type
 243  ) => Compile_Type ts cs where
 244         compile_Type
 245          :: forall meta err ret.
 246          ( MonoLift (Error_Type meta ts) err
 247          , MonoLift (Con_Kind meta ts) err
 248          ) => EToken meta ts
 249          -> (forall k h. Type cs (h::k) -> Either err ret)
 250          -> Either err ret
 251         compile_Type tok@(proj_etoken -> Just (Token_Type cst args)) kk =
 252                 fromMaybe (Left $ olift $ Error_Type_Constant_unknown $ At (Just tok) cst) $
 253                 read_TyName cst $ \typ -> Just $
 254                 go args typ kk
 255                 where
 256                 go :: [EToken meta ts]
 257                  -> Type cs h
 258                  -> (forall k' h'. Type cs (h'::k') -> Either err ret)
 259                  -> Either err ret
 260                 go [] typ k = k typ
 261                 go (tok_x:tok_xs) ty_f k =
 262                         compile_Type tok_x $ \(ty_x::Type cs (h'::k')) ->
 263                         check_Kind_arrow
 264                          (At (Just tok) $ kind_of ty_f) $ \Refl ki_f_a _ki_f_b ->
 265                         check_Kind
 266                          (At (Just tok) ki_f_a)
 267                          (At (Just tok_x) $ kind_of ty_x) $ \Refl ->
 268                         go tok_xs (ty_f :$ ty_x) k
 269         compile_Type tok _k = Left $ olift $ Error_Type_Token_invalid tok
 270
 271 -- * Type 'Types'
 272 data Types cs (hs::[K.Type]) where
 273         TypesZ :: Types cs '[]
 274         TypesS :: Type  cs h
 275                -> Types cs hs
 276                -> Types cs (Proxy h ': hs)
 277 infixr 5 `TypesS`
 278
 279 eTypes :: Types cs hs -> [EType cs]
 280 eTypes TypesZ = []
 281 eTypes (TypesS t ts) = EType t : eTypes ts
 282
 283 -- | Build the left spine of a 'Type'.
 284 spine_of_Type
 285  :: Type cs h
 286  -> (forall kc (c::kc) hs. TyConst cs c -> Types cs hs -> ret) -> ret
 287 spine_of_Type (TyConst c) k = k c TypesZ
 288 spine_of_Type (f :$ a) k = spine_of_Type f $ \c as -> k c (a `TypesS` as)
 289
 290 -- * Type 'UnProxy'
 291 type family UnProxy (x::K.Type) :: k where
 292         UnProxy (Proxy x) = x
 293
 294 -- * Class 'MonoLift'
 295 class MonoLift a b where
 296         olift :: a -> b
 297 instance MonoLift
 298  (Error_Type meta ts)
 299  (Error_Type meta ts) where
 300         olift = id
 301 instance
 302  MonoLift (Con_Kind meta ts) (Error_Type meta ts) where
 303         olift = olift . Error_Type_Con_Kind
 304
 305 -- * Class 'Gram_Type'
 306 type TokType meta = EToken meta '[Proxy Token_Type]
 307 class
 308  ( Alt g
 309  , Alter g
 310  , App g
 311  , Try g
 312  , Gram_CF g
 313  , Gram_Rule g
 314  , Gram_Terminal g
 315  , Gram_Lexer g
 316  , Gram_Op g
 317  , Gram_Meta meta g
 318  ) => Gram_Type meta g where
 319         g_type :: CF g (TokType meta)
 320         g_type = rule "type" $ g_type_fun
 321         g_type_fun :: CF g (TokType meta)
 322         g_type_fun = rule "type_fun" $
 323                 infixrG g_type_list (metaG $ op <$ symbol "->")
 324                 where op meta a b = inj_EToken meta $ Token_Type (TyName "(->)") [a, b]
 325         g_type_list :: CF g (TokType meta)
 326         g_type_list = rule "type_list" $
 327                 metaG $ inside f
 328                  (symbol "[") (option [] (pure <$> g_type)) (symbol "]")
 329                  (const <$> g_type_tuple2)
 330                 where f a meta = inj_EToken meta $ Token_Type (TyName "[]") a
 331         g_type_tuple2 :: CF g (TokType meta)
 332         g_type_tuple2 = rule "type_tuple2" $
 333                 try (parens (infixrG g_type (metaG $ op <$ symbol ","))) <+> g_type_app
 334                 where op meta a b = inj_EToken meta $ Token_Type (TyName "(,)") [a, b]
 335         g_type_app :: CF g (TokType meta)
 336         g_type_app = rule "type_app" $
 337                 f <$> some g_type_atom
 338                 where
 339                 f :: [TokType meta] -> TokType meta
 340                 f (EToken (TokenZ meta (Token_Type a as)):as') =
 341                         EToken $ TokenZ meta $ Token_Type a $ as <> as'
 342                 f _ = error "Oops, the impossible happened"
 343         g_type_atom :: CF g (TokType meta)
 344         g_type_atom = rule "type_atom" $
 345                 try (parens g_type) <+>
 346                 g_type_name <+>
 347                 g_type_symbol
 348         g_type_name :: CF g (TokType meta)
 349         g_type_name = rule "type_name" $
 350                 metaG $ lexeme $
 351                 (\c cs meta -> EToken $ TokenZ meta $ Token_Type (TyName $ Text.pack $ c:cs) [])
 352                  <$> unicat (Unicat Char.UppercaseLetter)
 353                  <*> many (choice $ unicat <$> [Unicat_Letter, Unicat_Number])
 354         g_type_symbol :: CF g (TokType meta)
 355         g_type_symbol = rule "type_symbol" $
 356                 metaG $ (f <$>) $
 357                 parens $ many $ cf_of_Terminal $ choice g_ok `but` choice g_ko
 358                 where
 359                 f s meta = inj_EToken meta $ (`Token_Type` []) $
 360                         TyName $ Text.concat ["(", Text.pack s, ")"]
 361                 g_ok = unicat <$>
 362                  [ Unicat_Symbol
 363                  , Unicat_Punctuation
 364                  , Unicat_Mark
 365                  ]
 366                 g_ko = char <$> ['(', ')', '`']
 367
 368 deriving instance Gram_Type meta g => Gram_Type meta (CF g)
 369 instance Gram_Type meta EBNF
 370 instance Gram_Type meta RuleDef
 371
 372 -- | List of the rules of 'Gram_Type'.
 373 gram_type :: Gram_Type meta g => [CF g (TokType meta)]
 374 gram_type =
 375  [ g_type
 376  , g_type_fun
 377  , g_type_list
 378  , g_type_tuple2
 379  , g_type_app
 380  , g_type_atom
 381  , g_type_name
 382  , g_type_symbol
 383  ]