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