Haskellにおける型レベルプログラミングの基本(翻訳)

概要

IOHKのHaskell及び暗号通貨の集中講義に参加したのですが、その中でも苦戦したのが型レベルプログラミングです。
そんな時に非常に助かったのがMatt Parsons氏のブログにて掲載されていたBasic Type Level Programming in Haskellです。是非この記事を翻訳し、日本のHaskellコミュニティの方とも共有したいと本人に伝えたところ、快く承諾を得られましたので以下にその文を掲載させて頂きます。

実装したコードはGitHubにもアップロードしているのでそちらも参照してみて下さい。
https://github.com/HirotoShioi/Basic-Type-Level-Programming

注意点

なお私はまだHaskellを始めたばかりなので誤訳、誤解しているところがあるかもしれません。それらを指摘して頂けると非常に助かります！

始めに

　近年、型依存プログラミングが盛んになっているし、支持している人は型システムにより多くの情報を取り入れることで実現できる素晴らしいことについていつも話している。これは事実だ。型レベルプログラミングはソフトウェアを設計する上で新しい、興味深いツールを提供してくれる。安全性を保証することがでるとともに、場合によっては型を利用することでパフォーマンスの最適化も可能なんだ。

　僕は読者にこれらの利点を売り込もうとしているわけじゃない。おそらく読者の中には型依存ニューラル・ネットワークやIdrisを用いて型システムでネットワークプロトコルを記述するを読んだことがある人もいるだろう。これらの記事を読んで型レベルプログラミングに興味を持てなかった人にはこの記事はオススメしない。一方でもし興味があった上でHaskell, Elm, F#,やML系の言語を知っているなら、この記事はあなたにうってつけだ。

型の基本

まずはHaskellにて１行で記述できるもっとも基本的なことから始めよう。

data Unit = MkUnit
data Bool = True | False

　このコードブロックでは2つの新たな型を定義している:Unit型とBool型だ。Unit型には値コンストラクタであるMkUnitがある。この型には値コンストラクタ1つしかない上に、引数もないのでUnitと呼んでいる。

　Boolには2つの値コンストラクタがある: TrueとFalseだ。これらもMkUnit同様引数をとらないため、定数と似たような振る舞いをする。

　型であるというのはどういう意味なのかって？型は物を分類する方法なんだ。「物」では曖昧かもしれない。ここでは「物」とは何を指すのだろうか。

　上記の基本型に関していえば、それぞれの取りうる値を全て定義したことになる。TrueとFalseはBool型の値と言える。また1やa、Unitは決してBool型ではないこともわかる。

　この例では退屈だ。他の型も見てみよう。

data IntAndChar = MkIntAndChar Int Char

　ここでは2つの引数Int、Charを取り、値コンストラクタが1つだけのIntAndChar型を定義している。この型の値は以下のようになる：

theFirstOne = MkIntAndChar 3 'a'
theSecond   = MkIntAndChar (-3) 'b'

MkIntAnCharはまるで関数のようだ。実際、GHCiにその型を問い合わせると以下のものが得られる。

λ> :t MkIntAndChar
MkIntAndChar :: Int -> Char -> IntAndChar

MkIntAndCharはIntとCharを引数に取り、IntAndChar型の値を返す関数であることがわかる。つまり値コンストラクタに引数を渡すこと値となり、その値には型があるんだ。では型に引数を渡すことはできるだろうか。もしできたとしたらそれはなんなのだろうか。

高階カインド(Higher Kinds)

まず関数と値についておさらいをしよう。型シグネチャがfoo :: Int -> IntAndCharである関数は以下のことを述べている

Int型の値を渡してください、そうすればIntAndChar型の値を返しますよ。

では次にそれを型レベルにリフトしよう。値コンストラクタは値を受け取り、値を返す。つまり型コンストラクタは型を受け取り、型を返すべきだ。Haskellでは型変数がこれを可能にする。

ここでみんなが大好きな直和型を例に挙げよう

data Maybe a
    = Just a
    | Nothing

ここでは2つの値コンストラクタJust aとNothingを持つMaybe型を定義している。Justはa型の値を引数にとり、Nothingは何も受け取らない。ここでGHCiにJustとNothingの型を聞いてみよう!

