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