haskell - 在 Nat 上使用 * 作为原语

Question

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

以下 session 显示在本书中有效，但在我的机器上失败:

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 认为我的意思是那种 *而不是类型级函数* .

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

Answer 1

I suspect the problem has something to do with * also indicates a kind.

是的，这就是问题所在。可以使用 -XNoStarIsType 来解决扩展，让您对待 *作为另一个类型运算符。

指以前称为 * 的那种您可以导入 Type表格 Data.Kind .例如，Maybe 的种类是 Type -> Type和 StateT 的那种是 Type -> (Type -> Type) -> Type -> Type .

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