λ> :t Just
Just :: a -> Maybe a
λ> :t Nothing
Nothing :: Maybe a

どうやらJustは関数型のようだ。そして与えた型のMaybe型となる。一方Nothingは値も取らずに任意の型になれる。これらで少し遊んでみよう

λ> let nothingA = Nothing :: Maybe a
λ> let nothingInt = Nothing :: Maybe Int
λ> let nothingChar = Nothing :: Maybe Char
λ> nothingInt == nothingChar

\<interactive\>:27:15: error:
    • Couldn't match type ‘Char’ with ‘Int’
      Expected type: Maybe Int
        Actual type: Maybe Char
    • In the second argument of ‘(==)’, namely ‘nothingChar’
      In the expression: nothingInt == nothingChar
      In an equation for ‘it’: it = nothingInt == nothingChar
λ> nothingA == nothingInt
True
λ> nothingA == nothingChar
True

ワーオ！ nothingIntをnothingCharと比較しようとすると型エラーが出力されたぞ。でもこれは理にかなってるんだ。だって(==)は型が同じもの同士でしか比較ができないからね。ではnothingIntとnothingCharをnothingAと比較したときにエラーが出ないのはなぜだろう?

それはnothingA :: Maybe aの実際の意味が

私はMaybe a型の値です。aの取りうる型であれば任意の型になります。

だからだ。
MkIntAndCharに値を渡すことと、Maybeに型を渡すことは非常に似ているんだ。
ここでGHCIにMaybeの型を尋ねてみよう

λ> :type Maybe

