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