最近GHC言語拡張を眺めて遊んでいます。
GHC言語拡張を使うとHaskellに機能追加ができます。個別にオンオフすることができます。
今回はType-Level Literalsというのを遊んでみました。
型レベルリテラルです。
この機能は、型を書くところで、1や2といった数値リテラルを書くことができるみたいです。"hoge"といった文字列リテラルも使うことができるようです。今回は数値で遊んでみます。
型の確認
ghciで型を確認するには:typeが使えます。
ghci> :type 1
1 :: Num a => a
Haskellで小文字で書かれた型は型変数です。なんらかの型が入ります。しかし、Num a =>というので制約が加えらています。
足し算や掛け算ができるような型であればなんにでもなれます。
制約を満たす型にどんなものがあるかはghciで:infoを使うと確認できます。
ghci> :info Num
class Num a where
(+) :: a -> a -> a
(-) :: a -> a -> a
(*) :: a -> a -> a
negate :: a -> a
abs :: a -> a
signum :: a -> a
fromInteger :: Integer -> a
-- Defined in ‘GHC.Num’
instance Num Word -- Defined in ‘GHC.Num’
instance Num Integer -- Defined in ‘GHC.Num’
instance Num Int -- Defined in ‘GHC.Num’
instance Num Float -- Defined in ‘GHC.Float’
instance Num Double -- Defined in ‘GHC.Float’
1というリテラルの型は、WordやInteger、Int,Float, Doubleになれます。
明示的に型を指定することで、様々な型にすることができます。
ghci> :type 1 :: Int
1 :: Int :: Int
1 :: Int :: Intは(1 :: Int) :: Intと読むと良さそうです。「I :: Intの型はIntです」と読めます。
ghci> :type 1 :: Word
1 :: Word :: Word
ghci> :type 1 :: Float
1 :: Float :: Float
undefiend という値
ところで、Haskellにはどんな型の値にでもなれる便利な値undefinedがあります。
ghci> :type undefined
undefined :: t
ghci> :type undefined :: Int
undefined :: Int :: Int
ghci> :type undefined :: String
undefined :: String :: String
これらの例からわかるかもしれませんが::の後に続く部分に型を書くことができます。
型レベルリテラルなのでその部分に数値がかけるわけです。
試してみます。
ghci> :type undefined :: 1
<interactive>:1:14:
Illegal type: ‘1’ Perhaps you intended to use DataKinds
「違法な型 1が使われてます。たぶん DataKinds という拡張をつかえばいいです」と言われてます。
DataKinds拡張
GHCの拡張を使うにはソースコードの頭に{-# LANGUAGE DataKinds #-}とかいたり、コマンドラインのオプションで -XDataKindsとつけたりすることでできます。ghciの場合は:setを使うことで使えるようにできます。
ghci> :set -XDataKinds
ghci> :type undefined :: 1
<interactive>:1:14:
Expected a type, but ‘1’ has kind ‘GHC.TypeLits.Nat’
In an expression type signature: 1
In the expression: undefined :: 1
1とかけるようになりましたが、「型を要求してたけど、1のkindはGHC.TypeLits.Natだった」と言われてエラーになりました。
kind
kind(種、カインド)は型に対する型で、「値に型がある」ように「型には種」があります。
:kindを使うと型の種を確認できます。
ghci> :kind Int
Int :: *
ghci> :kind Int -> Int
Int -> Int :: *
ghci> let add = \x y -> x + y :: Int
ghci> :type add
add :: Int -> Int -> Int
ghci> :kind Int -> Int -> Int
Int -> Int -> Int :: *
普段つかっている関数や値の種は*(スター)になることが確認できます。
*以外になる型を見てみます。
ghci> :kind Num
Num :: * -> GHC.Prim.Constraint
ghci> :kind Monad
Monad :: (* -> *) -> GHC.Prim.Constraint
ghci> :kind []
[] :: * -> *
ghci> :kind Maybe
Maybe :: * -> *
型変数を持つような型は * -> *を持つことがわかります。Num a => a -> aで使われていたNum aは何か渡すと制約になったりするようです。これ以上深掘りはしません。
:kindの後には型がかけています。型がかけるので型レベルリテラルをかくことができます。
ghci> :kind 1
1 :: GHC.TypeLits.Nat
*ではなくGHC.TypeLits.Natだったためundefined :: 1とかけなかったようです。Natを受け取って*を返すような型があるとかけそうです。Proxyがあります。
ghci> import Data.Proxy
ghci> :kind Proxy
Proxy :: k -> *
ghci> :kind Proxy 1
Proxy 1 :: *
* にすることができました。
ghci> :type undefined :: Proxy 1
undefined :: Proxy 1 :: Proxy 1
ばっちりです。
undefiendをつかってきましたが、Proxy aな値をつくるには Proxyが使えます。
ghci> :type Proxy :: Proxy 1
Proxy :: Proxy 1 :: Proxy 1
型レベル数値リテラルの演算
数値は+や*で演算できます。型レベルでもできます。
やってみます。
ghci> :kind 1 + 1
<interactive>:1:3:
Illegal operator ‘+’ in type ‘1 + 1’
Use TypeOperators to allow operators in types
「TypeOperatorsという拡張をつかってみて」と言われました。
ghci> :set -XTypeOperators
ghci> :kind 1 + 1
<interactive>:1:3: Not in scope: type constructor or class ‘+’
世の中そんなに甘くないようです。
といっても、+はGHC.TypeLitsというところで定義されているだけです。
ghci> :kind 1 GHC.TypeLits.+ 1
1 GHC.TypeLits.+ 1 :: GHC.TypeLits.Nat
ghci> import GHC.TypeLits
ghci> :kind 1 + 1
1 + 1 :: Nat
エラーはでませんでした。
:kindの後ろにかけるのは型レベルの式です。(型式)
型式を評価するには:kind!というのを使うと評価できます。
ghci> :kind! 1 + 1
1 + 1 :: Nat
= 2
足し算できました。他にもできます。
ghci> :kind! 2 * 3
2 * 3 :: Nat
= 6
ghci> :kind! 6 - 2
6 - 2 :: Nat
= 4
ghci> :kind! 2 ^ 3
2 ^ 3 :: Nat
= 8
比較とかもできます。
ghci> :kind! 2 <=? 3
2 <=? 3 :: Bool
= 'True
ghci> :kind! 4 <=? 3
4 <=? 3 :: Bool
= 'False
ghci> :kind! 2 <= 3
2 <= 3 :: GHC.Prim.Constraint
= 'True ~ 'True
ghci> :kind! 4 <= 3
4 <= 3 :: GHC.Prim.Constraint
= 'False ~ 'True
制約になるものあるようです。
値のTrueと型のTrueが区別つく用にクオートがつくっぽいです。（よくわかってない)
ghci> :kind True
True :: Bool
ghci> :kind 'True
'True :: Bool
ghci> :type Proxy :: Proxy 'True
Proxy :: Proxy 'True :: Proxy 'True
ghci> :type Proxy :: Proxy True
Proxy :: Proxy True :: Proxy 'True
Orderingな結果を返す型レベルの関数もあります。
ghci> :kind! CmpNat 2 3
CmpNat 2 3 :: Ordering
= 'LT
ghci> :kind! CmpNat 3 3
CmpNat 3 3 :: Ordering
= 'EQ
ghci> :kind! CmpNat 4 3
CmpNat 4 3 :: Ordering
= 'GT
型から値を取り出すこともできます。
ghci> :type Proxy :: Proxy (1 + 1)
Proxy :: Proxy (1 + 1) :: Proxy 2
ghci> natVal (Proxy :: Proxy (1 + 1))
2
遊んでみる
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}
import Data.Proxy
import GHC.TypeLits
hoge1 :: Proxy 1
hoge1 = Proxy
hoge2 :: Proxy 2
hoge2 = Proxy
hoge3 :: Proxy 3
hoge3 = Proxy
hoge4 :: Proxy 4
hoge4 = Proxy
add' :: Proxy x -> Proxy y -> Proxy (x + y)
add' _ _ = Proxy
mul' :: Proxy x -> Proxy y -> Proxy (x * y)
mul' _ _ = Proxy
div' :: Proxy (x * y) -> Proxy x -> Proxy y
div' _ _ = Proxy
ghci> hoge1
Proxy
ghci> :type hoge1
hoge1 :: Proxy 1
ghci> hoge2
Proxy
ghci> :type hoge2
hoge2 :: Proxy 2
ghci> add' hoge1 hoge2
Proxy
ghci> :type add' hoge1 hoge2
add' hoge1 hoge2 :: Proxy 3
ghci> :type mul' hoge2 hoge4
mul' hoge2 hoge4 :: Proxy 8
ghci> :type div' hoge4 hoge2
div' hoge4 hoge2 :: Proxy 2
割り算をするための演算子はないが割り算を実現することができた
ghci> natVal div' hoge3 hoge2
div' hoge3 hoge2 :: ((2 * y) ~ 3) => Proxy y
ghci> natVal $ div' hoge3 hoge2
<interactive>:137:15:
Couldn't match type ‘2 * n0’ with ‘3’
The type variable ‘n0’ is ambiguous
Expected type: Proxy (2 * n0)
Actual type: Proxy 3
In the first argument of ‘div'’, namely ‘hoge3’
In the second argument of ‘($)’, namely ‘div' hoge3 hoge2’
3 / 2を型レベルでやろうとすると2 * y ~ 3のyに入る型がみつけられないようなエラーになりました。
余談
実用的な例を用意できなかった
まとめ
- 値に型があるように、型には種がある
- 型レベルで使える数値リテラルがある
- 型レベルの数値に使える演算子がある
- kind! で型式を評価できる
- kindが
*にならないと式としてつかえない - 手軽に
*にする方法としてProxyがある - GHC拡張にはいろいろおもしろい機能がある
- :set -X をつかえばghciでもGHC拡張が使える
プログラミングには言語によって表現しやすい機能がいろいろある。
Haskellを学んで自分が使い慣れている言語で置き換えたりしてみるといろんな学びがあるんじゃないかとおもうので、興味がでたらHaskellやその他の変わっているプログラミング言語を勉強してみたら良いのではないかとおもいます。