在 Nat 上使用 * 作为原语

Question

我目前正在阅读 Sandy Maguire 的Thinking with Types，第 2 章涵盖术语、类型和种类。其中，有一个与类型级原语的简单交互示例，用于对Nats执行算术。

以下会话在书中显示有效，但在我的机器上失败：

Prelude> import GHC.TypeLits
Prelude GHC.TypeLits> :set -XDataKinds
Prelude GHC.TypeLits> :set -XTypeOperators
Prelude GHC.TypeLits> :kind! (1 + 17) * 3

<interactive>:1:1: error:
    * Expected kind `* -> Nat -> k0', but `1 + 17' has kind `Nat'
    * In the type `(1 + 17) * 3'

不过，书中的下一个示例有效：

Prelude GHC.TypeLits> :kind! (128 `Div` 8) ^ 2
(128 `Div` 8) ^ 2 :: Nat
= 256

我怀疑这个问题有关系*也预示着一种。Sandy Maguire 写道，这种语法将被弃用，但如果它仍然存在，我可以看到 GHCi 如何认为我的意思是kind *而不是类型级别的function *。

我是否在正确的轨道上，如果是，是否有一些标志可以用来使示例工作？

Answer 1

我怀疑问题与*有关，也表示一种。

是的，这就是问题所在。它可以通过使用-XNoStarIsType扩展来解决，它可以让您将其*视为另一种类型运算符。

要参考那种以前称为*可以输入的Type形式Data.Kind。例如，种类Maybe是Type -> Type和种类StateT是Type -> (Type -> Type) -> Type -> Type。

希望在未来的某个时候-XNoStarIsType将成为默认值，我们将始终使用 Type.