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 SkipTyProv :: () => () => Ty prov vs a -> Ty prov vs a
 212 pattern SkipTyProv ty <- (skipTyProv -> ty)
 213 {-# COMPLETE SkipTyProv #-}
 214
 215 skipTyProv :: Ty prov vs a -> Ty prov vs a
 216 skipTyProv TyProv{tyUnProv} = tyUnProv
 217 skipTyProv x = x
 218
 219 pattern FUN ::
 220   -- CReq
 221   forall k (fun :: k) prov vs.
 222   () =>
 223   {-Monoid prov-}
 224   -- CProv
 225   forall
 226     (r1 :: RuntimeRep)
 227     (r2 :: RuntimeRep)
 228     (arg :: TYPE r1)
 229     (res :: TYPE r2).
 230   ( k ~ Type
 231   , fun ~~ (arg -> res)
 232   -- , r1 ~ LiftedRep
 233   -- , r2 ~ LiftedRep {- fixme: remove those 2 constraints -}
 234   ) =>
 235   Ty prov vs arg ->
 236   Ty prov vs res ->
 237   Ty prov vs fun
 238 pattern FUN arg res <-
 239   SkipTyProv
 240     TyApp
 241       { tyAppFun =
 242         SkipTyProv
 243           TyApp
 244             { tyAppFun = SkipTyProv TyConst{tyConst = eqTypeRep (typeRep @(->)) -> Just HRefl}
 245             , tyAppArg = arg
 246             }
 247       , tyAppArg = res
 248       }
 249
 250 (~>) :: Monoid prov => Ty prov vs a -> Ty prov vs b -> Ty prov vs (a -> b)
 251 (~>) arg res =
 252   TyApp
 253     { tyAppFun =
 254         TyApp
 255           { tyAppFun =
 256               TyConst{tyConst = typeRep, tyConstLen = (lenVar arg)}
 257           , tyAppArg = arg
 258           }
 259     , tyAppArg = res
 260     }
 261 infixr 0 ~>
 262
 263 deriving instance Show prov => Show (Ty prov vs a)
 264
 265 -- type instance SourceOf (Ty vs src t) = src
 266 instance LenVar Ty where
 267   lenVar TyConst{tyConstLen} = tyConstLen
 268   lenVar TyApp{tyAppFun} = lenVar tyAppFun
 269   lenVar TyVar{tyVar} = lenVar tyVar
 270   lenVar TyProv{tyUnProv} = lenVar tyUnProv
 271
 272 -- lenVars (TyFam l _f _as) = l
 273 instance AllocVars Ty where
 274   allocVarsL len ty@TyConst{..} = ty{tyConstLen = addLen len tyConstLen}
 275   allocVarsL len TyApp{..} = TyApp{tyAppFun = allocVarsL len tyAppFun, tyAppArg = allocVarsL len tyAppArg}
 276   allocVarsL len ty@TyVar{..} = ty{tyVar = allocVarsL len tyVar}
 277   allocVarsL len TyProv{..} = TyProv{tyProv, tyUnProv = allocVarsL len tyUnProv}
 278
 279   -- allocVarsL len (TyFam l f as) = TyFam (addLen len l) f $ allocVarsL len `mapTys` as
 280
 281   allocVarsR len ty@TyConst{..} = ty{tyConstLen = addLen tyConstLen len}
 282   allocVarsR len TyApp{..} = TyApp{tyAppFun = allocVarsR len tyAppFun, tyAppArg = allocVarsR len tyAppArg, ..}
 283   allocVarsR len ty@TyVar{..} = ty{tyVar = allocVarsR len tyVar}
 284   allocVarsR len TyProv{..} = TyProv{tyProv, tyUnProv = allocVarsR len tyUnProv}
 285
 286 -- allocVarsR len (TyFam l f as) = TyFam (addLen l len) f $ allocVarsR len `mapTys` as
 287
 288 instance VarOccursIn Ty where
 289   varOccursIn v TyVar{tyVar = v'} | Just{} <- v `eqTy` v' = False
 290   varOccursIn _v TyVar{} = False
 291   varOccursIn _v TyConst{} = False
 292   varOccursIn v TyApp{tyAppFun = f, tyAppArg = a} = varOccursIn v f Prelude.|| varOccursIn v a
 293   varOccursIn v TyProv{..} = varOccursIn v tyUnProv
 294
 295 -- varOccursIn v (TyFam _src _len _fam as) = varOccursIn v as
 296 instance UsedVarsOf Ty where
 297   usedVarsOf vs TyConst{} k = k vs
 298   usedVarsOf vs TyApp{tyAppFun = f, tyAppArg = a} k =
 299     usedVarsOf vs f $ \vs' ->
 300       usedVarsOf vs' a k
 301   usedVarsOf vs TyVar{tyVar = v} k =
 302     case insertUsedVars v vs of
 303       Nothing -> k vs
 304       Just vs' -> k vs'
 305   usedVarsOf vs TyProv{tyUnProv} k = usedVarsOf vs tyUnProv k
 306
 307 -- usedVarsOf vs (TyFam _src _len _fam as) k = usedVarsOf vs as k
 308
 309 -- ** Type 'TyT'
 310
 311 -- | Existential for 'Type'.
 312 data TyT prov vs = forall a. TyT (Ty prov vs a)
 313
 314 -- type instance SourceOf (TyT vs src) = src
 315 instance Eq (TyT prov vs) where
 316   TyT x == TyT y = isJust $ eqTy x y
 317 instance Show prov => Show (TyT prov vs) where
 318   showsPrec p (TyT x) = showsPrec p x
 319
 320 -- * Type 'Kind'
 321 type Kind prov a = Ty prov '[] a
 322
 323 -- ** Type 'KindK'
 324 type KindK prov = TyT prov '[]
 325
 326 -- ** Type 'TyVT'
 327 data TyVT prov = forall vs a. TyVT (Ty prov vs a)
 328
 329 deriving instance Show prov => Show (TyVT prov)
 330 instance Eq (TyVT m) where
 331   TyVT x == TyVT y = isJust (eqTy x' y')
 332     where
 333       (x', y') = appendVars x y
 334
 335 -- instance (Monoid src) => EqTy (MT.Writer src) (MT.Writer src) where
 336 --  eqTy x y = eqTy (unSourced x) (unSourced y)
 337 instance EqTy (Ty prov vs) (Ty prov vs) where
 338   eqTy = go
 339     where
 340       go :: forall xK xT yK yT. Ty prov vs (xT :: xK) -> Ty prov vs (yT :: yK) -> Maybe (xT :~~: yT)
 341       go TyConst{tyConst = x} TyConst{tyConst = y} = eqTy x y
 342       go TyVar{tyVar = x} TyVar{tyVar = y} = eqTy x y
 343       go TyApp{tyAppFun = xF, tyAppArg = xA} TyApp{tyAppFun = yF, tyAppArg = yA}
 344         | Just HRefl <- go xF yF
 345         , Just HRefl <- go xA yA =
 346             Just HRefl
 347       go TyProv{tyUnProv = x} y = go x y
 348       go x TyProv{tyUnProv = y} = go x y
 349       go _x _y = Nothing
 350
 351 -- eqTy (TyFam _ _lx xF xA) (TyFam _ _ly yF yA)
 352 --  | Just HRefl <- eqTypeRep xF yF
 353 --  , Just HRefl <- eqTys xA yA
 354 --  = Just HRefl
 355 -- -- NOTE: 'TyFam' is expanded as much as possible.
 356 -- eqTy x@TyFam{} y = eqTy (expandFam x) y
 357 -- eqTy x y@TyFam{} = eqTy x (expandFam y)
 358
 359 -- * Type 'Tys'
 360 data Tys (as :: [Type]) prov vs (a :: aK) where
 361   TysZ :: Tys '[] prov vs a
 362   TysS :: Ty prov vs a -> Tys as prov vs b -> Tys (Proxy a ': as) prov vs b
 363 infixr 5 `TysS`
 364
 365 -- type instance SourceOf (Tys vs src ts) = src
 366 -- instance ConstsOf (Tys prov vs ts) where
 367 --  constsOf TysZ = Set.empty
 368 --  constsOf (TysS t ts) = constsOf t `Set.union` constsOf ts
 369 instance UsedVarsOf (Tys as) where
 370   usedVarsOf vs TysZ k = k vs
 371   usedVarsOf vs (TysS t ts) k =
 372     usedVarsOf vs t $ \vs' ->
 373       usedVarsOf vs' ts k
 374 instance VarOccursIn (Tys as) where
 375   varOccursIn _v TysZ = False
 376   varOccursIn v (TysS t ts) = varOccursIn v t Prelude.|| varOccursIn v ts
 377
 378 -- ** Type family 'FunArg'
 379 type family FunArg (fun :: Type) :: Type where
 380   FunArg (q #> f) = FunArg f
 381   FunArg (a -> b) = a
 382
 383 -- ** Type family 'FunRes'
 384 type family FunRes (fun :: Type) :: Type where
 385   FunRes (q #> f) = FunRes f
 386   FunRes (a -> b) = b
 387
 388 -- -- | Return, when the given 'Type' is a function,
 389 -- -- the argument of that function.
 390 -- unTyFun ::
 391 --  forall t src tys.
 392 --  SourceInj (TyVT src) src =>
 393 --  --Constable (->) =>
 394 --  Type src tys t ->
 395 --  Maybe ( Type src tys (FunArg t)
 396 --        , Type src tys (FunRes t) )
 397 -- unTyFun ty_ini = go ty_ini
 398 --   where
 399 --   go ::
 400 --    Type src tys x ->
 401 --    Maybe ( Type src tys (FunArg x)
 402 --          , Type src tys (FunRes x) )
 403 --   go (TyApp _ (TyApp _ (TyConst _ _ f) a) b)
 404 --    | Just HRefl <- proj_ConstKi @(K (->)) @(->) f
 405 --    = Just ((a `withSource` TyVT ty_ini), (b `withSource` TyVT ty_ini))
 406 --   go (TyApp _ (TyApp _ (TyConst _ _ f) _a) b)
 407 --    | Just HRefl <- proj_ConstKi @(K (#>)) @(#>) f
 408 --    = go b
 409 --   go TyApp{}   = Nothing
 410 --   go TyConst{} = Nothing
 411 --   go TyVar{}   = Nothing
 412 --   go TyFam{}   = Nothing
 413
 414 proj_ConstKi ::
 415   forall kc (c :: kc) u.
 416   Typeable c =>
 417   -- (kc ~ Type_of_Ty (Ty_of_Type kc)) =>
 418   -- KindInjP (Ty_of_Type kc) =>
 419   Const u ->
 420   Maybe (c :~~: u)
 421 proj_ConstKi = eqTypeRep (typeRep @c)
 422
 423 -- ** Type @(#>)@
 424
 425 -- | /Type constant/ to qualify a 'Type'.
 426 newtype (#>) (q :: Constraint) (a :: Type) = Qual (q => a)
 427
 428 -- | Qualify a 'Type'.
 429 (#>) :: Monoid prov => Ty prov vs q -> Ty prov vs t -> Ty prov vs (q #> t)
 430 (#>) q t =
 431   -- (tyConstLen @(K (#>)) @(#>) (lenVars q) `tyApp` q) `tyApp` t
 432   TyApp
 433     { tyAppFun =
 434         TyApp
 435           { tyAppFun = TyConst{tyConst = typeRep @(#>), tyConstLen = lenVar q}
 436           , tyAppArg = q
 437           }
 438     , tyAppArg = t
 439     }
 440
 441 infixr 0 #>
 442
 443 -- NOTE: should actually be (-1)
 444 -- to compose well with @infixr 0 (->)@
 445 -- but this is not allowed by GHC.
 446
 447 -- ** Class @(#)@
 448
 449 -- | 'Constraint' union.
 450 class ((x, y) :: Constraint) => x # y
 451
 452 instance ((x, y) :: Constraint) => x # y
 453
 454 -- | Unify two 'K.Constraint's.
 455 (#) :: Monoid prov => Ty prov vs qx -> Ty prov vs qy -> Ty prov vs (qx # qy)
 456 (#) a b =
 457   -- (tyConstLen @(K (#)) @(#) (lenVars a) `tyApp` a) `tyApp` b
 458   TyApp
 459     { tyAppFun =
 460         TyApp
 461           { tyAppFun = TyConst{tyConst = typeRep @(#), tyConstLen = lenVar a}
 462           , tyAppArg = a
 463           }
 464     , tyAppArg = b
 465     }
 466
 467 infixr 2 #
 468
 469 -- * Class 'KindOf'
 470 class KindOf (ty :: Prov -> [Type] -> aK -> Type) where
 471   -- | Return the kind of the given 'Var'.
 472   kindOf ::
 473     -- HasCallStack =>
 474     ProvenanceKindOf ty prov =>
 475     Show prov =>
 476     ty prov vs (a :: aK) ->
 477     Kind prov (aK :: Type)
 478
 479 instance KindOf Var where
 480   kindOf v@Var{varKind} = TyProv (provenanceKindOf v) varKind
 481 instance KindOf Ty where
 482   kindOf ty = TyProv (provenanceKindOf ty) (go ty)
 483     where
 484       go ::
 485         Show prov =>
 486         Ty prov vs (a :: aK) ->
 487         Kind prov (aK :: Type)
 488       go TyConst{tyConst = constType :: Const (a :: aK)} =
 489         tyOfTypeRep LenZ (typeRepKind constType)
 490       go TyApp{tyAppFun = f} = case go f of
 491         SkipTyProv
 492           TyApp
 493             { tyAppFun =
 494               SkipTyProv
 495                 TyApp
 496                   { tyAppFun = SkipTyProv TyConst{tyConst = eqTypeRep (typeRep @(->)) -> Just HRefl}
 497                   }
 498             , tyAppArg = k
 499             } -> k
 500         t -> Prelude.error $ "here: " <> show t
 501       go TyVar{..} = varKind tyVar
 502       go TyProv{..} = go tyUnProv
 503
 504 -- ** Class 'ProvenanceKindOf'
 505 class ProvenanceKindOf (ty :: Prov -> [Type] -> aK -> Type) prov where
 506   provenanceKindOf :: ty prov vs (a :: aK) -> prov
 507 instance ProvenanceKindOf ty () where
 508   provenanceKindOf _ = ()
 509 instance ProvenanceKindOf Ty String where
 510   provenanceKindOf = show
 511 instance ProvenanceKindOf Var String where
 512   provenanceKindOf = show
 513
 514 -- kindOf (TyFam _src _len fam _as) = kindOfConst fam