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