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  , Fixity_TyConst cs
 187  ) => Show (Error_MGU src cs)
 188
 189 instance Inj_Error (Error_MGU src cs) (Error_MGU src cs) where
 190         inj_Error = id
 191 instance Inj_Error (Con_Kind src) (Error_MGU src cs) where
 192         inj_Error = Error_MGU_Kind
 193
 194 -- | Return the /most general unification/ of two 'Type's, when it exists.
 195 --
 196 -- Support:
 197 --
 198 --  * 'TyConst' : OK
 199 --  * 'TyApp'   : OK
 200 --  * 'TyQuant' : Error_MGU_cannot_unify
 201 --  * 'TyVar'   : OK
 202 --  * 'Term'    : Transparent
 203 mguTy
 204  :: forall src cs ki a b.
 205     Inj_Source (EType src cs) src
 206  => MapTyVar src cs
 207  -> Type src cs (a::ki)
 208  -> Type src cs (b::ki)
 209  -> Either (Error_MGU src cs) (MapTyVar src cs)
 210 mguTy = go
 211         where
 212         go
 213          :: MapTyVar src cs
 214          -> Type src cs (x::k)
 215          -> Type src cs (y::k)
 216          -> Either (Error_MGU src cs) (MapTyVar src cs)
 217         go vs x y =
 218                 let ki = kindTyOS x in
 219                 let (xh, xp) = spineTy x in
 220                 let (yh, yp) = spineTy y in
 221                 case ( unTerm `mapEType` xh
 222                      , unTerm `mapEType` yh ) of
 223                  ( EType (TyVar _ xkv xv), _ ) | Just Refl <- eqKi xkv ki -> goVar vs xkv xv y
 224                  ( _, EType (TyVar _ ykv yv) ) | Just Refl <- eqKi ki ykv -> goVar vs ykv yv x
 225                  ( EType (TyConst _xs xc), EType (TyConst _ys yc) )
 226                   | Just KRefl <- eqKiTyConst xc yc -> goList vs xp yp
 227                   | otherwise -> Left $ inj_Error $ Error_MGU_TyConst_mismatch xh yh
 228                  _ ->
 229                         case (unTerm x, unTerm y) of
 230                          ( TyApp _ xa xb, TyApp _ ya yb ) ->
 231                                 goList vs
 232                                  [EType xa, EType xb]
 233                                  [EType ya, EType yb]
 234                          _ -> Left $ inj_Error $ Error_MGU_cannot_unify (EType x) (EType y)
 235         goVar
 236          :: MapTyVar src cs
 237          -> Kind src k
 238          -> Var
 239          -> Type src cs (y::k)
 240          -> Either (Error_MGU src cs) (MapTyVar src cs)
 241         goVar vs xkv xv y =
 242                 case Map.lookup xv vs of
 243                  Just (EType x) -> if_EqKind xkv (kindTyOS x) $ \Refl -> go vs y x
 244                  Nothing ->
 245                         case substTyVar vs y of
 246                          KT (TyVar _src _ykv yv) | xv == yv -> Right vs
 247                          KT y'
 248                           | xv `elem` freeTyVars y' -> Left $ Error_MGU_TyVar_Loop xv (EType y')
 249                           | otherwise -> Right $ Map.singleton xv (EType y') `unionSubst` vs
 250         goList
 251          :: MapTyVar src cs
 252          -> [EType src cs]
 253          -> [EType src cs]
 254          -> Either (Error_MGU src cs) (MapTyVar src cs)
 255         goList vs [] [] = Right vs
 256         goList vs (EType x:xs) (EType y:ys) =
 257                 if_EqKind (kindTy x) (kindTy y) $ \Refl ->
 258                 go vs x y >>= \vs' -> goList vs' xs ys
 259         goList _vs _x _y = error "[BUG] mguTy: kinds mismatch"
 260
 261 -- | Return the left spine of a 'Type':
 262 -- the root 'Type' and its 'Type' parameters,
 263 -- from the left to the right.
 264 spineTy
 265  :: forall src cs k h. Inj_Source (EType src cs) src
 266  => Type src cs (h::k)
 267  -> (EType src cs, [EType src cs])
 268 spineTy typ = go [] typ
 269         where
 270         go :: forall x. Inj_Source (EType src cs) src
 271            => [EType src cs]
 272            -> Type src cs x
 273            -> (EType src cs, [EType src cs])
 274         go ts (TyApp  _src f a) = go (EType (a `source` EType typ) : ts) f
 275         go ts (Term _te x) = go ts x
 276         go ts t = (EType (t `source` EType typ), ts)
 277 {-
 278 spineTy
 279  :: Type src cs (h::k)
 280  -> (forall kx (x::kx) xs. Type src cs x -> Types src cs xs -> ret)
 281  -> ret
 282 spineTy = go TypesZ
 283         where
 284         go :: Types src cs hs
 285            -> Type src cs (h::k)
 286            -> (forall kx (x::kx) xs. Type src cs x -> Types src cs xs -> ret)
 287            -> ret
 288         go ts (TyApp  _src f a) k = go (a `TypesS` ts) f k
 289         go ts (Term _te x)    k = go ts x k
 290         go ts (TyAny x)         k = go ts x k
 291         go ts t k = k t ts
 292 -}
 293
 294 -- | Return, when the given 'Type' is a function,
 295 -- the argument of that function.
 296 unTyFun :: forall src cs h.
 297  Inj_Source (EType src cs) src
 298  => Proj_TyConst cs (->)
 299  => Type src cs h -> Maybe (KTerm src cs, KTerm src cs)
 300 unTyFun t = go t
 301         where
 302         go :: forall x. Type src cs x -> Maybe (KTerm src cs, KTerm src cs)
 303         go (TyApp _ (TyApp _ (TyConst _ f) a) b)
 304          | Just KRefl <- proj_TyConstKi @_ @(->) f
 305          = Just (KT (a `source` EType t), KT (b `source` EType t))
 306         go TyApp{}   = Nothing
 307         go TyConst{} = Nothing
 308         go TyQuant{} = Nothing
 309         go TyVar{}   = Nothing
 310         go (Term _te x) = go x
 311
 312 -- | Return given 'Type', polymorphized by 'TyQuant'ifying
 313 -- over the given 'Var' of given 'Kind' and 'NameHint'.
 314 polyTyVar :: forall src cs kv h.
 315  Source src
 316  => Show_TyConst cs
 317  => Proj_TyConst cs (->)
 318  => Proj_TyConst cs (#>)
 319  => NameHint -> Kind src kv -> Var
 320  -> Type src cs (h::k)
 321  -> KT src cs k
 322 polyTyVar nv kv var typ =
 323         KT $ TyQuant (source_of typ) nv kv $
 324         go var typ
 325         where
 326         go :: forall km (m::km).
 327             Var
 328          -> Type src cs m
 329          -> (forall (v::kv). Type src cs v -> KT src cs km)
 330         go _v m@TyConst{} = \_a -> KT m
 331         go v (TyApp src x y) = \a ->
 332                 bind2KT
 333                  (\f' a' -> KT $ TyApp src f' a')
 334                  (go v x a)
 335                  (go v y a)
 336         go v (TyQuant src n kv' f) = \a ->
 337                 KT $ TyQuant src n kv' $ \a' ->
 338                         (\p -> go v p a) `ofKT` f a'
 339         go v (TyVar _src kv' v') | v == v' =
 340                 case eqKi kv kv' of
 341                  Nothing -> error "[BUG] polyTyVar: polymorphized TyVar has not expected kind"
 342                  Just Refl -> KT
 343         go _v m@TyVar{} = \_a -> KT m
 344         go v (Term te m) = \a ->
 345                 case go v m a of
 346                  KT p
 347                   | TyVar _ _ka va <- a
 348                   , m' <- changeTyVar v va m
 349                   , Just Refl <- eqTy m' p ->
 350                         KT $ Term te p
 351                         -- NOTE: if @a@ is also a 'TyVar',
 352                         -- the indexed type can be preserved
 353                         -- and thus the 'Term' can be preserved too.
 354                         -- However, the old @v@ used to polymorphize
 355                         -- must be changed to the new @va@
 356                         -- to make 'eqTy' succeed.
 357                         -- Hence, the 'Term' can survive cycles
 358                         -- of 'monoTy' then 'polyTy'.
 359                         -- Because @freeTyVars p == freeTyVars m \\ v@,
 360                         -- @va@ should never be within @freeTyVars m@,
 361                         -- unless it again is @v@.
 362                  KT p -> KT p
 363
 364 -- | Polymorphize given 'Type':
 365 -- applying successively 'polyTyVar'
 366 -- for all 'freeTyVars' of given 'Type'.
 367 polyTy
 368  :: Source src
 369  => Show_TyConst cs
 370  => Proj_TyConst cs (->)
 371  => Proj_TyConst cs (#>)
 372  => Type src cs (h::k)
 373  -> KT src cs k
 374 polyTy t =
 375         let fvs = freeKiTyVars t in
 376         Map.foldrWithKey
 377          (\v (EKind kv) (KT x) ->
 378                 polyTyVar "" kv v x)
 379          (KT t) fvs