涉及种类 `Nat` 的乘法问题答案

【问题标题】：Multiplication problem involving kind `Nat`涉及种类 `Nat` 的乘法问题
【发布时间】：2021-09-17 19:55:50
【问题描述】：

为什么Nats 的加法、减法和除法有效，而乘法无效？

λ> :set -XDataKinds
λ> :set -XTypeOperators
λ> import GHC.TypeLits
λ> :k! 1 + 2
1 + 2 :: Nat
= 3
λ> :k! 1 - 2
1 - 2 :: Nat
= 1 - 2
λ> :k! 5 `Div` 2
5 `Div` 2 :: Nat
= 2
λ> :k! 1 * 2

<interactive>:1:1: error:
    • Expected kind ‘* -> Nat -> k0’, but ‘1’ has kind ‘Nat’
    • In the type ‘1 * 2’

【问题讨论】：

与* 指的是Type 种类。你应该明确使用* 所以:k 1 GHC.TypeLits.* 2。

标签： haskell data-kinds

【解决方案1】：

* 用于指定简单的Type。因此，1 被视为将*（所以Type）作为第一个类型参数，2 作为第二个类型参数，因此1 应该具有类型* -> Nat -> <em>something</em>。如果默认启用了StarIsType extension，GHC 会将星号 (*) 解析为对 Type 的引用。

如果禁用它，那么星号 (*) 将指代乘法，例如：

Prelude> :set -XDataKinds 
Prelude> :set -XTypeOperators
Prelude> :set -XNoStarIsType
Prelude> import GHC.TypeLits
Prelude GHC.TypeLits> :k 1 * 2
1 * 2 :: Nat
Prelude GHC.TypeLits> :kind! 1 * 2
1 * 2 :: Nat
= 2

您还可以显式指定使用 * 类型族族的模块：

Prelude> :set -XDataKinds 
Prelude> :set -XTypeOperators
Prelude> import GHC.TypeLits
Prelude GHC.TypeLits> :k 1 GHC.TypeLits.* 2
1 GHC.TypeLits.* 2 :: Nat
Prelude GHC.TypeLits> :kind! 1 GHC.TypeLits.* 2
1 GHC.TypeLits.* 2 :: Nat
= 2

【讨论】：

太棒了！此外，使用-XNoStarIsType，GHC 将类型的类型打印为Type 而不是*，这样更清晰。