src/Symantic/Typer/Type.hs

   1 {-# LANGUAGE ConstraintKinds #-}
   2 {-# LANGUAGE PatternSynonyms #-}
   3 {-# LANGUAGE PolyKinds #-}
   4 {-# LANGUAGE RankNTypes #-}
   5 {-# LANGUAGE StandaloneDeriving #-}
   6 {-# LANGUAGE UndecidableInstances #-}
   7 {-# LANGUAGE UndecidableSuperClasses #-}
   8 {-# LANGUAGE ViewPatterns #-}
   9 {-# OPTIONS_GHC -Wno-partial-fields #-}
  10
  11 module Symantic.Typer.Type where
  12
  13 import Control.Monad.Classes as MC ()
  14 import Control.Monad.Classes.Run as MC ()
  15 import Data.Eq (Eq (..))
  16 import Data.Function (($))
  17 import Data.Functor ((<$>))
  18 import Data.Map.Strict qualified as Map
  19 import Data.Maybe (Maybe (..), isJust)
  20 import Data.Monoid (Monoid (..))
  21 import Data.Proxy (Proxy (..))
  22 import Data.Semigroup (Semigroup (..))
  23 import Data.String (String)
  24 import GHC.Types
  25 import Text.Show (Show (..))
  26 import Type.Reflection (TypeRep, Typeable, eqTypeRep, typeRep, typeRepKind, (:~~:) (..), pattern App)
  27 import Prelude qualified
  28
  29 import Symantic.Typer.Eq
  30 import Symantic.Typer.List
  31
  32 data WithProv prov a = WithProv {withProv :: prov, unWithProv :: a}
  33
  34 -- * Type 'Const'
  35 type Const = TypeRep
  36
  37 -- * Type 'Name'
  38 type Name = String
  39
  40 -- * Type 'Prov'
  41 type Prov = Type
  42
  43 -- * Type 'Var'
  44 data Var :: forall vK. Prov -> [Type] -> vK -> Type where
  45   VarZ ::
  46     { varZKind :: Kind prov vK
  47     , varZNext :: Len ws
  48     } ->
  49     Var prov (Proxy (v :: vK) ': ws) (v :: vK)
  50   VarS :: Var prov vs v -> Var prov (not_v ': vs) v
  51 deriving instance Show prov => Show (Var prov vs v)
  52
  53 pattern Var :: () => () => Kind prov vK -> Len ws -> Var prov vs' (v :: vK)
  54 pattern Var{varKind, varNext} <- (var -> VarVS VarZ{varZKind = varKind, varZNext = varNext})
  55 {-# COMPLETE Var #-}
  56
  57 -- -- * Type 'VarVS'
  58 data VarVS prov (v :: vK) = forall vs. VarVS (Var prov vs v)
  59 var :: Var prov vs (v :: vK) -> VarVS prov (v :: vK)
  60 var v@VarZ{} = VarVS v
  61 var (VarS v) = var v
  62
  63 instance EqTy (Var prov vs) (Var prov vs) where
  64   eqTy VarZ{} VarZ{} = Just HRefl
  65   eqTy (VarS x) (VarS y) = eqTy x y
  66   eqTy _ _ = Nothing
  67
  68 type VarSem = Type -> [Type] -> Type -> Type
  69
  70 -- data VarV (var::VarSem) vs = forall vK (v::vK). VarVSem (var vs v)
  71 data VarV prov vs = forall v. VarV (Var prov vs v)
  72
  73 class LenVar var where
  74   lenVar :: var prov vs a -> Len vs
  75 instance LenVar Var where
  76   lenVar VarZ{varZNext} = LenS varZNext
  77   lenVar (VarS v) = LenS (lenVar v)
  78
  79 class LenVar var => AllocVars var where
  80   allocVarsL :: Len len -> var prov vs x -> var prov (len ++ vs) x
  81   allocVarsR :: Len len -> var prov vs x -> var prov (vs ++ len) x
  82 instance AllocVars Var where
  83   allocVarsL LenZ v = v
  84   allocVarsL (LenS len) v = VarS (allocVarsL len v)
  85
  86   allocVarsR len VarZ{..} = VarZ{varZNext = addLen varZNext len, ..}
  87   allocVarsR len (VarS v) = VarS (allocVarsR len v)
  88
  89 appendVars ::
  90   AllocVars xVar =>
  91   AllocVars yVar =>
  92   xVar prov xVS (x :: xK) ->
  93   yVar prov yVS (y :: yK) ->
  94   ( xVar prov (xVS ++ yVS) x
  95   , yVar prov (xVS ++ yVS) y
  96   )
  97 appendVars x y =
  98   ( allocVarsR (lenVar y) x
  99   , allocVarsL (lenVar x) y
 100   )
 101
 102 -- ** Type 'IndexVar'
 103
 104 -- | Index of a 'Var'.
 105 type IndexVar = Int
 106
 107 indexVar :: Var prov vs v -> Int
 108 indexVar VarZ{} = 0
 109 indexVar (VarS v) = 1 Prelude.+ indexVar v
 110
 111 -- instance KindOf (Var prov vs) where
 112 --   kindOf = fmap go
 113 --     where
 114 --     go :: forall vs2 aK a. Var prov vs2 (Proxy (a::aK)) -> TypeRep aK
 115 --     go VarZ{varKind} = varKind
 116 --     go (VarS v) = go v
 117
 118 -- * Type 'Vars'
 119 type Vars prov vs = Map.Map Name (VarV prov vs)
 120
 121 lookupVar :: Name -> Vars prov vs -> Maybe (VarV prov vs)
 122 lookupVar = Map.lookup
 123
 124 insertVar :: Name -> VarV prov vs -> Vars prov vs -> Vars prov vs
 125 insertVar = Map.insert
 126
 127 -- * Type 'UsedVars'
 128
 129 -- | List of 'Var's, used to change the context of a 'Var'
 130 -- when removing unused 'Var's.
 131 data UsedVars oldVS prov newVS a where
 132   UsedVarsZ :: UsedVars oldVS prov '[] a
 133   UsedVarsS ::
 134     Var prov oldVS (v :: vK) ->
 135     UsedVars oldVS prov newVS a ->
 136     UsedVars oldVS prov (Proxy (v :: vK) ': newVS) a
 137
 138 instance LenVar (UsedVars oldVS) where
 139   lenVar UsedVarsZ = LenZ
 140   lenVar (UsedVarsS _v oldVS) = LenS $ lenVar oldVS
 141
 142 lookupUsedVars ::
 143   Var prov oldVS (v :: vK) ->
 144   UsedVars oldVS prov newVS a ->
 145   Maybe (Var prov newVS (v :: vK))
 146 lookupUsedVars _v UsedVarsZ = Nothing
 147 lookupUsedVars v (UsedVarsS v' us) = do
 148   case v `eqTy` v' of
 149     Just HRefl ->
 150       case v' of
 151         Var{varKind} ->
 152           Just
 153             VarZ
 154               { varZNext = lenVar us
 155               , varZKind = varKind
 156               }
 157     Nothing -> VarS Data.Functor.<$> lookupUsedVars v us
 158
 159 insertUsedVars ::
 160   Var prov vs v ->
 161   UsedVars vs prov us a ->
 162   Maybe (UsedVars vs prov (Proxy v ': us) a)
 163 insertUsedVars v vs =
 164   case lookupUsedVars v vs of
 165     Just{} -> Nothing
 166     Nothing -> Just (UsedVarsS v vs)
 167
 168 -- * Class 'VarOccursIn'
 169
 170 -- | Test whether a given 'Var' occurs within @(t)@.
 171 class VarOccursIn (t :: Type -> [Type] -> aK -> Type) where
 172   varOccursIn :: Var prov vs v -> t prov vs a -> Bool
 173
 174 -- * Class 'UsedVarsOf'
 175 class UsedVarsOf t where
 176   usedVarsOf ::
 177     UsedVars vs prov oldVS a ->
 178     t prov vs b ->
 179     (forall newVS. UsedVars vs prov newVS a -> ret) ->
 180     ret
 181
 182 -- * Type 'Ty'
 183
 184 -- Use a CUSK, because it's a polymorphically recursive type,
 185 -- See https://ryanglscott.github.io/2020/01/05/five-benefits-to-using-standalonekindsignatures/
 186 data Ty :: forall aK. Prov -> [Type] -> aK -> Type where
 187   TyConst :: {tyConst :: Const a, tyConstLen :: Len vs} -> Ty prov vs a
 188   TyVar :: {tyVar :: Var prov vs a, tyVarName :: Name} -> Ty prov vs a
 189   TyApp :: {tyAppFun :: Ty prov vs f, tyAppArg :: Ty prov vs a} -> Ty prov vs (f a)
 190   TyProv :: {tyProv :: prov, tyUnProv :: Ty prov vs a} -> Ty prov vs a
 191 infixl 9 `TyApp`
 192
 193 tyOfTypeRep :: Len vs -> TypeRep a -> Ty prov vs a
 194 tyOfTypeRep len ty = case ty of
 195   App f x -> TyApp{tyAppFun = tyOfTypeRep len f, tyAppArg = tyOfTypeRep len x}
 196   constType -> TyConst{tyConst = constType, tyConstLen = len}
 197
 198 -- | Monomorphic 'Ty' from a 'Typeable'.
 199 monoTy :: forall {aK} (a :: aK) prov. Typeable a => Ty prov '[] a
 200 monoTy = tyOfTypeRep LenZ typeRep
 201
 202 aTy :: LenInj vs => Monoid prov => Ty prov (Proxy a ': vs) (a :: Type)
 203 bTy :: LenInj vs => Monoid prov => Ty prov (Proxy a ': Proxy b ': vs) (b :: Type)
 204 cTy :: LenInj vs => Monoid prov => Ty prov (Proxy a : Proxy b : Proxy c : vs) (c :: Type)
 205 dTy :: LenInj vs => Monoid prov => Ty prov (Proxy a : Proxy b : Proxy c : Proxy d : vs) (d :: Type)
 206 aTy = TyVar{tyVar = VarZ{varZKind = monoTy @Type, varZNext = lenInj}, tyVarName = "a"}
 207 bTy = TyVar{tyVar = VarS $ VarZ{varZKind = monoTy @Type, varZNext = lenInj}, tyVarName = "b"}
 208 cTy = TyVar{tyVar = VarS $ VarS $ VarZ{varZKind = monoTy @Type, varZNext = lenInj}, tyVarName = "c"}
 209 dTy = TyVar{tyVar = VarS $ VarS $ VarS $ VarZ{varZKind = monoTy @Type, varZNext = lenInj}, tyVarName = "d"}
 210
 211 pattern FUN ::
 212   -- CReq
 213   forall k (fun :: k) prov vs.
 214   () =>
 215   {-Monoid prov-}
 216   -- CProv
 217   forall
 218     (r1 :: RuntimeRep)
 219     (r2 :: RuntimeRep)
 220     (arg :: TYPE r1)
 221     (res :: TYPE r2).
 222   ( k ~ Type
 223   , fun ~~ (arg -> res)
 224   -- , r1 ~ LiftedRep
 225   -- , r2 ~ LiftedRep {- fixme: remove those 2 constraints -}
 226   ) =>
 227   Ty prov vs arg ->
 228   Ty prov vs res ->
 229   Ty prov vs fun
 230 pattern FUN arg res <-
 231   TyApp
 232     { tyAppFun =
 233       TyApp
 234         { tyAppFun = TyConst{tyConst = eqTypeRep (typeRep @(->)) -> Just HRefl}
 235         , tyAppArg = arg
 236         }
 237     , tyAppArg = res
 238     }
 239
 240 (~>) :: Monoid prov => Ty prov vs a -> Ty prov vs b -> Ty prov vs (a -> b)
 241 (~>) arg res =
 242   TyApp
 243     { tyAppFun =
 244         TyApp
 245           { tyAppFun =
 246               TyConst{tyConst = typeRep, tyConstLen = (lenVar arg)}
 247           , tyAppArg = arg
 248           }
 249     , tyAppArg = res
 250     }
 251 infixr 0 ~>
 252
 253 deriving instance Show prov => Show (Ty prov vs a)
 254
 255 -- type instance SourceOf (Ty vs src t) = src
 256 instance LenVar Ty where
 257   lenVar TyConst{tyConstLen} = tyConstLen
 258   lenVar TyApp{tyAppFun} = lenVar tyAppFun
 259   lenVar TyVar{tyVar} = lenVar tyVar
 260   lenVar TyProv{tyUnProv} = lenVar tyUnProv
 261
 262 -- lenVars (TyFam l _f _as) = l
 263 instance AllocVars Ty where
 264   allocVarsL len ty@TyConst{..} = ty{tyConstLen = addLen len tyConstLen}
 265   allocVarsL len TyApp{..} = TyApp{tyAppFun = allocVarsL len tyAppFun, tyAppArg = allocVarsL len tyAppArg}
 266   allocVarsL len ty@TyVar{..} = ty{tyVar = allocVarsL len tyVar}
 267   allocVarsL len TyProv{..} = TyProv{tyProv, tyUnProv = allocVarsL len tyUnProv}
 268
 269   -- allocVarsL len (TyFam l f as) = TyFam (addLen len l) f $ allocVarsL len `mapTys` as
 270
 271   allocVarsR len ty@TyConst{..} = ty{tyConstLen = addLen tyConstLen len}
 272   allocVarsR len TyApp{..} = TyApp{tyAppFun = allocVarsR len tyAppFun, tyAppArg = allocVarsR len tyAppArg, ..}
 273   allocVarsR len ty@TyVar{..} = ty{tyVar = allocVarsR len tyVar}
 274   allocVarsR len TyProv{..} = TyProv{tyProv, tyUnProv = allocVarsR len tyUnProv}
 275
 276 -- allocVarsR len (TyFam l f as) = TyFam (addLen l len) f $ allocVarsR len `mapTys` as
 277
 278 instance VarOccursIn Ty where
 279   varOccursIn v TyVar{tyVar = v'} | Just{} <- v `eqTy` v' = False
 280   varOccursIn _v TyVar{} = False
 281   varOccursIn _v TyConst{} = False
 282   varOccursIn v TyApp{tyAppFun = f, tyAppArg = a} = varOccursIn v f Prelude.|| varOccursIn v a
 283   varOccursIn v TyProv{..} = varOccursIn v tyUnProv
 284
 285 -- varOccursIn v (TyFam _src _len _fam as) = varOccursIn v as
 286 instance UsedVarsOf Ty where
 287   usedVarsOf vs TyConst{} k = k vs
 288   usedVarsOf vs TyApp{tyAppFun = f, tyAppArg = a} k =
 289     usedVarsOf vs f $ \vs' ->
 290       usedVarsOf vs' a k
 291   usedVarsOf vs TyVar{tyVar = v} k =
 292     case insertUsedVars v vs of
 293       Nothing -> k vs
 294       Just vs' -> k vs'
 295   usedVarsOf vs TyProv{tyUnProv} k = usedVarsOf vs tyUnProv k
 296
 297 -- usedVarsOf vs (TyFam _src _len _fam as) k = usedVarsOf vs as k
 298
 299 -- ** Type 'TyT'
 300
 301 -- | Existential for 'Type'.
 302 data TyT prov vs = forall a. TyT (Ty prov vs a)
 303
 304 -- type instance SourceOf (TyT vs src) = src
 305 instance Eq (TyT prov vs) where
 306   TyT x == TyT y = isJust $ eqTy x y
 307 instance Show prov => Show (TyT prov vs) where
 308   showsPrec p (TyT x) = showsPrec p x
 309
 310 -- * Type 'Kind'
 311 type Kind prov a = Ty prov '[] a
 312
 313 -- ** Type 'KindK'
 314 type KindK prov = TyT prov '[]
 315
 316 -- ** Type 'TyVT'
 317 data TyVT prov = forall vs a. TyVT (Ty prov vs a)
 318
 319 deriving instance Show prov => Show (TyVT prov)
 320 instance Eq (TyVT m) where
 321   TyVT x == TyVT y = isJust (eqTy x' y')
 322     where
 323       (x', y') = appendVars x y
 324
 325 -- instance (Monoid src) => EqTy (MT.Writer src) (MT.Writer src) where
 326 --  eqTy x y = eqTy (unSourced x) (unSourced y)
 327 instance EqTy (Ty prov vs) (Ty prov vs) where
 328   eqTy = go
 329     where
 330       go :: forall xK xT yK yT. Ty prov vs (xT :: xK) -> Ty prov vs (yT :: yK) -> Maybe (xT :~~: yT)
 331       go TyConst{tyConst = x} TyConst{tyConst = y} = eqTy x y
 332       go TyVar{tyVar = x} TyVar{tyVar = y} = eqTy x y
 333       go TyApp{tyAppFun = xF, tyAppArg = xA} TyApp{tyAppFun = yF, tyAppArg = yA}
 334         | Just HRefl <- go xF yF
 335         , Just HRefl <- go xA yA =
 336             Just HRefl
 337       go TyProv{tyUnProv = x} y = go x y
 338       go x TyProv{tyUnProv = y} = go x y
 339       go _x _y = Nothing
 340
 341 -- eqTy (TyFam _ _lx xF xA) (TyFam _ _ly yF yA)
 342 --  | Just HRefl <- eqTypeRep xF yF
 343 --  , Just HRefl <- eqTys xA yA
 344 --  = Just HRefl
 345 -- -- NOTE: 'TyFam' is expanded as much as possible.
 346 -- eqTy x@TyFam{} y = eqTy (expandFam x) y
 347 -- eqTy x y@TyFam{} = eqTy x (expandFam y)
 348
 349 -- * Type 'Tys'
 350 data Tys (as :: [Type]) prov vs (a :: aK) where
 351   TysZ :: Tys '[] prov vs a
 352   TysS :: Ty prov vs a -> Tys as prov vs b -> Tys (Proxy a ': as) prov vs b
 353 infixr 5 `TysS`
 354
 355 -- type instance SourceOf (Tys vs src ts) = src
 356 -- instance ConstsOf (Tys prov vs ts) where
 357 --  constsOf TysZ = Set.empty
 358 --  constsOf (TysS t ts) = constsOf t `Set.union` constsOf ts
 359 instance UsedVarsOf (Tys as) where
 360   usedVarsOf vs TysZ k = k vs
 361   usedVarsOf vs (TysS t ts) k =
 362     usedVarsOf vs t $ \vs' ->
 363       usedVarsOf vs' ts k
 364 instance VarOccursIn (Tys as) where
 365   varOccursIn _v TysZ = False
 366   varOccursIn v (TysS t ts) = varOccursIn v t Prelude.|| varOccursIn v ts
 367
 368 -- ** Type family 'FunArg'
 369 type family FunArg (fun :: Type) :: Type where
 370   FunArg (q #> f) = FunArg f
 371   FunArg (a -> b) = a
 372
 373 -- ** Type family 'FunRes'
 374 type family FunRes (fun :: Type) :: Type where
 375   FunRes (q #> f) = FunRes f
 376   FunRes (a -> b) = b
 377
 378 -- -- | Return, when the given 'Type' is a function,
 379 -- -- the argument of that function.
 380 -- unTyFun ::
 381 --  forall t src tys.
 382 --  SourceInj (TyVT src) src =>
 383 --  --Constable (->) =>
 384 --  Type src tys t ->
 385 --  Maybe ( Type src tys (FunArg t)
 386 --        , Type src tys (FunRes t) )
 387 -- unTyFun ty_ini = go ty_ini
 388 --   where
 389 --   go ::
 390 --    Type src tys x ->
 391 --    Maybe ( Type src tys (FunArg x)
 392 --          , Type src tys (FunRes x) )
 393 --   go (TyApp _ (TyApp _ (TyConst _ _ f) a) b)
 394 --    | Just HRefl <- proj_ConstKi @(K (->)) @(->) f
 395 --    = Just ((a `withSource` TyVT ty_ini), (b `withSource` TyVT ty_ini))
 396 --   go (TyApp _ (TyApp _ (TyConst _ _ f) _a) b)
 397 --    | Just HRefl <- proj_ConstKi @(K (#>)) @(#>) f
 398 --    = go b
 399 --   go TyApp{}   = Nothing
 400 --   go TyConst{} = Nothing
 401 --   go TyVar{}   = Nothing
 402 --   go TyFam{}   = Nothing
 403
 404 proj_ConstKi ::
 405   forall kc (c :: kc) u.
 406   Typeable c =>
 407   -- (kc ~ Type_of_Ty (Ty_of_Type kc)) =>
 408   -- KindInjP (Ty_of_Type kc) =>
 409   Const u ->
 410   Maybe (c :~~: u)
 411 proj_ConstKi = eqTypeRep (typeRep @c)
 412
 413 -- ** Type @(#>)@
 414
 415 -- | /Type constant/ to qualify a 'Type'.
 416 newtype (#>) (q :: Constraint) (a :: Type) = Qual (q => a)
 417
 418 -- | Qualify a 'Type'.
 419 (#>) :: Monoid prov => Ty prov vs q -> Ty prov vs t -> Ty prov vs (q #> t)
 420 (#>) q t =
 421   -- (tyConstLen @(K (#>)) @(#>) (lenVars q) `tyApp` q) `tyApp` t
 422   TyApp
 423     { tyAppFun =
 424         TyApp
 425           { tyAppFun = TyConst{tyConst = typeRep @(#>), tyConstLen = lenVar q}
 426           , tyAppArg = q
 427           }
 428     , tyAppArg = t
 429     }
 430
 431 infixr 0 #>
 432
 433 -- NOTE: should actually be (-1)
 434 -- to compose well with @infixr 0 (->)@
 435 -- but this is not allowed by GHC.
 436
 437 -- ** Class @(#)@
 438
 439 -- | 'Constraint' union.
 440 class ((x, y) :: Constraint) => x # y
 441
 442 instance ((x, y) :: Constraint) => x # y
 443
 444 -- | Unify two 'K.Constraint's.
 445 (#) :: Monoid prov => Ty prov vs qx -> Ty prov vs qy -> Ty prov vs (qx # qy)
 446 (#) a b =
 447   -- (tyConstLen @(K (#)) @(#) (lenVars a) `tyApp` a) `tyApp` b
 448   TyApp
 449     { tyAppFun =
 450         TyApp
 451           { tyAppFun = TyConst{tyConst = typeRep @(#), tyConstLen = lenVar a}
 452           , tyAppArg = a
 453           }
 454     , tyAppArg = b
 455     }
 456
 457 infixr 2 #
 458
 459 -- * Class 'KindOf'
 460 class KindOf (ty :: Prov -> [Type] -> aK -> Type) where
 461   -- | Return the kind of the given 'Var'.
 462   kindOf ::
 463     -- HasCallStack =>
 464     ProvenanceKindOf ty prov =>
 465     Show prov =>
 466     ty prov vs (a :: aK) ->
 467     Kind prov (aK :: Type)
 468
 469 instance KindOf Var where
 470   kindOf v@Var{varKind} = TyProv (provenanceKindOf v) varKind
 471 instance KindOf Ty where
 472   kindOf ty = TyProv (provenanceKindOf ty) (go ty)
 473     where
 474       go ::
 475         Show prov =>
 476         Ty prov vs (a :: aK) ->
 477         Kind prov (aK :: Type)
 478       go TyConst{tyConst = constType :: Const (a :: aK)} =
 479         tyOfTypeRep LenZ (typeRepKind constType)
 480       go TyApp{tyAppFun = f} = case go f of
 481         TyApp
 482           { tyAppFun =
 483             TyApp
 484               { tyAppFun = TyConst{tyConst = eqTypeRep (typeRep @(->)) -> Just HRefl}
 485               }
 486           , tyAppArg = k
 487           } -> k
 488         t -> Prelude.error $ "here: " <> show t
 489       go TyVar{..} = varKind tyVar
 490       go TyProv{..} = go tyUnProv
 491
 492 -- ** Class 'ProvenanceKindOf'
 493 class ProvenanceKindOf (ty :: Prov -> [Type] -> aK -> Type) prov where
 494   provenanceKindOf :: ty prov vs (a :: aK) -> prov
 495 instance ProvenanceKindOf ty () where
 496   provenanceKindOf _ = ()
 497 instance ProvenanceKindOf Ty String where
 498   provenanceKindOf = show
 499 instance ProvenanceKindOf Var String where
 500   provenanceKindOf = show
 501
 502 -- kindOf (TyFam _src _len fam _as) = kindOfConst fam