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

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

种类参数是不可见的，但您可以在类型族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之间的差异。它们是等效的(在旧的GHC 8.10上测试(，除了k是

• (forall.(specified=可以用TypeApplications指定，但如果未指定，则会自动推断
• (forall{}.(推断=TypeApplications跳过，不能直接指定

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

在Proxy和P(P @Nat @42 :: Proxy @Nat 42(中指定的

• k

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

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

Answer 2

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