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