多元类型的应用是单射的吗？

Question

多类型应用是单射的吗？

当我们enable PolyKinds时，我们知道f a ~ g b意味着f ~ g和a ~ b吗？

动机

当时，我将问题减少到仅在启用 PolyKinds 时收到以下错误。

Could not deduce (c1 ~ c)
from the context ((a, c z) ~ (c1 a1, c1 b))

如果多类型应用是单射的，我们可以推导出c1 ~ c如下。

(a,   c z) ~ (c1 a1,   c1 b)
(a,) (c z) ~ (c1 a1,) (c1 b) {- switch to prefix notation -}
      c z  ~           c1 b  {- f a ~ g b implies a ~ b -}
      c    ~           c1    {- f a ~ g b implies f ~ g -}
      c1   ~           c     {- ~ is reflexive -}

类型应用是单射的

在Haskell中，类型应用是单射的。如果 f a ~ g b 则 f ~ g 和 a ~ b。我们可以通过编译以下内容来证明这一点

{-# LANGUAGE GADTs #-}

import Control.Applicative

second :: a -> a -> a
second _ = id

typeApplicationIsInjective :: (Applicative f, f a ~ g b) => f a -> g b -> f b
typeApplicationIsInjective fa gb = second <$> fa <*> gb

Kind类型应用不是单射的

类型应用的种类不是单射的。如果我们考虑以下内容，其中有种类 (* -> *) -> *.

newtype HoldingInt f = HoldingInt (f Int)

我们可以问 ghci something of kind (* -> *) -> * 应用于 something kind * -> * 时有什么类型，即 *

> :k HoldingInt
HoldingInt :: (* -> *) -> *
> :k Maybe
Maybe :: * -> *
> :k HoldingInt Maybe
HoldingInt Maybe :: *

This is the same kind as something of kind * -> * applied to something of kind *

> :k Maybe
Maybe :: * -> *
> :k Int
Int :: *
> :k Maybe Int
Maybe Int :: *

因此，借用 syntax from KindSignatures，第一组亲切签名在第二组中暗示任何东西是不正确的。

f :: kf, g :: kg, a :: ka, b :: kb, f a :: k, g b :: k
g :: kf, f :: kg, b :: ka, a :: kb

Answer 1

如果一个类型级别的应用程序有不同的种类，那么这两个类型不能被视为相等。这是证据：

GHC.Prim> () :: ((Any :: * -> *) Any) ~ ((Any :: (* -> *) -> *) Any) => ()
<interactive>:6:1:
    Couldn't match kind ‘*’ with ‘* -> *’
    Expected type: Any Any
      Actual type: Any Any
    In the expression:
        () :: ((Any :: * -> *) Any) ~ ((Any :: (* -> *) -> *) Any) => ()
    In an equation for ‘it’:
        it
          = () :: ((Any :: * -> *) Any) ~ ((Any :: (* -> *) -> *) Any) => ()

<interactive>:6:7:
    Couldn't match kind ‘*’ with ‘* -> *’
    Expected type: Any Any
      Actual type: Any Any
    In the ambiguity check for: Any Any ~ Any Any => ()
    To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
    In an expression type signature:
      ((Any :: * -> *) Any) ~ ((Any :: (* -> *) -> *) Any) => ()
    In the expression:
        () :: ((Any :: * -> *) Any) ~ ((Any :: (* -> *) -> *) Any) => ()

（即使打开建议的 AllowAmbiguousTypes 扩展也会出现相同的类型检查错误——只是没有建议。）

因此，如果两个类型可以被证明是相等的，那么等式两侧相同结构位置的类型级应用具有相同的种类。

如果您想要证明而不是证据，则需要写下关于 Type Checking with Open Type Functions 中描述的系统的仔细归纳证明。检查图 3 在我看来不变量 "all type applications in ~'s have the same kind on both sides of the ~" 被保留，尽管我和论文都没有仔细证明这一点，所以有可能不是这样。

Answer 2

Polykinded 类型的应用程序从外部是单射的，但从内部肯定不是单射的 Haskell。

"injective from the outside" 我的意思是只要有 Refl 类型 f a :~: g b，那么 f 一定等于 g 并且 a 等于 b，并且由于我们知道不同种类的类型永远不会相等，所以种类也必须相同。

问题是 GHC 只有同质类型等式约束，根本没有种类等式约束。使用强制对 GADT 进行编码的机制仅存在于类型和提升类型级别。这就是为什么我们不能表达异构平等，为什么我们不能促进 GADTs。

{-# LANGUAGE PolyKinds, GADTs, TypeOperators #-}

data HEq (a :: i) (b :: k) :: * where
  HRefl :: HEq a a
-- ERROR: Data constructor ‘HRefl’ cannot be GADT-like in its *kind* arguments

此外，这是一个 GHC 未推断单射性的简单示例：

sym1 :: forall f g a b. f a :~: g b -> g b :~: f a
sym1 Refl = Refl
-- ERROR: could not deduce (g ~ f), could not deduce (b ~ a)

如果我们用相同的类型注释 a 和 b，它会检出。

This paper 讨论了上述限制以及如何在 GHC 中消除它们（他们描述了一个具有统一 kind/type 强制和异构平等约束的系统）。

多元类型的应用是单射的吗？

Is polykinded type application injective?

haskell

higher-kinded-types

type-kinds

polykinds

多类型应用是单射的吗？

动机

类型应用是单射的

Kind类型应用不是单射的