Haskell PolyKinds 扩展和类型族

Posted 2023-03-15

【中文标题】Haskell PolyKinds 扩展和类型族

【英文标题】：Haskell PolyKinds extension and type families

【发布时间】：2022-01-10 02:14:04

【问题描述】：

我在 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。提前感谢您的任何想法和帮助。

【参考方案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）。

使用 GADT，您可以编写 Proxy

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

有建议允许在声明头中显示（种类）应用程序：

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。除了 k 是

之外，它们是等效的（在旧的 GHC 8.10 上测试） (forall.) 指定= 可以用TypeApplications 指定，但如果不指定会自动推断 (forall.) inferred = TypeApplications 跳过，不能直接指定

这适用于类型构造函数Proxy 和名为P 的数据构造函数以消除歧义，因为它们都是多态的。 Proxy可以指定Proxy @Nat 42或者根据k的量化推断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 :: Proxy 42 (P @42 :: Proxy 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

k 在Proxy 和P (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

我正在等待对量化和范围界定的许多新的和即将发生的变化尘埃落定，这可能已经过时了。

【讨论】：

这是一个很好的解决方案，可以考虑以相同的方式编写类型族和数据类型，它可以更好地控制隐式细节。 GADs 扩展似乎也非常有用。还有一件事：Id 类型同义词可以等效地转换为类型族吗？

您可以将其写为type family Id a where Id a = a 并具有相同的签名，我相信它是等效的，但请谨慎对待，因为类型族可以有细微差别（请参阅On the arity of type families）

顺便说一句，写入的Proxy 数据类型（带有GADTs 扩展名的数据类型）是否等同于简单写入的数据类型（之前未定义其类型）：data Proxy a = Proxy？跨度>

我尝试了它的不同变体，见答案的结尾。

隐式绑定类型变量的作用发生了相当混乱的变化。我有点迷路了。

【参考方案2】：

您只差一种语言扩展。如果您也启用了CUSKs 扩展，那么您编写的内容将满足您的需求。