はじめに

λ ghc -V
The Glorious Glasgow Haskell Compilation System, version 8.8.1

λ :kind! 10*10
<interactive>:1:1: error:
Expected kind ‘* -> Nat -> k0’, but ‘10’ has kind ‘Nat
In the type10 * 10’
λ :set -XNoStarIsType
λ :kind! 10*10
10*10 :: Nat
= 100

型レベル四則演算

GHC.TypeLits に用意されている関数を使って型レベル自然数の四則演算を行ってみましょう。

λ :set -XDataKinds -XTypeOperators
λ import GHC.TypeLits

λ :kind! 1+1
1+1 :: Nat
= 2

λ :kind! 10-1
10-1 :: Nat
= 9

λ :kind! Div 10 2
Div 10 2 :: Nat
= 5

λ :kind! 10 * 10
<interactive>:1:1: error:
Expected kind ‘* -> Nat -> k0’, but ‘10’ has kind ‘Nat
In the type10 * 10’

掛け算だけエラーになりましたね・・・。それぞれの演算子のカインドを確認してみましょう。

λ :k (+)
(+) :: Nat -> Nat -> Nat
λ :k (-)
(-) :: Nat -> Nat -> Nat
λ :k Mod
Mod :: Nat -> Nat -> Nat
λ :k (*)
(*) :: *

1つだけ変ですね。これは *BoolMaybe などのよくある基本的な型 (lifted boxed types) のカインドの記号として割り当てられているためです。

λ :k Bool
Bool :: *

λ :k Maybe
Maybe :: * -> *

1つ前の GHC 8.6 から StarIsType 言語拡張がデフォルトで有効になり、* カインドは Type カインドのシノニムとして定義されるようになりました。なので明示的に StarIsType を無効にすると直ります。(この辺りの話題については既に “TypeOperators => NoStarIsType”の延期の提案 などにまとまっているため、気になる方はご参照ください)

λ :set -XNoStarIsType

λ :k Bool
Bool :: Type

λ :k Maybe
Maybe :: Type -> Type

λ :k (*)
(*) :: Nat -> Nat -> Nat

ということでこれで無事に型レベルの掛け算ができるようになりました。

λ :kind! 10 * 10
10 * 10 :: Nat
= 100

まとめ

kind! のエイリアスとして k! コマンド欲しい。

追記

k! コマンドのマージリクエストが作られました Allow completion for GHCi commands with option ! (#17345)

ありがとうございます :)

GHC に組み込まれるまでは、~/.ghci<proj>/.ghci に以下の内容を記述しておけば :kind! のエイリアスとして :k! が使えるようになります。

:def! k! (\e -> return (":kind! " ++ e))

実行結果

> :k! 1+1
1+1 :: Nat
= 2

参考リソース