\<interactive\>:1:1: error:
    • Data constructor not in scope: Maybe
    • Perhaps you meant variable ‘maybe’ (imported from Prelude

どうやら型の型はないようだ(ある意味ではね）。実は型にはカインド(Kind)があるんだ。:kindコマンドによってGHCiに型のカインドを尋ねることができる。

λ> :kind Maybe
Maybe :: * -> *

この*記号は何かって？　*は**値を持つ型(具体型)**のカインドを意味するんだ。GHCiにて確認してみよう。

λ> :kind Maybe
Maybe :: * -> *

Maybeのカインドが* -> *であるということは:

具体型を渡してくれれば具体型を返しますよ

ということなんだ。

　もしかしたら読者の中には高階多相カインドについて聞いたことがある人がいるかもしれない。ここである型を例に挙げてみよう。

data HigherKinded f a
    = Bare a
    | Wrapped (f a)

Haskellのカインド推論は非常に親切だ。ここではaにfを適用しているので、Haskellはfのカインドは* -> *であることを推論してくれる。ここでGHCiにHigherKindedのカインドを尋ねてみると

λ> :kind HigherKinded
HigherKinded :: (* -> *) -> * -> *

となる。

つまりHigherKindedはカインドが* -> *と*の型を受け取り、具体型である*を返す型なんだ。くどい説明をすると以下のようになる

2つの型をください。1つは具体型ではありませんが、具体型を渡すことで具体型となる関数です。もう1つは具体型です。2つを渡せば私は具体型を返します。

動的カインド付けプログラミング

*は正規表現の「なんでもマッチする」を思い出させる。*は具体型、あるいはその型の唯一の値が無限ループを生み出すものでさえそのカインドは*なんだ。

λ> data Void
λ> :kind Void
Void :: *

Voidには値コンストラクタがないが、それにもかかわらずカインドは*だ。

動的型を用いることで値レベルで効率的なプログラミングを行えることと同様に、動的カインドを用いることで型レベルで効率的にプログラミングを行うことが可能となるんだ。

型レベルで数字の記述を行なってみよう。まずはペアノ数の表現からだ。ペアノ数とは自然数をZero、もしくは任意の自然数NatのSuccessorであると定義されている。

data Zero
data Succ a

type One = Succ Zero
type Two = Succ One
type Three = Succ Two
type Four = Succ (Succ (Succ (Succ Zero)))

一応可能だが、これには納得がいかない。これではSucc Boolのような矛盾した型の定義が可能となるからだ。私は物事を明確にし、エラーを防ぐのが型の利点だと考えているので、型プログラミングを行う際に型の安全性を放棄するのはばかげている。安全性を取り戻すにはどうやら*以外のカインドを導入する必要があるようだ。

Data Kinds

{-# LANGUAGE DataKinds #-}

言語拡張であるDataKindsを利用することによって値コンストラクタを型コンストラクタへ、型コンストラクタをカインドコンストラクタへ昇格することができる。また昇格したものは名前の前にアポストロフィ'を付けることで利用できる。

それではカインド安全な自然数の定義を行なってみよう

data Nat = Zero | Succ Nat

普通のHaskellではこの定義によって、2つの値コンストラクタ、Zero、そしてNat型の値を受け取るSuccを持つ新しいNat型が定義されたことになる。言語拡張DataKindsを利用すると新たな定義が加えられる。別の名前空間に存在する新しいカインドNatと、定数型でありカインドがNatである'ZeroとカインドNatを持つ型を受け取ることのできる型コンストラクタ'Succだ。GHCiにこの2つのカインドを確認してみよう

λ> :kind 'Zero
'Zero :: Nat
λ> :kind 'Succ
'Succ :: Nat -> Nat

ここで「なんかこれ見たことあるぞ！」と思った人もいるかもしれない。それもそのはずだ、これらの値の型も見た目上は全く同じように見えるからだ。

λ> :type Zero
Zero :: Nat
λ> :type Succ
Succ :: Nat -> Nat

値なのか型なのかが曖昧であるときにはアポストロフィ'をつけることによって曖昧さを取り除くことができる。それ以外の場合にはHaskellは推論してくれる。ここで大事なのは'Zero型は具体型ではないことだ。カインドが*である型のみが具体型となる。
ここでは基本的な型及びカインドを構築した。実際にこれらを利用するには他の言語拡張が必要となる。

GADTs

{-# LANGUAGE GADTs #-}

ここで読者の中には「GADTって一体なんの略称なんですか？」と思った人もいるかもしれない。Richard Eisenberg氏ならGeneralized Algebraic Data Typesの略称なんだけど、その用語はあまり役に立たないからGADTsと呼んでくれと言うだろう。

GADTsはコンストラクタのパターンマッチングによって型の情報を提供できる言語拡張だ。GADTsではデータ型の構文が通常のHaskellとは異なる。ここで構文がどのように変わるのかを確認してみよう

data Maybe a where
    Just :: a -> Maybe a
    Nothing :: Maybe a

GADTの構文では値コンストラクタを１行ごとに定義する。また値コンストラクタにフィールドを提供するのではなく、型シグネチャを提供する。これは非常に興味深い変更だ。今Justをa -> Maybe aと記述することができた。つまりこれは以下の定義が可能になることを意味する。

data IntBool a where
    Int :: Int -> IntBool Int
    Bool :: Bool -> IntBool Bool

ここでは新たな型IntBool型を定義している、そしてそのカインドは* -> *だ。また値コンストラクタが2つある: Intは型シグネチャがInt -> IntBool Intであり、BoolはBool -> IntBool Boolとなっている。

値コンストラクタが返り値の型に関する情報を保持するので、値コンストラクタでパターンマッチを行なった際に型に関する情報が得ることができるんだ! これを次の関数で確認してみよう。

extractIntBool :: IntBool a -> a
extractIntBool (Int _)  = 0
extractIntBool (Bool b) = b

非常に興味深いことが起きた！Intでマッチングを行なった際にはIntBool a ~ IntBool IntであることをGHCがわかっているようだ。この波線~は**型同値(Type equality)**であることを意味し、GHCがコードの型チェックを行う際に解決する必要のある制約を課したことになる。

これらの言語拡張によりみんなが大好きな型依存を実装することができるようになった: 要素数を型レベルで表現するベクトルだ!

ベクトル

このベクトルはリストの長さを型レベルで表現するリストだ。これによってリストのout-of-boundsエラーを静的に回避することができる。我々はDataKindsを利用することによって自然数を型レベルに昇格することができた。またGADTsによって型の情報を提供できるようになった。次にこれらを組み合わせてみよう。

ここではわかりやすく説明するためにベクトルの定義を複数に分けて行う

data Vector (n :: Nat) a where

ここで我々はカインドがNat -> * -> *であるVector型を定義した。最初の型引数がベクトルの長さであって、2つ目の引数がベクトルに含まれる値の型となる。ここではカインド注釈を行なっているのでコンパイルするには以下の言語拡張が必要となる

{-# LANGUAGE KindSignatures #-}

型を意識する際に、私たちはしばしば、構築するときには帰納的に、そして分解するときには再帰的に考える必要があっただろう。ベクトルの基底部とはなんだろうか?それは長さがZeroのベクトルだ。

VNil :: Vector 'Zero a

VNilによって構築される値は任意の型aを持つことができるが、そのベクトルの長さは'Zeroとなる。
帰納的なケースはベクトルに値を追加することだ。値を1つ追加するということはベクトルの長さが１増えるということになる。

VCons :: a -> Vector n a -> Vector ('Succ n) a

値コンストラクタVConsは2つの値をとる、a型と、Vector n a型の値だ。渡されたベクトルの長さnは、任意の自然数であって、実際にどれだけ長いのかはわからない。ただVConsが返すベクトルの長さはnに1を足したものであることはわかっているので'Succ nとすればいい。
以下に完全な注釈を行なった明示的な定義を記載する

data Vector (n :: Nat) (a :: *) where
    VNil :: Vector 'Zero a
    VCons :: a -> Vector n a -> Vector ('Succ n) a

幸いなことにHaskellはこれらを推論してくれるので、上記の明示的な定義と暗黙的な定義のどちらを使用するかは読者の好みとなる。

data Vector n a where
    VNil :: Vector Zero a
    VCons :: a -> Vector n a -> Vector (Succ n) a

次にベクトルのShowインスタンスを定義しよう。これは簡単だ

instance Show a => Show (Vector n a) where
    show VNil         = "VNil"
    show (VCons a as) = "VCons " ++ show a ++ " (" ++ show as ++ ")"

ベクトルのAPI

次にベクトル同士の連結関数append :: Vector n a -> Vector m a -> Vector ??? aを定義してみよう。でも待てよ、???は一体どうすればいいんだ？ ???は2つの自然数nとmの合計値であることを表現しなければならない。足し算は関数だ。型関数なんてあるのだろうか？まぁ実はあるんだが、それを利用するにはGHCに新たな言語拡張を加えなければならない。

{-# LANGUAGE TypeFamilies #-}

なぜだか知らないが、型レベルで実行可能な関数は型族と呼ばれているんだ。型族の定義方法は２種類ある。オープンは誰でも新たなケースを追加できるのに対し、クローズドなものは全ての定義づけが一度に行われる。ここではクローズドな型族を扱うことになる。

では、型レベルで2つの自然数を追加する方法を考えてみよう。まずは値レベルで2つの自然数の合計値をどうやって求められるのか、その仕組みを理解しよう。

add :: Nat -> Nat -> Nat

これはみんなが大好きなHaskellの関数定義だ。ここでは値のパターンマッチ、where構文を用いて補助関数を定義することなどができる。

我々は帰納的に数値を定義したので、合計値は再帰的に求めることができそうだ。これはつまり基底部および帰納的なケースを扱う必要があることを意味する。まずは基本的なことから始めよう。任意の数nに0を足せば、その合計値はnとなる。

add Zero n = n

帰納的なケースでは以下のことが問われている

数（Succ n）の後続(Successor)を別の数（m）に足すと、その答えは何ですか？

Zeroまで再帰的に求めたいので、数を少しだけ減らしたいわけだ。ここでは左のSuccを右のmへ移動させる。これで2つの自然数の合計値を再帰的に求められるようになった。

add (Succ n) m = add n (Succ m)

自然数をお皿を積み上げたものだと想像すれば、自然数の加算というのは1つ目のスタックからお皿を１枚取り、2つ目のスタックに積み上げるようなものだと想像できるだろう。最終的に1つ目のお皿のスタックはZeroとなり、残された唯一のスタックが2つのスタックの合計値となる。

add :: Nat -> Nat -> Nat
add Zero n     = n
add (Succ n) m = add n (Succ m)

それではこの関数を型レベルに昇格させよう。

型族

型族の最初の定義はシグネチャとなる

type family Add n m where

これによって2つの引数を受け取る型関数Addを定義したことになる。次にそれぞれのケースを考えてみよう。ここでは値コンストラクタと同様、型コンストラクタを用いてパターンマッチすることができる。なので基底部Zeroは以下のようになる。

Add 'Zero n = n

次に帰納的なケースを再帰的に求めることになる

Add ('Succ n) m = Add n ('Succ m)

だがここでGHCはエラーを出力する

    • The type family application ‘Add n ('Succ m)’
        is no smaller than the instance head
      (Use UndecidableInstances to permit this)
    • In the equations for closed type family ‘Add’
      In the type family declaration for ‘Add’

GHCは決定不能性に非常に怯えており、それが自身で解決できない場合には何もしなくなるんだ。
UndecidableInstanceは次のような言語拡張となる。

GHC、大丈夫だよ。お前がこれを解決できないのはわかってる。最終的にこの問題は解決されるから安心してくれ

というわけでこの拡張も追加する。

{-# LANGUAGE UndecidableInstances #-}

これでコンパイルも通るようになった。この関数をどうやって試せばいいだろうか。

型のカインドを確認するのに:kindコマンドを利用したのと同様に、:kind!コマンドを使えば型の評価を行うことができる。以下のコードではその違いを紹介する

λ> :kind Add (Succ (Succ Zero)) (Succ Zero)
Add (Succ (Succ Zero)) (Succ Zero) :: Nat

λ> :kind! Add (Succ (Succ Zero)) (Succ Zero)
Add (Succ (Succ Zero)) (Succ Zero) :: Nat
= 'Succ ('Succ ('Succ 'Zero))

kindでは2つの自然数(Nat)を足すこと(Add)は自然数Natであることを示している。一方kind!を用いると型関数の評価を行い、その結果を返している。素晴らしい!これでappend関数を定義することができる

append :: Vector n a -> Vector m a -> Vector (Add n m) a

まずは型システムがもたらす恩恵を確認するために安易な実装を試みる。

append VNil rest = VNil

予想通りこれは型エラーが出力される。いい感じだ!

    • Could not deduce: m ~ 'Zero
      from the context: n ~ 'Zero
        bound by a pattern with constructor:
                   VNil :: forall a. Vector 'Zero a,
                 in an equation for ‘append’
        at /home/matt/Projects/dep-types.hs:31:8-11
      ‘m’ is a rigid type variable bound by
        the type signature for:
          append :: forall (n :: Nat) a (m :: Nat).
                    Vector n a -> Vector m a -> Vector (Add n m) a
        at /home/matt/Projects/dep-types.hs:30:11
      Expected type: Vector (Add n m) a
        Actual type: Vector 'Zero a
    • In the expression: VNil
      In an equation for ‘append’: append VNil rest = VNil
    • Relevant bindings include
        rest :: Vector m a
          (bound at /home/matt/Projects/dep-types.hs:31:13)
        append :: Vector n a -> Vector m a -> Vector (Add n m) a
          (bound at /home/matt/Projects/dep-types.hs:31:1)

エラーメッセージの量に怖気付いた人もいるかもしれない。これを読み解いてみよう。
GHCは2つ目のベクトルの長さであるmがZeroであることを推論できないと言っている。1つ目のベクトルの長さnはVNilのパターンマッチを行なっているのでZeroであることはわかっているようだ。ではどのような値を返すことができるのだろうか？一度GHCiで型を確認してみよう。

λ> :t append VNil
append VNil :: Vector m a -> Vector m a

append VNilは返り値としてVector m a型の値を返すようになっている。そして我々はmが一体何なのか全く知らない。よって引数をそのまま返す必要があるので基底部は以下のようになる。

append VNil xs = xs

返り値がVector m a型である以上、2つ目の引数をそのまま返す以外の方法を試みると型エラーによりコンパイルすらできなくなる。これが型レベルプログラミングの特徴だ。

次に先ほどの自然数の加算と同様、帰納的なケースも扱う必要がある。1つ目の引数の基底部を先ほど定義したので、1つ目を再帰的に呼び出すのが良さそうだ。
まずは安易な実装を試みる

append (VCons a rest) xs = append rest (VCons a xs)

しかしこれは我々が期待しているような動作はしない。GHCiにて確認してみよう。

λ> append (VCons 1 (VCons 3 VNil)) (VCons 2 VNil)
VCons 3 (VCons 1 (VCons 2 (VNil)))

ここではVCons 1 (VCons 3 (VCons 2 VNil))を返すはずだが実際には全く異なるものが返ってきた。ベクトルはその長さを型レベルで表現しているが、どのように連結しているかという情報は保持していない。型レベルに持ち込まれていないものはその正確性が保証されないんだ。
それでは先ほどの実装を修正してみよう。

append (VCons a rest) xs = VCons a (append rest xs)

次にGHCiにてこれを試してみよう

λ> :reload
[1 of 1] Compiling DepTypes         ( /home/matt/Projects/dep-types.hs, interpreted )

/home/matt/Projects/dep-types.hs:32:28: error:
    • Could not deduce: Add n1 ('Succ m) ~ 'Succ (Add n1 m)
      from the context: n ~ 'Succ n1
        bound by a pattern with constructor:
                   VCons :: forall a (n :: Nat).
                            a -> Vector n a -> Vector ('Succ n) a,
                 in an equation for ‘append’
        at /home/matt/Projects/dep-types.hs:32:9-20
      Expected type: Vector (Add n m) a
        Actual type: Vector ('Succ (Add n1 m)) a
    • In the expression: VCons a (append rest xs)
      In an equation for ‘append’:
          append (VCons a rest) xs = VCons a (append rest xs)
    • Relevant bindings include
        xs :: Vector m a (bound at /home/matt/Projects/dep-types.hs:32:23)
        rest :: Vector n1 a
          (bound at /home/matt/Projects/dep-types.hs:32:17)
        append :: Vector n a -> Vector m a -> Vector (Add n m) a
          (bound at /home/matt/Projects/dep-types.hs:31:1)
Failed, modules loaded: none.

なんてこった型エラーだ!どうやらGHCはAdd n (Succ m)がSucc (Add n m)と型同値であることを理解できないようだ。これはVector、Add、appendを並べてみるとその原因がわかる。

data Vector n a where
    VNil :: Vector Zero a
    VCons :: a -> Vector n a -> Vector (Succ n) a

type family Add x y where
    Add 'Zero n = n
    Add ('Succ n) m = Add n ('Succ m)

append :: Vector n a -> Vector m a -> Vector (Add n m) a
append VNil xs           = xs
append (VCons a rest) xs = VCons a (append rest xs)

Vectorの帰納的なケースではSuccを積み上げている。またAddの再帰的なケースでは、1つ目のスタックを減らしつつ2つ目に積み上げているのがわかる。最後にappendの再帰的なケースでは2つ目のスタックに積み上げている。エラーがどのようにして発生しているのか型注釈を与えながら調べてみよう。

append (VCons a rest) xs = VCons a (append rest xs)

値	型
VCons a rest	Vector (Succ n) a
xs	Vector m a
append rest xs	Add n m
VCons a (append rest xs)	Vector Succ (Add n m) a
求めている型	Vector Add (Succ n) m a

¹
ここではVCons a restの型がVector (Succ n) aであり、xsの型がVector m aであることがわかる。appendが返す型に合わせるためにこれらからVector (Add (Succ n) m) aを結果として返さなければならない。右側はVCons a (append rest xs)となっている。VConsはappend rest xsにSuccを足した長さを持っており、それはAdd n mであるはずだ。よって長さはSucc (Add n m)となる。残念なことに求めている型はAdd (Succ n) mだ。

我々はSucc (Add n m)とAdd (Succ n) mが型同値であることはわかっている。しかしGHCはこれを判断できないため、お手上げだと言っている。2つは明らかに同等であるが構造的に異なるためにエラーとなるんだ。これは型レベルプログラミングが抱えている大きな問題だ。実装内容が重要であり、安易な実装を試みると大問題につながる。ここでは型族Addを修正することにより解決される。

type family Add x y where
  Add 'Zero n     = n
  Add ('Succ n) m = 'Succ (Add n m)

この関数はSuccを取り出し、VConsにSuccを積み上げるという点においてappend関数の再帰部分と構造的に似ている。

この修正によりコンパイルが通り、append関数も正常に機能するようになる。

つまらないです

全くその通りだ。一方でこれに興味を持った読者の人にはこれに関してより良いチュートリアルがあるのでそれを読むことをオススメする。次に型レベルプログラミングを利用したより興味深い、実践的な例を挙げてみよう。

Heterogenous Lists

Heterogenous Listsはタプルのようなものだが、帰納的に定義されている。ここでは型レベルでリストの中身の型を保持することによってリストを安全に利用できるようにする。

Haskellにてリストを型レベルで扱うには、次の言語拡張が必要となる

{-# LANGUAGE TypeOperators #-}

これによって型レベルで演算子が利用できるようになる。

以下がHListの定義となる

data HList xs where
    HNil :: HList '[]
    (:::) :: a -> HList as -> HList (a ': as)

infixr 6 :::

値コンストラクタHNilは値がないため空のリストとなる。:::演算子は、a型の値と型のリストasを保持するHListをとり、返り値として型レベルで最初の要素がa型であり、その後にasが続くHListを返す。

次にこのHListを使ってみよう

λ> :t 'a' ::: 1 ::: "hello" ::: HNil
'a' ::: 1 ::: "hello" ::: HNil 
    :: HList '[Char, Int, String]

このHListではそれぞれの要素がChar,Int,Stringであることが型レベルで表現されている。このHListをShowしようとするとどうなるだろうか。

λ> 'a' ::: 1 ::: "hello" ::: HNil

\<interactive\>:13:1:
    No instance for (Show (HList '[Char, Int, String]))
      arising from a use of ‘print’
    In the first argument of ‘print’, namely ‘it’
    In a stmt of an interactive GHCi command: print it

どうやらHListのShowのインスタンスを定義する必要があるようだね。まずは安易な実装方法としてリストの中身を無視してみよう。

instance Show (HList xs) where
    show HNil         = "HNil"
    show (x ::: rest) = "_ ::: " ++ show rest

これは全く役に立たない。実際にShowのインスタンスを実装する方法はあるのだろうか。もちろんあるさ!

帰納的な型クラスのインスタンス

まずは基底部を定義しよう。基底部は空のHListだね。

instance Show (HList '[]) where
    show HNil         = "HNil"

これはコンパイルエラーを起こすので新たな言語拡張を追加する必要がある。

{-# LANGUAGE FlexibleInstances #-}

上記の型族の定義を行なったファイル以外でHListを実装している場合にはFlexibleContextについてもエラーが発生する。どうやらUndecidableInstancesを適用するとFlexibleContextsも同時に適用されるようだ。念のためにこれも追加しておこう。

{-# LANGUAGE FlexibleContexts #-}

以上によりコンパイラが通るようになり、show HNilが利用できるようになる。次は再帰的な部分の実装だ!
帰納法の原則によると

1. 基底部にて何かをする必要がある
2. 任意の場合でもそれが成り立つと仮定し、1段階上の場合でも成立することを証明する
3. 1と2により、すべての場合にて成り立つことが証明される。

基底部はすでに取り扱ったので、次は任意の場合でも成立すると仮定した上で、その１段階上のものも成り立つことを証明すればいい

instance (Show (HList as), Show a) 
    => Show (HList (a ': as)) where
    show (a ::: rest) = 
        show a ++ " ::: " ++ show rest

このインスタンスは以下のことを述べている

任意のHListであるasをShowする方法がわかっていると仮定し、その上でaのShowのインスタンスがわかっている場合、aとasを組み合わせたHListのShowインスタンスも存在する

λ> 'a' ::: 1 ::: "hello" ::: HNil
'a' ::: 1 ::: "hello" ::: HNil

練習問題

HListのaesonのインスタンスを定義せよ。これは先ほど定義したShowのインスタンスと似ているが、少し工夫が必要だ。

拡張可能レコード

Haskellの拡張可能レコードにはいくつか種類がある。ここでは小規模の実装を行うがそのためにはまた言語拡張を追加しなければならない

{-# LANGUAGE PolyKinds        #-}
{-# LANGUAGE TypeApplications #-}

PolyKindsは型変数の定義を一般化し、これによって具体型のない型変数のカインドを多相カインドにする。またTypeApplicationsは@シンボルを利用することにより多相関数に対して明示的に型を渡せるようになる。²

まずフィールドの型を定義し、その上でレコードを定義しよう

newtype s >> a = Named a

data HRec xs where
  HEmpty :: HRec '[]
  HCons  :: (s >> a) -> HRec xs -> HRec (s >> a ': xs)

引数sはカインドがSymbolの型だ。SymbolはGHC.TypeLitsにて定義されているので、インポートする必要がある。

次にTypeApplication構文を利用して値を構築してみよう。拡張レコードは以下のようになる

λ> HCons (Named @"foo" 'a') (HCons (Named @"bar" (3 :: Int)) HEmpty)

\<interactive\>:10:1: error:
    • No instance for (Show (HRec '["foo" >> Char, "bar" >> Int]))
        arising from a use of ‘print’
    • In a stmt of an interactive GHCi command: print it

いい感じだ。まだShowのインスタンスがないのでそれを実装しよう。
フィールド名は型レベルでのみ存在するが、KnownSymbol型クラスにあるsymbolVal関数を利用することで値レベルに変換することができる。

λ> :t symbolVal
-- proxyを受け取って、その型をStringとして返す
symbolVal :: KnownSymbol n => proxy n -> String
λ> let a = (Proxy :: Proxy "hello")
λ> symbolVal a
"hello"

基底部は以下のようになる

instance Show (HRec '[]) where
  show _ = "HEmpty"

再帰部にはもう少し情報が必要だ。まずはheadのShowインスタンスから始めよう。以下の変数が必要であることはわかっている

instance Show (HRec (s >> a ': xs)) where

ここではカインドがSymbolである型sと、具体型aそしてxsがある。次にパターンマッチを行おう

instance Show (HRec (s >> a ': xs)) where
    show (HCons (Named a) rest) =

まずはaの値をshowしたい。これは型クラス制約Show aをインスタンスに追加すればだけなので簡単だ。

instance (Show a) 
    => Show (HRec (s >> a ': xs)) where
    show (HCons (Named a) rest) =
        let val = show a

次にkeyを文字列として表現する必要がある。つまりsが型クラスKnownSymbolのインスタンスがあると仮定する必要がある。その上でproxy sを受け取り、Stringを返すsymbolValを利用すればいい。

instance (Show a, KnownSymbol s) 
    => Show (HRec (s >> a ': xs)) where
    show (HCons (Named a) rest) =
        let val = show a
            key = symbolVal (Proxy :: Proxy s)

この時点でNo instance for 'KnownSymbol s0'というエラーメッセージが表示された人もいるだろう。これは、Haskellの型変数のスコープがデフォルトでは非常に狭いためだ。例えば以下の例では

topLevelFunction :: a -> (a -> b) -> b
topLevelFunction a = go
  where
    go :: (a -> b) -> b
    go f = f a

Haskellは各型シグネチャの型変数はそれぞれのスコープがあると解釈する。これは補助関数goの変数aとbはtopLevelFunctionのものと異なるスコープにあることを意味する。よりわかりやすく記述すると以下のようになる

topLevelFunction :: a0 -> (a0 -> b0) -> b0
topLevelFunction a = go
  where
    go :: (a1 -> b1) -> b1
    go f = f a

型変数が他の変数と同様のスコープを持つようにするには、次の言語拡張が必要となる。

{-# LANGUAGE ScopedTypeVariables #-}

最後に、残りの部分を実装しよう

instance (Show a, KnownSymbol s, Show (HRec xs)) 
    => Show (HRec (s >> a ': xs)) where
    show (HCons (Named a) rest) =
        let val = show a
            key = symbolVal (Proxy :: Proxy s)
            more = show rest
         in "(" ++ key ++ ": " ++ val ++ ") " ++ more

以上により非常に納得のいくShowのインスタンスができた

λ> HCons (Named @"foo" 'a') (HCons (Named @"bar" (3 :: Int)) HEmpty)
(foo: 'a') (bar: 3) HEmpty

練習問題

JSONオブジェクトに変換するためにHRec型のAesonToJSONインスタンスを実装してみよう。
ボーナスポイント: HRec型のAesonFromJSONインスタンスを実装してみよう。

1. 文章ではわかりにくいと思ったのでテーブルにまとめました。 ↩

2. PolyKinds、Proxyに関してはAbout kind system of Haskell (Part 1)種の仕組みとそれに付随する言語拡張についてを参照してください。 ↩