haskell - 涉及种类 `Nat` 的乘法问题

Question

为什么Nat的加减除法s 工作，但不是乘法？

λ> :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’

Answer 1

*用于指定一个简单的 Type .结果1被视为将 * 作为第一个类型参数的东西(所以 Type )和作为第二类型参数 a 2 ，因此 1应该有种* -> Nat -> something . GHC 将解析星号 ( * ) 作为对 Type 的引用如果 StarIsType extension已启用，这是默认设置。
如果禁用它，那么星号 ( * ) 将指代乘法，例如:

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

您还可以明确指定使用 * 的模块。键入 family family 来自:

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