symantic/Language/Symantic/Typing/Quantification.hs

   1 {-# LANGUAGE TypeInType #-}
   2 {-# LANGUAGE UndecidableInstances #-}
   3 {-# LANGUAGE ViewPatterns #-}
   4 module Language.Symantic.Typing.Quantification where
   5
   6 import Data.Map.Strict (Map)
   7 import Data.Set (Set)
   8 import qualified Control.Monad.Trans.State.Strict as SS
   9 import qualified Data.Map.Strict as Map
  10 import qualified Data.Set as Set
  11
  12 import Language.Symantic.Helper.Data.Type.Equality
  13 import Language.Symantic.Parsing
  14 import Language.Symantic.Typing.Constant
  15 import Language.Symantic.Typing.Kind
  16 import Language.Symantic.Typing.Type
  17
  18 -- | /type beta-reduction/: substitute the abstraction
  19 -- of a 'TyQuant' by using the given argument, when possible.
  20 unTyQuant :: Type src ctx ss cs (a::ka) -> Type src ctx ss cs b -> Maybe (KT src ctx ss cs ka)
  21 unTyQuant (TyQuant _src _ kv f) v
  22  | Just Refl <- eqKi kv (kindTyOS v)
  23  = Just (f v)
  24 unTyQuant _f _v = Nothing
  25 infixl 2 `unTyQuant`
  26
  27 -- | Monomorphize given 'Type':
  28 -- introduce new 'TyVar's to remove rank-1 'TyQuant's.
  29 monoTy :: Monad m
  30  => Type src ctx ss cs (h::k)
  31  -> SS.StateT Var m (KT src ctx ss cs k)
  32 monoTy t@TyConst{}          = return $ KT t
  33 monoTy t@(TyApp _src _f _a) = return $ KT t
  34 monoTy (TyQuant src _n kv f) = do
  35         v <- SS.get
  36         SS.put $ v + 1
  37         case f $ TyVar src kv v of
  38          KT t -> monoTy t
  39 monoTy t@TyVar{} = return $ KT t
  40 monoTy t@(TyFam _src _f _hs) = return $ KT t
  41 monoTy (Term x te) =
  42         monoTy x >>= \case
  43          KT t | Just Refl <- eqTy x t -> return $ KT $ Term t te
  44          t -> return t
  45
  46 -- * Type 'MapTyVar'
  47 -- | /type variable substitution/
  48 type MapTyVar src ctx ss cs = Map Var (EType src ctx ss cs)
  49
  50 -- | Substitute the 'TyQuant's of the given 'Type',
  51 -- according to the given 'MapTyVar',
  52 -- where their associated 'Var' counts from the given 'Var'.
  53 substTyQuant :: forall src ctx ss cs k h.
  54  Var -> MapTyVar src ctx ss cs
  55  -> Type src ctx ss cs (h::k)
  56  -> KT   src ctx ss cs k
  57 substTyQuant var vs = go var
  58         where
  59         go :: forall kx x. Var -> Type src ctx ss cs (x::kx) -> KT src ctx ss cs kx
  60         go _v t@TyConst{} = KT t
  61         go v (TyApp src f a) = bind2KT (\f' a' -> KT $ TyApp src f' a') (go v f) (go v a)
  62         go v (TyQuant src n kv f) =
  63                 case Map.lookup v vs of
  64                  Just (EType TyVar{}) -> KT $ TyQuant src n kv $ bindKT (go (v + 1)) . f
  65                  Just (EType r) | Just Refl <- eqKi kv (kindTyOS r) -> bindKT (go (v + 1)) $ f r
  66                  Just{} -> error "[BUG] substTyQuant: expected and actual kinds mismatch"
  67                  Nothing -> KT $ TyQuant src n kv $ bindKT (go (v + 1)) . f
  68         go _v t@TyVar{} = KT t
  69         go v (TyFam src f hs) = goArgs v hs $ \hs' -> KT $ TyFam src f hs'
  70                 where
  71                 goArgs :: forall hs ret. Var
  72                  -> Types src ctx ss cs hs
  73                  -> (forall hs'. Types src ctx ss cs hs' -> ret)
  74                  -> ret
  75                 goArgs _v TypesZ k = k TypesZ
  76                 goArgs v' (TypesS h as) k =
  77                         case go v' h of
  78                          KT h' -> goArgs v' as $ \as' -> k $ TypesS h' as'
  79         go v (Term x te) =
  80                 case go v x of
  81                  KT t | Just Refl <- eqTy x t -> KT $ Term t te -- FIXME: likely useless
  82                  t -> t
  83
  84 -- | Substitute the 'TyVar's of the given 'Type',
  85 -- according to the given 'MapTyVar'.
  86 substTyVar
  87  :: forall src ctx ss cs k (h::k).
  88     MapTyVar src ctx ss cs
  89  -> Type src ctx ss cs h
  90  -> KT   src ctx ss cs k
  91 substTyVar vs = go
  92         where
  93         go :: forall kx x. Type src ctx ss cs (x::kx) -> KT src ctx ss cs kx
  94         go (TyQuant src n kv f) = KT $ TyQuant src n kv $ bindKT go . f
  95         go (TyApp src f a) = bind2KT (\f' a' -> KT $ TyApp src f' a') (go f) (go a)
  96         go t@TyConst{} = KT t
  97         go t@(TyVar _src kv v) =
  98                 case Map.lookup v vs of
  99                  Nothing -> KT t
 100                  Just (EType x) | Just Refl <- eqKi kv (kindTyOS x) -> KT x
 101                  Just{} -> error "[BUG] substTyVar: expected and actual kinds mismatch"
 102         go (TyFam src f hs) = goArgs hs $ \hs' -> KT $ TyFam src f hs'
 103                 where
 104                 goArgs :: forall hs ret.
 105                     Types src ctx ss cs hs
 106                  -> (forall hs'. Types src ctx ss cs hs' -> ret)
 107                  -> ret
 108                 goArgs TypesZ k = k TypesZ
 109                 goArgs (TypesS h as) k =
 110                         case go h of
 111                          KT h' -> goArgs as $ \as' -> k $ TypesS h' as'
 112         go (Term x te) =
 113                 case go x of
 114                  KT t | Just Refl <- eqTy x t -> KT $ Term t te -- FIXME: likely useless
 115                  t -> t
 116
 117 -- | Change the 'TyVar's of the given 'Type' matching the first 'Var', to the second.
 118 --
 119 -- NOTE: This is special case of 'substTyVar'
 120 -- in which the indexed type can be preserved.
 121 changeTyVar :: Var -> Var -> Type src ctx ss cs (h::k) -> Type src ctx ss cs (h::k)
 122 changeTyVar ov nv = go
 123         where
 124         go :: Type src ctx ss cs (h::k) -> Type src ctx ss cs (h::k)
 125         go t@TyConst{} = t
 126         go (TyApp src f a) = TyApp src (go f) (go a)
 127         go (TyQuant src n kv f) = TyQuant src n kv $ mapKT go . f
 128         go t@(TyVar src kv v) | v == ov = TyVar src kv nv -- matching Var
 129                               | otherwise = t
 130         go (TyFam src f hs) = TyFam src f $ go `mapTys` hs
 131         go (Term x te) = Term (go x) te
 132
 133 -- | Unify two 'MapTyVar'.
 134 --
 135 -- NOTE: the union is left-biased: in case of duplicate 'Var',
 136 -- it keeps those from the first 'MapTyVar' given.
 137 --
 138 -- NOTE: the first 'MapTyVar' given is applied to the second (with 'substTyVar'),
 139 -- this way each 'Var' directly maps to an expanded 'Type',
 140 -- so that, when using the resulting 'MapTyVar',
 141 -- there is no need to apply it multiple times
 142 -- until there is no more substitution to be done.
 143 unionSubst :: MapTyVar src ctx ss cs -> MapTyVar src ctx ss cs -> MapTyVar src ctx ss cs
 144 unionSubst x y = x `Map.union` ((\(EType t) -> EType `ofKT` substTyVar x t) <$> y)
 145
 146 -- | Return the smallest 'Var' not used in given 'Type'.
 147 freeTyVar :: Type src ctx ss cs (h::k) -> Var
 148 freeTyVar = (+ 1) . maxTyVar (-1)
 149         where
 150         maxTyVar :: Var -> Type src ctx ss cs h -> Var
 151         maxTyVar m TyConst{}             = m
 152         maxTyVar m (TyApp   _src f a)    = maxTyVar m f `max` maxTyVar m a
 153         maxTyVar m (TyQuant src _n kv f) = maxTyVar m `ofKT` f (TyVar src kv (-1))
 154         maxTyVar m (TyVar   _src _kv v)  = max m $ if v < 0 then -1 else v + 1
 155         maxTyVar m (TyFam _src _f as)    = foldrTys (flip maxTyVar) as m
 156         maxTyVar m (Term x _te)          = maxTyVar m x
 157
 158 -- | Return the 'Var' of the 'TyVar's in given 'Type'.
 159 freeTyVars :: Type src ctx ss cs (h::k) -> Set Var
 160 freeTyVars = go
 161         where
 162         go :: Type src ctx ss cs h -> Set Var
 163         go TyConst{} = Set.empty
 164         go (TyApp _src f a) = go f `Set.union` go a
 165         go (TyQuant  src _n kv f) = go `ofKT` f (TyVar src kv (-1))
 166         go (TyVar _src _kv v) | v < 0     {- bound Var -} = Set.empty
 167                               | otherwise {- free  Var -} = Set.singleton v
 168         go (TyFam _src _f as) = foldrTys (\h acc -> Set.union acc $ go h) as Set.empty
 169         go (Term x _te) = go x
 170
 171 -- | Like 'freeTyVars', but also return the 'Kind' of each 'Var'.
 172 freeKiTyVars :: Type src ctx ss cs (h::k) -> Map Var (EKind src)
 173 freeKiTyVars = go
 174         where
 175         go :: Type src ctx ss cs h -> Map Var (EKind src)
 176         go TyConst{} = Map.empty
 177         go (TyApp _src f a) = go f `uni` go a
 178         go (TyQuant  src _n kv f) = go `ofKT` f (TyVar src kv (-1))
 179         go (TyVar _src kv v) | v < 0     {- bound Var -} = Map.empty
 180                              | otherwise {- free  Var -} = Map.singleton v (EKind kv)
 181         go (TyFam _src _f as) = foldrTys (\h acc -> uni acc $ go h) as Map.empty
 182         go (Term x _te) = go x
 183
 184         uni :: Map Var (EKind src) -> Map Var (EKind src) -> Map Var (EKind src)
 185         uni = Map.unionWith $ \new@(EKind kx) (EKind ky) ->
 186                 case eqKi kx ky of
 187                  Just{} -> new
 188                  Nothing -> error "[BUG] freeKiTyVars: inconsistent kinds"
 189
 190 {-
 191 -- | Remove 'TyQuant's binding a type variable which is not used.
 192 cleanTyQuants :: Type src ctx ss cs (h::k) -> Type src ctx ss cs (h::k)
 193 cleanTyQuants t = go (freeTyVar t) t
 194         where
 195         go :: Var -> Type src ctx ss cs (h::k) -> Type src ctx ss cs (h::k)
 196         go v (TyQuant src n kv f) =
 197                 let x = f $ TyVar src kv v in
 198                 if v `elem` freeTyVars x
 199                 then TyQuant src n kv $ go (v + 1) . f
 200                 else x
 201         go _v x@TyConst{}     = x
 202         go _v x@TyVar{}       = x
 203         go v (TyApp src f a)  = TyApp src (go v f) (go v a)
 204         go v (Term x te)    = Term (go v x) te
 205 -}
 206
 207 -- ** Type 'Error_MGU'
 208 -- | Reasons why two 'Type's cannot be unified.
 209 data Error_MGU src ss cs
 210  =   Error_MGU_TyVar_Loop Var (EType src '[] ss cs)
 211      -- ^ /occurence check/: a 'TyVar' is unified with a 'Type'
 212      --   which contains this same 'TyVar'.
 213  |   Error_MGU_TyConst_mismatch (EType src '[] ss cs) (EType src '[] ss cs)
 214      -- ^ Two 'TyConst's should be the same, but are different.
 215  |   Error_MGU_Kind_mismatch (EKind src) (EKind src)
 216      -- ^ Two 'Kind's should be the same, but are different.
 217  |   Error_MGU_Kind (Con_Kind src)
 218      -- ^ Two 'Kind's mismatch.
 219  |   Error_MGU_cannot_unify (EType src '[] ss cs) (EType src '[] ss cs)
 220      -- ^ Cannot unify those two 'Type's.
 221 deriving instance
 222  ( Eq src
 223  , Eq_Token ss
 224  , Inj_Source (EType src '[] ss cs) src
 225  ) => Eq (Error_MGU src ss cs)
 226 deriving instance
 227  ( Show src
 228  , Show_TyConst cs
 229  , Show (EType src '[] ss cs)
 230  , Fixity_TyConst cs
 231  ) => Show (Error_MGU src ss cs)
 232
 233 instance Inj_Error (Error_MGU src ss cs) (Error_MGU src ss cs) where
 234         inj_Error = id
 235 instance Inj_Error (Con_Kind src) (Error_MGU src ss cs) where
 236         inj_Error = Error_MGU_Kind
 237
 238 -- | Return the /most general unification/ of two 'Type's, when it exists.
 239 --
 240 -- Support:
 241 --
 242 --  * 'TyConst' : OK
 243 --  * 'TyApp'   : OK
 244 --  * 'TyQuant' : Error_MGU_cannot_unify
 245 --  * 'TyVar'   : OK
 246 --  * 'Term'    : Transparent
 247 mguTy
 248  :: forall src ctx ss cs ki a b.
 249     Inj_Source (EType src '[] ss cs) src
 250  => MapTyVar src ctx ss cs
 251  -> Type src ctx ss cs (a::ki)
 252  -> Type src ctx ss cs (b::ki)
 253  -> Either (Error_MGU src ss cs) (MapTyVar src ctx ss cs)
 254 mguTy = go
 255         where
 256         go
 257          :: MapTyVar src ctx ss cs
 258          -> Type src ctx ss cs (x::k)
 259          -> Type src ctx ss cs (y::k)
 260          -> Either (Error_MGU src ss cs) (MapTyVar src ctx ss cs)
 261         go vs x y =
 262                 let ki = kindTyOS x in
 263                 case (spineTy x, spineTy y) of
 264                  ((EType (unTerms -> hx), px), (EType (unTerms -> hy), py)) ->
 265                         case (hx, hy) of
 266                          (TyVar _ kvx vx, _) | Just Refl <- eqKi kvx ki -> goVar vs kvx vx y
 267                          (_, TyVar _ kvy yv) | Just Refl <- eqKi ki kvy -> goVar vs kvy yv x
 268                          (TyConst _sx cx, TyConst _sy cy)
 269                           | Just KRefl <- eqKiTyConst cx cy -> goList vs px py
 270                           | otherwise -> Left $ inj_Error $
 271                                 Error_MGU_TyConst_mismatch (EType hx) (EType hy)
 272                          _ ->
 273                                 case (unTerm x, unTerm y) of
 274                                  (TyApp _ ax bx, TyApp _ ay by) ->
 275                                         goList vs
 276                                          [EType ax, EType bx]
 277                                          [EType ay, EType by]
 278                                  _ -> Left $ inj_Error $
 279                                         Error_MGU_cannot_unify
 280                                          (EType $ unCtxTe x)
 281                                          (EType $ unCtxTe y)
 282         goVar
 283          :: MapTyVar src ctx ss cs
 284          -> Kind src k
 285          -> Var
 286          -> Type src ctx ss cs (y::k)
 287          -> Either (Error_MGU src ss cs) (MapTyVar src ctx ss cs)
 288         goVar vs xkv xv y =
 289                 case Map.lookup xv vs of
 290                  Just (EType x) -> if_EqKind xkv (kindTyOS x) $ \Refl -> go vs y x
 291                  Nothing ->
 292                         case substTyVar vs y of
 293                          KT (TyVar _src _ykv yv) | xv == yv -> Right vs
 294                          KT y' | xv `elem` freeTyVars y' -> Left $ Error_MGU_TyVar_Loop xv (EType $ unCtxTe y')
 295                                | otherwise -> Right $ Map.singleton xv (EType y') `unionSubst` vs
 296         goList
 297          :: MapTyVar src ctx ss cs
 298          -> [EType src ctx ss cs]
 299          -> [EType src ctx ss cs]
 300          -> Either (Error_MGU src ss cs) (MapTyVar src ctx ss cs)
 301         goList vs [] [] = Right vs
 302         goList vs (EType x:xs) (EType y:ys) =
 303                 if_EqKind (kindTy x) (kindTy y) $ \Refl ->
 304                 go vs x y >>= \vs' -> goList vs' xs ys
 305         goList _vs _x _y = error "[BUG] mguTy: kinds mismatch"
 306
 307 -- | Return the left spine of a 'Type':
 308 -- the root 'Type' and its 'Type' parameters,
 309 -- from the left to the right.
 310 spineTy
 311  :: forall src ctx ss cs k h.
 312     Inj_Source (EType src '[] ss cs) src
 313  => Type src ctx ss cs (h::k)
 314  -> (EType src ctx ss cs, [EType src ctx ss cs])
 315 spineTy typ = go [] typ
 316         where
 317         go :: forall x. Inj_Source (EType src '[] ss cs) src
 318            => [EType src ctx ss cs]
 319            -> Type src ctx ss cs x
 320            -> (EType src ctx ss cs, [EType src ctx ss cs])
 321         go ts (TyApp  _src f a) = go (EType (a `source` EType (unCtxTe typ)) : ts) f
 322         go ts (Term x _te) = go ts x
 323         go ts t = (EType (t `source` EType (unCtxTe typ)), ts)
 324 {-
 325 spineTy
 326  :: Type src ctx ss cs (h::k)
 327  -> (forall kx (x::kx) xs. Type src ctx ss cs x -> Types src ctx ss cs xs -> ret)
 328  -> ret
 329 spineTy = go TypesZ
 330         where
 331         go :: Types src ctx ss cs hs
 332            -> Type src ctx ss cs (h::k)
 333            -> (forall kx (x::kx) xs. Type src ctx ss cs x -> Types src ctx ss cs xs -> ret)
 334            -> ret
 335         go ts (TyApp  _src f a) k = go (a `TypesS` ts) f k
 336         go ts (Term x _te)    k = go ts x k
 337         go ts (TyAny x)       k = go ts x k
 338         go ts t k = k t ts
 339 -}
 340
 341 -- | Return, when the given 'Type' is a function,
 342 -- the argument of that function.
 343 unTyFun :: forall src ctx ss cs h.
 344  Inj_Source (EType src '[] ss cs) src
 345  => Proj_TyConst cs (->)
 346  => Type src ctx ss cs h -> Maybe (KTerm src ctx ss cs, KTerm src ctx ss cs)
 347 unTyFun t = go t
 348         where
 349         go :: forall x. Type src ctx ss cs x -> Maybe (KTerm src ctx ss cs, KTerm src ctx ss cs)
 350         go (TyApp _ (TyApp _ (TyConst _ f) a) b)
 351          | Just KRefl <- proj_TyConstKi @_ @(->) f
 352          = Just (KT (a `source` EType (unCtxTe t)), KT (b `source` EType (unCtxTe t)))
 353         go TyApp{}      = Nothing
 354         go TyConst{}    = Nothing
 355         go TyQuant{}    = Nothing
 356         go TyVar{}      = Nothing
 357         go TyFam{}      = Nothing
 358         go (Term x _te) = go x
 359
 360 -- | Return given 'Type', polymorphized by 'TyQuant'ifying
 361 -- over the given 'Var' of given 'Kind' and 'NameHint'.
 362 polyTyVar :: forall src ctx ss cs kv h.
 363  Source src
 364  => Show_TyConst cs
 365  => Proj_TyConst cs (->)
 366  => Proj_TyConst cs (#>)
 367  => NameHint -> Kind src kv -> Var
 368  -> Type src ctx ss cs (h::k)
 369  -> KT src ctx ss cs k
 370 polyTyVar nv kv var typ =
 371         KT $ TyQuant (source_of typ) nv kv $
 372         go var typ
 373         where
 374         go :: forall km (m::km).
 375             Var
 376          -> Type src ctx ss cs m
 377          -> (forall (v::kv). Type src ctx ss cs v -> KT src ctx ss cs km)
 378         go _v m@TyConst{} _a = KT m
 379         go v (TyApp src x y) a =
 380                 bind2KT
 381                  (\f' a' -> KT $ TyApp src f' a')
 382                  (go v x a)
 383                  (go v y a)
 384         go v (TyQuant src n kv' f) a =
 385                 KT $ TyQuant src n kv' $ \a' ->
 386                         (\p -> go v p a) `ofKT` f a'
 387         go v (TyVar _src kv' v') a | v == v' =
 388                 case eqKi kv kv' of
 389                  Nothing -> error "[BUG] polyTyVar: polymorphized TyVar has not expected kind"
 390                  Just Refl -> KT a
 391         go _v m@TyVar{} _a = KT m
 392         go v (TyFam src f hs) a =
 393                 goArgs hs $ \hs' -> KT $ TyFam src f hs'
 394                 where
 395                 goArgs :: forall hs ret.
 396                     Types src ctx ss cs hs
 397                  -> (forall hs'. Types src ctx ss cs hs' -> ret)
 398                  -> ret
 399                 goArgs TypesZ k = k TypesZ
 400                 goArgs (TypesS h as) k =
 401                         case go v h a of
 402                          KT h' -> goArgs as $ \as' -> k $ TypesS h' as'
 403         go v (Term m te) a =
 404                 case go v m a of
 405                  KT p
 406                   | TyVar _ _ka va <- a
 407                   , m' <- changeTyVar v va m
 408                   , Just Refl <- eqTy m' p ->
 409                         KT $ Term p te
 410                         -- NOTE: if @a@ is also a 'TyVar',
 411                         -- the indexed type can be preserved
 412                         -- and thus the 'Term' can be preserved too.
 413                         -- However, the old @v@ used to polymorphize
 414                         -- must be changed to the new @va@
 415                         -- to make 'eqTy' succeed.
 416                         -- Hence, the 'Term' can survive cycles
 417                         -- of 'monoTy' then 'polyTy'.
 418                         -- Because @freeTyVars p == freeTyVars m \\ v@,
 419                         -- @va@ should never be within @freeTyVars m@,
 420                         -- unless it again is @v@.
 421                  KT p -> KT p
 422
 423 -- | Polymorphize given 'Type':
 424 -- applying successively 'polyTyVar'
 425 -- for all 'freeTyVars' of given 'Type'.
 426 polyTy
 427  :: Source src
 428  => Show_TyConst cs
 429  => Proj_TyConst cs (->)
 430  => Proj_TyConst cs (#>)
 431  => Type src ctx ss cs (h::k)
 432  -> KT src ctx ss cs k
 433 polyTy t =
 434         let fvs = freeKiTyVars t in
 435         Map.foldrWithKey
 436          (\v (EKind kv) (KT x) ->
 437                 polyTyVar "" kv v x)
 438          (KT t) fvs