7

polykinded 类型的应用程序是单射的吗？

当我们启用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，(* -> *) -> *当应用于某种类型时，某种类型的东西有什么类型* -> *，即*

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

这与* -> *应用于某种事物的某种事物相同*

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

因此，从 借用语法KindSignatures，第一组种类签名暗示第二组中的任何内容是不正确的。

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

2 回答 2

6

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

所谓“外射”，我的意思是只要有一个Reflwith 类型f a :~: g b，那么它一定f是等于g和a等于b相同。

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

{-# 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它就会检查出来。

本文讨论了上述限制以及如何在 GHC 中消除它们（它们描述了一个具有统一种类/类型强制和异构平等约束的系统）。

于 2015-01-16T21:28:46.133 回答
5

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

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扩展也会产生相同的类型检查错误——只是没有建议。）

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

如果您希望证明而不是证据，则需要写下关于使用开放类型函数进行类型检查中描述的系统的仔细归纳证明。对图 3 的检查表明，不变量“~ 中的所有类型应用程序在 ~ 的两侧都有相同的类型”被保留了，尽管我和论文都没有仔细证明这一点，所以有一些机会是不是这样。

于 2015-01-16T21:08:18.233 回答