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.List as List
  18 import qualified Data.Text as Text
  19 import Data.Type.Equality
  20 import qualified Data.Kind as K
  21 import GHC.Exts (Constraint)
  22 import Data.Void (Void)
  23 import Unsafe.Coerce (unsafeCoerce)
  24 import GHC.Prim (Any)
  25
  26 import Language.Symantic.Typing.Kind
  27 import Language.Symantic.Typing.Constant
  28 import Language.Symantic.Parsing
  29
  30 -- * Type 'Type'
  31
  32 -- | /Type of terms/.
  33 --
  34 -- * @vs@: /type variables/, fixed at compile time.
  35 -- * @cs@: /type constants/, fixed at compile time.
  36 -- * @h@: indexed Haskell type.
  37 -- * @k@: indexed Haskell kind of @h@.
  38 --
  39 -- * 'TyConst': /type constant/, selected amongst @cs@.
  40 -- * 'TyVar': /type variable/.
  41 --   Note that only the kind @k@ is coerced,
  42 --   @h@ being set to 'Any' to loose the type indexing.
  43 --   Note also that there is no De Bruijn encoding done to link 'TyPi's and 'TyVar's.
  44 -- * 'TyPi': /type abstraction/.
  45 --   Note that only the kind @k@ is coerced,
  46 --   @h@ being set to 'Any' to loose the type indexing.
  47 -- * @(:$)@: /type application/.
  48 -- * @(:=>)@: /type constraint/.
  49 --   Note that there is no proof of the 'Constraint' attached.
  50 --
  51 -- See also: https://ghc.haskell.org/trac/ghc/wiki/Typeable
  52 -- Which currently concludes:
  53 -- "Why kind equalities, then? Given the fact that Richard's branch
  54 -- doesn't solve this problem, what is it good for?
  55 -- It still works wonders in the mono-kinded case,
  56 -- such as for decomposing ->.
  57 -- It's just that poly-kinded constructors are still a pain."
  58
  59 data Type (cs::[K.Type]) (h::k) where
  60         TyConst :: TyConst cs c -> Type cs c
  61         (:$)    :: Type cs f -> Type cs x -> Type cs (f x)
  62         TyVar   :: SKind k -> Var -> Type cs (Any::k)
  63         TyPi    :: SKind kv -> (forall (v::kv). Type cs v -> Type cs (Any::k)) -> Type cs (Any::k)
  64         (:=>)   :: {-c =>-} Type cs (c::Constraint) -> Type cs h -> Type cs h
  65 infixl 9 :$
  66 infixl 1 :=>
  67
  68 -- | /beta-reduction/: when possible, substitute
  69 -- the abstraction of a 'TyPi' with a given 'Type'.
  70 tyApp :: Type cs a -> Type cs b -> Maybe (Type cs a)
  71 tyApp (TyPi kv f) v
  72  | Just Refl <- eq_SKind kv (kind_of v)
  73  = Just (f v)
  74 tyApp _f _v = Nothing
  75 infixl 2 `tyApp`
  76
  77 -- * Type 'Var'
  78 type Var = Int
  79
  80 -- | Drop the type index.
  81 --
  82 -- Useful when the type index cannot represent the wanted type,
  83 -- like a polymorphic type.
  84 tyVoid :: Type cs (a::k) -> Type cs (Any::Void)
  85 tyVoid = unsafeCoerce
  86 kindVoid :: SKind k -> SKind Void
  87 kindVoid = unsafeCoerce
  88 reflVoid :: (x::Void) :~: (y::Void)
  89 reflVoid = unsafeCoerce Refl
  90
  91 -- | 'Type' constructor to be used
  92 -- with @TypeApplications@
  93 -- and @NoMonomorphismRestriction@.
  94 ty :: forall c cs. Inj_TyConst cs c => Type cs c
  95 ty = TyConst inj_TyConst
  96  -- NOTE: The forall brings @c@ first in the type variables,
  97  -- which is convenient to use @TypeApplications@.
  98
  99 kind_of :: Type cs (h::k) -> SKind k
 100 kind_of t =
 101         case t of
 102          TyConst c -> kind_of_TyConst c
 103          f :$ _x ->
 104                 case kind_of f of
 105                  _kx `SKiArrow` kf -> kf
 106          _c :=> x -> kind_of x
 107          TyVar k _v -> k
 108          TyPi k f -> kind_of $ f (TyVar k 0)
 109
 110 -- | Return the smallest 'Var' not used in given 'Type'.
 111 freeTyVar :: Type cs (h::k) -> Var
 112 freeTyVar = (+ 1) . maxTyVar (-1)
 113         where
 114         maxTyVar :: Var -> Type cs h -> Var
 115         maxTyVar m TyConst{}     = m
 116         maxTyVar m (f :$ a)      = maxTyVar m f `max` maxTyVar m a
 117         maxTyVar m (TyVar _kv v) = max m v
 118         maxTyVar m (TyPi kv f)   = maxTyVar m $ f $ TyVar kv (-1)
 119         maxTyVar m (_c :=> x)    = maxTyVar m x
 120
 121 -- | Return the 'Var's (without doubles) used in given 'Type'.
 122 freeTyVars :: Type cs (h::k) -> [Var]
 123 freeTyVars = List.nub . go
 124         where
 125         go :: Type cs h -> [Var]
 126         go TyConst{}     = []
 127         go (f :$ a)      = go f `List.union` go a
 128         go (TyVar _kv v) | v >= 0    = [v]
 129                          | otherwise = []
 130         go (TyPi kv f)   = go $ f $ TyVar kv (-1)
 131         go (_c :=> x)    = go x
 132
 133 eq_Type :: Type cs (x::k)
 134         -> Type cs (y::k)
 135         -> Maybe (x:~:y)
 136 eq_Type = eq (-1)
 137         where
 138         eq :: Var
 139            -> Type cs (x::k)
 140            -> Type cs (y::k)
 141            -> Maybe (x:~:y)
 142         eq _v (TyConst x) (TyConst y)
 143          | Just Refl <- testEquality x y
 144          = Just Refl
 145         eq v (xf :$ xx) (yf :$ yx)
 146          | Just Refl <- eq_SKind (kind_of xf) (kind_of yf)
 147          , Just Refl <- eq v xf yf
 148          , Just Refl <- eq v xx yx
 149          = Just Refl
 150         eq v (TyPi xk x::Type cs xv) (TyPi xy y::Type cs yv)
 151          | Just Refl <- eq_SKind xk xy
 152          , Just Refl <- eq (v - 1) (x $ TyVar xk v) (y $ TyVar xy v)
 153          = Just Refl
 154         eq _v (TyVar xk x) (TyVar yk y)
 155          | Just Refl <- eq_SKind xk yk
 156          , True <- x == y
 157          = Just Refl
 158         eq v (xc :=> x) (yc :=> y)
 159          | Just Refl <- eq v xc yc
 160          , Just Refl <- eq v x y
 161          = Just Refl
 162         eq _ _ _ = Nothing
 163
 164 eq_Kind_Type :: Type cs (x::kx)
 165              -> Type cs (y::ky)
 166              -> Maybe (kx:~:ky)
 167 eq_Kind_Type = eq
 168         where
 169         eq :: Type cs (x::kx)
 170            -> Type cs (y::ky)
 171            -> Maybe (kx:~:ky)
 172         eq (TyConst x) (TyConst y)
 173          | Just Refl <- eq_Kind_TyConst x y
 174          = Just Refl
 175         eq (xf :$ xx) (yf :$ yx)
 176          | Just Refl <- eq xf yf
 177          , Just Refl <- eq xx yx
 178          = Just Refl
 179         eq (TyPi xk x::Type cs xv) (TyPi xy y::Type cs yv)
 180          | Just Refl <- eq_SKind xk xy
 181          , Just Refl <- eq (x $ TyVar xk 0) (y $ TyVar xy 0)
 182          = Just Refl
 183         eq (TyVar kx _x) (TyVar ky _y)
 184          | Just Refl <- eq_SKind kx ky
 185          = Just Refl
 186         eq (_xc :=> x) (_yc :=> y)
 187          | Just Refl <- eq x y
 188          = Just Refl
 189         eq _x _y = Nothing
 190
 191 show_Type :: Show_TyConst cs => Int -> Type cs h -> ShowS
 192 show_Type pr t = go (freeTyVar t) pr t
 193         where
 194         go :: Show_TyConst cs => Var -> Int -> Type cs h -> ShowS
 195         go _v p (TyConst c)   = showsPrec p c
 196         go _v p (TyVar _kv v) = showString "a" . showsPrec p v
 197         go v p (f :$ a) =
 198                 showParen (p > 10) $
 199                 go v 11 f .
 200                 showString " " .
 201                 go v 11 a
 202         go v p (c :=> a) =
 203                 showParen (p > 10) $
 204                 go v 11 c .
 205                 showString " => " .
 206                 go v 11 a
 207         go v p (TyPi kv f) =
 208                 let var = TyVar kv v in
 209                 showParen (p > 10) $
 210                 showString "forall " .
 211                 go v p var .
 212                 showString ". " .
 213                 go v 11 (f var)
 214
 215 instance TestEquality (Type cs) where
 216         testEquality = eq_Type
 217 instance Eq (Type cs h) where
 218         _x == _y = True
 219 instance Show_TyConst cs => Show (Type cs h) where
 220         showsPrec = show_Type
 221
 222 -- * Type 'EType'
 223 -- | Existential for 'Type'.
 224 data EType cs = forall h. EType (Type cs h)
 225
 226 instance Eq (EType cs) where
 227         EType x == EType y
 228          | Just Refl <- eq_Kind_Type x y
 229          = isJust $ eq_Type x y
 230         _x == _y = False
 231 instance Show_TyConst cs => Show (EType cs) where
 232         show (EType t) = show t
 233
 234 -- * Type 'KType'
 235 -- | Existential for 'Type' of a known 'Kind'.
 236 data KType cs k = forall (h::k). KType (Type cs h)
 237
 238 instance Eq (KType cs ki) where
 239         KType x == KType y = isJust $ eq_Type x y
 240 instance Show_TyConst cs => Show (KType cs ki) where
 241         showsPrec p (KType t) = show_Type p t
 242
 243 -- * Type 'TyName'
 244 newtype TyName = TyName Text
 245  deriving (Eq, Ord, Show)
 246 instance IsString TyName where
 247         fromString = TyName . fromString
 248
 249 -- * Class 'Read_TyName'
 250 type Read_TyName raw cs = Read_TyNameR raw cs cs
 251
 252 read_TyName
 253  :: forall raw cs ret.
 254  Read_TyNameR raw cs cs
 255  => raw -> (forall k c. Type cs (c::k) -> Maybe ret)
 256  -> Maybe ret
 257 read_TyName = read_TyNameR (Proxy @cs)
 258
 259 -- ** Class 'Read_TyNameR'
 260 class Read_TyNameR raw cs rs where
 261         read_TyNameR
 262          :: Proxy rs -> raw -> (forall k c. Type cs (c::k) -> Maybe ret)
 263          -> Maybe ret
 264
 265 instance Read_TyNameR raw cs '[] where
 266         read_TyNameR _cs _c _k = Nothing
 267
 268 -- TODO: move each of these to a dedicated module.
 269 instance
 270  ( Read_TyNameR TyName cs rs
 271  , Inj_TyConst cs Fractional
 272  ) => Read_TyNameR TyName cs (Proxy Fractional ': rs) where
 273         read_TyNameR _cs (TyName "Fractional") k = k (ty @Fractional)
 274         read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
 275 instance
 276  ( Read_TyNameR TyName cs rs
 277  , Inj_TyConst cs []
 278  , Inj_TyConst cs Char
 279  ) => Read_TyNameR TyName cs (Proxy String ': rs) where
 280         read_TyNameR _cs (TyName "String") k = k (ty @[] :$ ty @Char)
 281         read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
 282
 283 -- * Type 'Token_Type'
 284 type Token_Type = Type '[] ()
 285 -- data Token_Type
 286
 287 data instance TokenT meta ts (Proxy Token_Type)
 288  = Token_Type TyName [EToken meta ts]
 289 deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy Token_Type))
 290 deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy Token_Type))
 291 instance
 292  ( Read_TyNameR TyName cs rs
 293  , Inj_TyConst cs Token_Type
 294  ) => Read_TyNameR TyName cs (Proxy Token_Type ': rs) where
 295         read_TyNameR _rs (TyName "Type") k = k (ty @Token_Type)
 296         read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
 297 instance Show_TyConst cs => Show_TyConst (Proxy Token_Type ': cs) where
 298         show_TyConst TyConstZ{} = "Type"
 299         show_TyConst (TyConstS c) = show_TyConst c
 300
 301 -- * Type 'Error_Type'
 302 data Error_Type meta ts
 303  =   Error_Type_Token_invalid    (EToken meta ts)
 304  |   Error_Type_Constant_unknown (At meta ts TyName)
 305  |   Error_Type_Con_Kind  (Con_Kind meta ts)
 306 deriving instance (Eq_TokenR meta ts ts) => Eq (Error_Type meta ts)
 307 deriving instance (Show_TokenR meta ts ts) => Show (Error_Type meta ts)
 308
 309 -- * Class 'MonoLift'
 310 class MonoLift a b where
 311         olift :: a -> b
 312 instance MonoLift
 313  (Error_Type meta ts)
 314  (Error_Type meta ts) where
 315         olift = id
 316 instance
 317  MonoLift (Con_Kind meta ts) (Error_Type meta ts) where
 318         olift = olift . Error_Type_Con_Kind
 319
 320 -- * Type 'Con_Kind'
 321 data Con_Kind meta ts
 322  =   Con_Kind_Eq    (At meta ts EKind) (At meta ts EKind)
 323  |   Con_Kind_Arrow (At meta ts EKind)
 324 deriving instance (Eq_TokenR meta ts ts) => Eq (Con_Kind meta ts)
 325 deriving instance (Show_TokenR meta ts ts) => Show (Con_Kind meta ts)
 326
 327 check_Kind
 328  :: MonoLift (Con_Kind meta ts) err
 329  => At meta ts (SKind x)
 330  -> At meta ts (SKind y)
 331  -> ((x :~: y) -> Either err ret) -> Either err ret
 332 check_Kind x y k =
 333         case unAt x `eq_SKind` unAt y of
 334          Just Refl -> k Refl
 335          Nothing -> Left $ olift $
 336                 Con_Kind_Eq (EKind <$> x) (EKind <$> y)
 337
 338 check_Kind_Arrow
 339  :: MonoLift (Con_Kind meta ts) err
 340  => At meta ts (SKind x)
 341  -> (forall a b. (x :~: (a -> b)) -> SKind a -> SKind b -> Either err ret)
 342  -> Either err ret
 343 check_Kind_Arrow x k =
 344         case unAt x of
 345          a `SKiArrow` b -> k Refl a b
 346          _ -> Left $ olift $
 347                 Con_Kind_Arrow (EKind <$> x)
 348
 349 -- * Class 'Compile_Type'
 350
 351 -- | Try to build a 'Type' from an 'EToken'.
 352 class Compile_Type ts cs where
 353         compile_Type
 354          :: ( MonoLift (Error_Type meta ts) err
 355             , MonoLift (Con_Kind meta ts) err )
 356          => EToken meta ts
 357          -> (forall k h. Type cs (h::k) -> Either err ret)
 358          -> Either err ret
 359
 360 instance
 361  ( Read_TyName TyName cs
 362  , Proj_Token ts Token_Type
 363  ) => Compile_Type ts cs where
 364         compile_Type
 365          :: forall meta err ret.
 366          ( MonoLift (Error_Type meta ts) err
 367          , MonoLift (Con_Kind meta ts) err
 368          ) => EToken meta ts
 369          -> (forall k h. Type cs (h::k) -> Either err ret)
 370          -> Either err ret
 371         compile_Type tok@(proj_EToken -> Just (Token_Type cst args)) kk =
 372                 fromMaybe (Left $ olift $ Error_Type_Constant_unknown $ At (Just tok) cst) $
 373                 read_TyName cst $ \typ -> Just $
 374                 go args typ kk
 375                 where
 376                 go :: [EToken meta ts]
 377                  -> Type cs h
 378                  -> (forall k' h'. Type cs (h'::k') -> Either err ret)
 379                  -> Either err ret
 380                 go [] typ k = k typ
 381                 go (tok_x:tok_xs) ty_f k =
 382                         compile_Type tok_x $ \(ty_x::Type cs (h'::k')) ->
 383                         check_Kind_Arrow
 384                          (At (Just tok) $ kind_of ty_f) $ \Refl ki_f_a _ki_f_b ->
 385                         check_Kind
 386                          (At (Just tok) ki_f_a)
 387                          (At (Just tok_x) $ kind_of ty_x) $ \Refl ->
 388                         go tok_xs (ty_f :$ ty_x) k
 389         compile_Type tok _k = Left $ olift $ Error_Type_Token_invalid tok
 390
 391 compile_EType
 392  :: Read_TyName TyName cs
 393  => EToken meta '[Proxy Token_Type]
 394  -> Either (Error_Type meta '[Proxy Token_Type]) (EType cs)
 395 compile_EType tok = compile_Type tok (Right . EType)
 396
 397 -- * Type 'Types'
 398 data Types cs (hs::[K.Type]) where
 399         TypesZ :: Types cs '[]
 400         TypesS :: Type  cs h
 401                -> Types cs hs
 402                -> Types cs (Proxy h ': hs)
 403 infixr 5 `TypesS`
 404
 405 eTypes :: Types cs hs -> [EType cs]
 406 eTypes TypesZ = []
 407 eTypes (TypesS t ts) = EType t : eTypes ts
 408
 409 -- | Build the left spine of a 'Type'.
 410 spine_of_Type
 411  :: Type cs h
 412  -> (forall ka (a::ka) hs.
 413      Either Var (TyConst cs a) -> Types cs hs -> ret)
 414  -> ret
 415 spine_of_Type = go
 416         where
 417         go :: Type cs h
 418            -> (forall ka (a::ka) hs.
 419               Either Var (TyConst cs a) -> Types cs hs -> ret)
 420            -> ret
 421         go (TyConst c)   k = k (Right c) TypesZ
 422         go (f :$ a)      k = go f $ \c as -> k c (a `TypesS` as)
 423         go (TyVar _kv v) k = k (Left v) TypesZ
 424         go (TyPi _kv _f) _k = undefined -- FIXME: see what to do in this case.
 425         go (_c :=> x)    k = go x k
 426
 427 -- * Type 'UnProxy'
 428 type family UnProxy (x::K.Type) :: k where
 429         UnProxy (Proxy x) = x
 430
 431 -- * Class 'Gram_Type'
 432 type TokType meta = EToken meta '[Proxy Token_Type]
 433 class
 434  ( Alt g
 435  , Alter g
 436  , App g
 437  , Try g
 438  , Gram_CF g
 439  , Gram_Rule g
 440  , Gram_Terminal g
 441  , Gram_Lexer g
 442  , Gram_Op g
 443  , Gram_Meta meta g
 444  ) => Gram_Type meta g where
 445         g_type :: CF g (TokType meta)
 446         g_type = rule "type" $ g_type_fun
 447         g_type_fun :: CF g (TokType meta)
 448         g_type_fun = rule "type_fun" $
 449                 infixrG g_type_list (metaG $ op <$ symbol "->")
 450                 where op meta a b = inj_EToken meta $ Token_Type "(->)" [a, b]
 451         g_type_list :: CF g (TokType meta)
 452         g_type_list = rule "type_list" $
 453                 metaG $ inside f
 454                  (symbol "[") (option [] (pure <$> g_type)) (symbol "]")
 455                  (const <$> g_type_tuple2)
 456                 where f a meta = inj_EToken meta $ Token_Type "[]" a
 457         g_type_tuple2 :: CF g (TokType meta)
 458         g_type_tuple2 = rule "type_tuple2" $
 459                 try (parens (infixrG g_type (metaG $ op <$ symbol ","))) <+> g_type_app
 460                 where op meta a b = inj_EToken meta $ Token_Type "(,)" [a, b]
 461         g_type_app :: CF g (TokType meta)
 462         g_type_app = rule "type_app" $
 463                 f <$> some g_type_atom
 464                 where
 465                 f :: [TokType meta] -> TokType meta
 466                 f (EToken (TokenZ meta (Token_Type a as)):as') =
 467                         EToken $ TokenZ meta $ Token_Type a $ as <> as'
 468                 f _ = error "Oops, the impossible happened"
 469         g_type_atom :: CF g (TokType meta)
 470         g_type_atom = rule "type_atom" $
 471                 try (parens g_type) <+>
 472                 g_type_name <+>
 473                 g_type_symbol
 474         g_type_name :: CF g (TokType meta)
 475         g_type_name = rule "type_name" $
 476                 metaG $ lexeme $
 477                 (\c cs meta -> EToken $ TokenZ meta $ Token_Type (TyName $ Text.pack $ c:cs) [])
 478                  <$> unicat (Unicat Char.UppercaseLetter)
 479                  <*> many (choice $ unicat <$> [Unicat_Letter, Unicat_Number])
 480         g_type_symbol :: CF g (TokType meta)
 481         g_type_symbol = rule "type_symbol" $
 482                 metaG $ (f <$>) $
 483                 parens $ many $ cf_of_Terminal $ choice g_ok `but` choice g_ko
 484                 where
 485                 f s meta = inj_EToken meta $ (`Token_Type` []) $
 486                         TyName $ Text.concat ["(", Text.pack s, ")"]
 487                 g_ok = unicat <$>
 488                  [ Unicat_Symbol
 489                  , Unicat_Punctuation
 490                  , Unicat_Mark
 491                  ]
 492                 g_ko = char <$> ['(', ')', '`']
 493
 494 deriving instance Gram_Type meta g => Gram_Type meta (CF g)
 495 instance Gram_Type meta EBNF
 496 instance Gram_Type meta RuleDef
 497
 498 -- | List of the rules of 'Gram_Type'.
 499 gram_type :: Gram_Type meta g => [CF g (TokType meta)]
 500 gram_type =
 501  [ g_type
 502  , g_type_fun
 503  , g_type_list
 504  , g_type_tuple2
 505  , g_type_app
 506  , g_type_atom
 507  , g_type_name
 508  , g_type_symbol
 509  ]