5

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

4

2 回答 2

4

我建议您使用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 = Charkind 参数是不可见的，但您可以在类型族（requires 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 或半开玩笑：'legacy' 语法）或 GADT。除了k之外，它们是等效的（在旧 GHC 8.10 上测试）

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

这适用于类型构造函数Proxy和为消除歧义而命名的数据构造函数P，因为它们都是多态的。Proxy可以根据 的量化来指定Proxy @Nat 42或推断：Proxy 42k

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

并且根据 中的量化P，可以指定或推断k：P @Nat @42P @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推断PP @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

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

于 2021-12-03T18:23:45.020 回答
1

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

于 2021-12-03T18:28:30.817 回答