Haskell的PolyKinds扩展和类型族

Question

我正在研究Haskell中的类型族，尝试同时使用多态种类和类型族。

例如，文件开头有以下语言扩展（文件中稍后会显示更多内容）：

{-# LANGUAGE TypeFamilies,
StandaloneKindSignatures,
RankNTypes,
PolyKinds,
DataKinds,
TypeOperators,
TypeApplications,
KindSignatures,
ScopedTypeVariables,
UndecidableInstances,
MultiParamTypeClasses,
AllowAmbiguousTypes #-}

我在类型声明中使用了多态种类：

data Proxy (a :: k) = Proxy

这个功能很好用。但是当我试图在更丰富的类型族定义中使用它们时：

type family PK (a :: k) :: Type where
  PK Int = Char

GHC 抛出了一个错误:

• Expected kind ‘k’, but ‘Int’ has kind ‘*’
• In the first argument of ‘PK’, namely ‘Int’
  In the type family declaration for ‘PK’.

这个问题有解决方法吗？GHC版本是8.10.7。提前感谢任何想法和帮助。

- A. G

Answer 1

我建议您使用StandaloneKindSignatures：

..
{-# Language StandaloneKindSignatures #-}

type Id :: k -> k
type Id a = a

type Proxy :: k -> Type
data Proxy a = Proxy

type
  PK :: k -> Type
type family
  PK a where
  PK Int = Char

kind参数在类型族PK @Type Int = Char中是隐式的，但您可以显式地编写它（需要TypeApplications）。

使用GADTs，您可以编写Proxy。

type Proxy :: k -> Type
data Proxy a where
  Proxy :: Proxy @k a

有提议允许在声明头中使用可见的（kind）应用程序：

type Id :: k -> k
type Id @k a = a

type Proxy :: k -> Type
data Proxy @k a = Proxy

type
  PK :: k -> Type
type family
  PK @k    a where
  PK @Type Int = Char

我们可以在具有forall->而不是（隐式）不可见的forall的种类中使用“可见依赖量词”。

type Id :: forall k -> k -> k
type Id k a = a

type Proxy :: forall k -> k -> Type
data Proxy k a = Proxy

type
  PK :: forall k -> k -> Type
type family
  PK k    a where
  PK Type Int = Char

---

Proxy的区别在于它是定义为统一数据类型（非GADT或者俚语：“传统”语法）还是一个GADT。它们是等价的（在旧版本的GHC 8.10上进行了测试），除了k之外。

• (forall.)指定的=可以使用TypeApplications来指定, 如果未指定，将自动推断。
• (forall{}.)推断的=TypeApplications跳过它，不能直接指定。

这适用于类型构造函数Proxy和命名为P的数据构造函数，因为两者都是多态的。Proxy可以通过量化k的方式来指定Proxy @Nat 42或推断Proxy 42。

Proxy :: forall (k :: Type). k -> Type
-- or
Proxy :: forall {k :: Type}. k -> Type

根据 P 中的量化方式，可以指定 k 为 P @Nat @42 或推断为 P @42：

P :: forall {k :: Type} (a :: k). Proxy @k a
P :: forall {k :: Type} (a :: k). Proxy    a
-- or
P :: forall (k :: Type) (a :: k). Proxy @k a
P :: forall (k :: Type) (a :: k). Proxy    a

这会产生几个结果

• k 在两者中推断出来: P @42 :: 代理 42 (P @42 :: 代理 42)

data Proxy a = P
--
data Proxy a where
 P :: Proxy a

• k 在 Proxy 中被指定但在 P 中被推断出来 (P @42 :: Proxy @Nat 42)

data Proxy (a :: k) where
 P :: Proxy a
--
type Proxy :: k -> Type
data Proxy a where
  P :: Proxy a

• 在Proxy和P中都指定了k（P @Nat @42 :: Proxy @Nat 42）

data Proxy (a :: k) = P
--
type Proxy :: k -> Type
data Proxy a = P
--
type Proxy :: forall k. k -> Type
data Proxy a = P
--
type Proxy :: forall k. k -> Type
data Proxy (a :: k) = P
--
type Proxy :: k -> Type
data Proxy a where
 P :: Proxy @k a

我正在等待许多与量化和范围有关的新变化定型，这可能已经过时了。

- Iceland_jack

---

考虑以相同的方式编写类型族和数据类型，这是一个不错的解决方案，它可以更好地控制隐式细节。此外，GAD扩展也非常有用。还有一件事：Id类型同义词是否可以等效地转换为类型族？ - A. G

你可以将其写成 type family Id a where Id a = a，并使用相同的类型签名。我相信这是等效的，但要注意类型族可能会有微妙之处（请参见关于类型族的元数）。 - Iceland_jack

顺便问一下，使用GADTs扩展定义的Proxy数据类型是否等同于简单定义的（没有先定义其种类）：data Proxy a = Proxy？ - A. G

我尝试了不同的变体，请参见答案末尾。 - Iceland_jack

类型变量的隐含绑定（implicitly bound）发生了相当令人困惑的变化。我有点迷失了。 - dfeuer

@Iceland_jack，你对隐式和显式类型的问题进行了非常清晰的解释，因为我在编程时遇到了指定它们的问题，但是没有看到错误的原因。 - A. G

Answer 2

你只需要再添加一个语言扩展即可。如果你也启用了 CUSKs 扩展，那么你所写的代码将会实现你想要的功能。

- Joseph Sible-Reinstate Monica