型レベルで値の個数の範囲を指定できるリストを使ってFinger Treeを実装する - GHCの型チェックプラグインを活用する

型レベルで値の個数の範囲を指定できるリストを使ってFinger Treeを実装する - GHCの型チェックプラグインを活用する
===============================================================================================

はじめにの前に
------------

これは2020年のアドベントカレンダーの18日目の記事です。「値の個数の範囲を型レベルで指定できるリスト」を作って、使ってみましたという話なのですが、なにやらつめこみすぎた感じがあります。作るだけじゃつまらないし、使うだけでもつまらないというところで、まず内容が多くなり、まともに使うためには「型チェックプラグイン」が必要という話で内容が倍増し、さらに「型チェックプラグイン」を実装するうえで「試しながら実装する」ためにパーサが必要だよねという話で、Packrat Parserの説明も追加したという、お祭りさわぎになってしまいました。最終的には

```haskell
foo :: RangeL 3 12 a -> RangeL 1 4 (RangeL 2 3 a)
```

みたいな関数を作ります。「要素が3個から12個のリストを『要素が2個から3個のリスト』を1個から4個含むリスト」に分割する関数です。「ふつうのリストだと要素の個数の範囲を型でしぼれなくて気持ち悪い」という特殊なタイプの需要に対応しています。実用性があるかどうかはわかりませんが、たとえば「100個の値」を表現するのにリストを使うのが気持ち悪いと感じたことがある人ならば、一読の価値があるかもしれません。

サンプルプログラムは以下に置きました。

[GitHub: try-fingertree-with-range-first](https://github.com/YoshikuniJujo/test_haskell/tree/master/tribial/qiita/fingertree_with_range/try-fingertree-with-range-first)

なんかFinger Treeってクリスマスツリーに似てる気がする。

はじめに
-------

リストを使ったアルゴリズムがあったとして、そのリストにはいる要素数が決まっていることがある。あるいは要素数の範囲が決まっていることがある。たとえば、Finger Treeというデータ構造の一部として、値の数が1個から4個までのデータ構造がある。つぎのような疑似コードで表されるような構造だ。

```
data Node a = a型の要素を2個か3個
data Digit a = a型の要素を1個から4個

data FingerTree a
        = Empty
        | Single a
        | Deep (Digit a) (FingerTree (Node a)) (Digit a)
```

データ型Nodeのほうは、つぎのように表せばいいだろう。

```
data Node a = Node2 a a | Node3 a a a
```

データ型Digitのほうには、ふたつの候補がある。ひとつは型シノニムとして

```
type Digit a = [a]
```

とするやりかたで、もうひとつは

```
data Digit a
        = One a
        | Two a a
        | Three a a a
        | Four a a a a
```

のように定義するやりかただ。前者はリストを使うやりかたで、この場合、本当は要素は「1個から4個」なのだけど「0個から無限個」までの要素の個数を許すようになっている。後者のほうは「1個から4個の値」ということを型で表現できているけれど冗長だ。これがたとえば「10個から20個」だったら、ちょっとやってられないだろう。

そこで「値の個数の範囲を型レベルで指定できる型Range」というものを考える。すると、

```
type Node a = Range 2 3 a
type Digit a = Range 1 4 a
```

のように指定できる。型Rangeを使えば、たとえば「値の個数が10個から20個」だったとしても

```
Range 10 20 a
```

のように表記することができる。このような型Rangeを定義したうえで、それを使ってFinger Treeとそれに対する演算を定義していこうと思う。

そのためには、型Rangeに対するいくつかの演算を定義しなくてはならないのだけど、そのうちのいくつかはGHCのデフォルトの型チェックでは解決できない型をもつ。たとえば、GHCのデフォルトの型チェックでは`(n + 1) - 1`と`(n - 1) + 1`とを異なる型であると判断するので、つぎのような関数は型チェックを通らない。

```
foo :: Proxy ((n + 1) - 1) -> Proxy ((n - 1) + 1)
foo = id
```

これをコンパイルしようとすると、つぎのようなエラーがでる。

```
Couldn't match type `(n + 1) - 1' with `(n - 1) + 1'
```

でも、これぐらいは計算できてもいいように思う。GHCには「型チェックプラグイン」という仕組みがあり、型チェックの機構を拡張することができる。そこで、今回は型チェックプラグインを使って「変数の足し算、引き算」くらいはできるように拡張してみようと思う。

この記事で題材とするテーマ
----------------------

* Finger Tree
* 要素の個数の範囲を指定できるリスト
* 型チェックプラグイン
* Packrat parser

### Finger Tree

値の並びを表現するデータ構造。先頭と末尾に対して、値の追加と取り出しが償却定数時間で実行できる。またFinger Treeどうしの結合は対数時間で実行可能となる。すこし、拡張することでFinger Treeの分割も対数時間で可能となるが、今回はそれはあつかわない。

### 要素の個数の範囲を指定できるリスト

型レベルで要素の個数の範囲を指定できるリスト。本質的にはおなじものだが、要素を左から追加できるものと、右から追加できるものとを定義する。たとえば、要素を左から追加できる2個から3個のa型の要素をもつリストは、つぎのように表記される。

```
RangeL 2 3 a
```

要素を右から追加できる1個から4個のa型の要素をもつリストの型は、つぎのようになる。

```
RangeR 1 4 a
```

### 型チェックプラグイン

GHCには型チェックの機構を拡張できる仕組みがある。`-fplugin=Foo.Bar`のようにすることで、`Foo.Bar.plugin`で指定されるプラグインを、コンパイル時に実行するようにできる。

RangeLやRangeRに対する演算のなかには、これを使って型チェックを拡張してやる必要があるものがある。

### Packrat parser

今回やることに本質的には関係ないが、型チェックプラグインを実装するうえで、いちいちコンパイラの型チェックのデバッグメッセージを出力するのではなく、簡潔にテストできるようにしたい。そのために、型チェックの対象となるダミーのデータを文字列をパースすることで用意したいのだけど、単純なコードでは実行効率が悪く、最悪では指数時間になってしまう。「愚直なコード」に対して、すこし変更することでO(n)時間でパースできるPackrat parserを構築することができることを示し、これをパーサとして利用する。

Finger Treeを実装する - `RangeL`や`RangeR`を使わない場合
------------------------------------------------

まずは、`RangeL`や`RangeR`を利用しないでFinger Treeと、先頭に要素を追加する関数を定義してみよう。Finger Treeに関しては、以下の論文を参照のこと。

[Finger Trees: A Simple General-purpose Data Structure](http://www.staff.city.ac.uk/~ross/papers/FingerTree.html)

ここで、この記事のサンプルプログラムを置くプロジェクトを作成する。

```
% stack new try-fingertree-with-range
% cd try-fingertree-with-range
% stack build
% mkdir src/Data
% mkdir src/Data/FingerTree
```

`Digit`としてリストを使うバージョンを作成する。

```haskell:src/Data/FingerTree/NoRange.hs
{-# OPTIONS_GHC -Wall -fno-warn-tabs #-}

module Data.FingerTree.NoRange where

data Node a = Node2 a a | Node3 a a a deriving Show
type Digit a = [a]

data FingerTree a
        = Empty | Single a | Deep (Digit a) (FingerTree (Node a)) (Digit a)
        deriving Show
```

`Empty`は空であり、`Single x`は値をひとつだけもつことを示す。値構築子`Deep`は再帰的な構造になっていて、左右の両端には、それぞれ、要素を1個から4個持つリストがあり、まんなかは`FingerTree (Node a)`となっており、これは`Node a`を要素とするFinger Treeになっている。さらに、「`Node a`を要素とするFinger Treeのなかには`Node (Node a)`を要素とするFinger Treeが含まれる」といったように、再帰的な構造になっている。

このFinger Treeに左から値を追加する関数を定義する。

```haskell:src/Data/FingerTree/NoRange.hs
infixr 5 <|

(<|) :: a -> FingerTree a -> FingerTree a
a <| Empty = Single a
a <| Single b = Deep [a] Empty [b]
a <| Deep [b, c, d, e] m sf = Deep [a, b] (Node3 c d e <| m) sf
a <| Deep pr m sf = Deep (a : pr) m sf
```

うえから順に説明する。「空の木」に要素をひとつ追加すると「要素がひとつの木」になる。「要素がひとつの木」に要素をひとつ追加すると「左右の`Digit`の部分に値がひとつずつはいっていて、まんなかの`FingerTree`は空であるような`FingerTree`」となる。

3行目の定義は再帰的になっている。左側の`Digit`にすでに4個の値がはいっている`FingerTree`に左から値を追加しようとしている。左側の`Digit`に含まれる値と、新しい値とで5個の値があることになるが、はじめのふたつは左側の`Digit`の部分にはいり、残りのみっつは`Node3 c d e`という形にまとめてから、`FingerTree a`型の値に含まれる`FingerTree (Node a)`型の値に左から追加される。

4行目の定義は左側の`Digit`の要素の数が4ではない、つまり1, 2, 3個の要素をもつ`Digit`である場合なので、そのときは、それに単純に値を追加すればいいということになる。試してみよう。

`stack ghci`として対話環境を呼び出して、つぎのようにする。

```
> 123 <| Empty
Single 123
> 456 <| it
Deep [456] Empty [123]
> 789 <| it
Deep [789,456] Empty [123]
> foldr (<|) Empty [0 .. 15]
Deep [0,1,2] (Deep [Node3 3 4 5,Node3 6 7 8,Node3 9 10 11] Empty [Node3 12 13 14]) [15]
```

`RangeL`の実装
-------------

うえで定義した`FingerTree`だと`Digit`の部分には1個から4個の要素しかはいらないのだけど、型としては0個から無限個まで収納可能になっている。これから定義していく`FingerTree`では、その部分には1個から4個までの要素しかはいらないデータ型を使うようにする。まずは、そのようなデータ型のうち、左から要素を追加していくタイプのものを実装してみよう。まずはファイルを用意して言語拡張などを、さきに書き出してしまおう。また、型レベル自然数と、それに対する演算を使うので`GHC.TypeNats`を導入しておく。

```
% mkdir src/Data/List
% mkdir src/Data/List/Range
```

```haskell:src/Data/List/Range/RangeL.hs
{-# LANGUAGE ScopedTypeVariables, InstanceSigs #-}
{-# LANGUAGE DataKinds, KindSignatures, TypeOperators #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE MultiParamTypeClasses, FlexibleContexts, FlexibleInstances,
        UndecidableInstances #-}
{-# OPTIONS_GHC -Wall -fno-warn-tabs #-}

module Data.List.Range.RangeL where

import GHC.TypeNats (Nat, type (+), type (-), type (<=))
```

データ型`RangeL`を定義する。言語拡張GADTsを使う。

```
infixr 6 :., :..

data RangeL :: Nat -> Nat -> * -> * where
        NilL :: RangeL 0 m a
        (:..) :: 1 <= m => a -> RangeL 0 (m - 1) a -> RangeL 0 m a
        (:.) :: a -> RangeL (n - 1) (m - 1) a -> RangeL n m a

deriving instance Show a => Show (RangeL n m a)
```

`RangeL n m a`の`n`は最小の要素数なので、空リストを意味する`NilL`の型は`RangeL 0 m a`である必要がある。`a :.. foo`のようなリストについては、`a`はオプショナルな値である。なくてもいい。つまり、値構築子`(:..)`が先頭にあるリストの型は`RangeL 0 m a`である必要がある。オプショナルな要素をひとつ追加して`RangeL 0 m a`となっているので、リスト`foo`の型は`RangeL 0 (m - 1) a`だ。

`a :. foo`では`a`は必要な値である。このリストの型を`RangeL n m a`とすると、リスト`foo`はそのリストから必要な要素をひとつ減らしたものなので、型は`RangeL (n - 1) (m - 1) a`であるはずだ。

ごちゃごちゃと説明したが、実際に値を作ってみたほうがわかりやすいかもしれない。対話環境を呼び出して試してみよう。

```
% stack ghci
> :set -XDataKinds
> type List35 = RangeL 3 5 Integer
> 1 :. 2 :. 3 :. NilL :: List35
1 :. (2 :. (3 :. NilL))
> 1 :. 2 :. 3 :. 4 :.. NilL :: List35
1 :. (2 :. (3 :. (4 :.. NilL)))
> 1 :. 2 :. 3 :. 4 :.. 5 :.. NilL :: List35
1 :. (2 :. (3 :. (4 :.. (5 :.. NilL))))
> 1 :. 2 :. 3 :. 4 :.. 5 :.. 6 :.. NilL :: List35

<interactive>:X:Y:error:
    ・Couldn't match type `'False' with `'True'
...
> 1 :. 2 :. NilL :: List35

<interactive>:X:Y:error:
    ・Couldn't match type `1' with `0'
```

要素が3個から5個まではリストが返されるが、6個以上の要素を入れようとしたり、2個以下だけしか要素を入れなかったりすると、型エラーになる。

`RangeL n m`を型クラスFoldableのインスタンスにしてみよう。

```haskell:src/Data/List/Range/RangeL.hs
instance Foldable (RangeL 0 0) where
        foldr _ z NilL = z
        foldr _ _ _ = error "never occur"


instance {-# OVERLAPPABLE #-}
        Foldable (RangeL 0 (m - 1)) => Foldable (RangeL 0 m) where
        foldr _ z NilL = z
        foldr (-<) z (x :.. xs) = x -< foldr (-<) z xs
        foldr _ _ _ = error "never occur"

instance {-# OVERLAPPABLE #-}
        Foldable (RangeL (n - 1) (m - 1)) => Foldable (RangeL n m) where
        foldr (-<) z (x :. xs) = x -< foldr (-<) z xs
        foldr _ _ _ = error "never occur"
```

`RangeL n m`を型クラスFoldableのインスタンスにするには、n, mの値について

* nとmの両者が0
* nのみ0
* nとmの両者が0でない

のみっつに場合わけする必要がある。ひとつめの場合については`RangeL 0 0 a`は空リスト以外ではあり得ない。空リストであれば関数`foldr`の結果は初期値のままであり、ここでは引数`z`がそのまま返り値となる。ふたつめの場合には、`RangeL 0 m a`は空リストかまたは`x :.. xs`のようにオプショナルな値`x`が先頭の値となる。後者の場合には通常のリストに対する`foldr`の定義と同様の定義になる。みっつめの場合には必須の要素が先頭の要素になる。つまり、`x :. xs`のようなパターンにマッチする。この場合も`foldr`の定義は通常のリストに対するものと同様だ。

それぞれの関数定義の最後に`foldr _ _ _ = error "..."`のように定義しているのは、コンパイラの警告を抑制するためだ。

対話環境で試してみよう。

```
> :set -XDataKinds
> foldr (+) 0 (1 :. 2 :. 3 :. 4 :.. 5 :.. NilL :: RangeL 3 5 Integer)
15
```

`RangeL n m a`型の値を構成するのに、必須の値を先頭に追加する演算子`(:.)`と、`RangeL 0 m a`型のリストにオプショナルな要素を先頭に追加する演算子`(:..)`とがある。一般的な`RangeL n m a`型のリストにオプショナルな値を追加する演算子はまだない。データ型の構成として「必須な値」が先にあり、「オプショナルな値」がそれに続くような構成なので、必須な値を含むリストの先頭へのオプショナルな要素の追加には演算子`(:..)`は使えない。

一般的な`RangeL n m a`型のリストの先頭にオプショナルな要素を追加する演算子`(.:..)`を定義する。この演算子の型はつぎのようになる。

```haskell
(.:..) :: a -> RangeL n m a -> RangeL n (m + 1) a
```

オプショナルな要素の追加なので、最小の個数`n`は増えない。最大の個数`m`は`1`だけ増加する。この演算子には型変数`n`の値によって場合わけが必要だ。`n`が`0`のときは`(.:..)`は`(:..)`とおなじでいい。`n`が`0`でないときには値構築演算子`(:.)`をずらしていく必要がある。

```
n == 0のとき、x .:.. xs = x :.. xs
n /= 0のとき、x .:.. (y :. ys) = x :. (y .:.. ys)
```

このように「型による場合わけ」が必要なときは、型クラス`Foldable`でみたように、インスタンス宣言のなかでクラス関数として定義してやる。型クラス`Foldable`のときとちがって、もとになる型クラスがないので、ここで定義する。

```haskell:src/Data/List/Range/RangeL.hs
infixr 5 .:..

class PushL n m where (.:..) :: a -> RangeL n m a -> RangeL n (m + 1) a
```

型クラスPushLを定義した。この型クラスに対するインスタンス宣言として、実際の演算子を定義する。

```haskell:src/Data/List/Range/RangeL.hs
instance PushL 0 m where (.:..) = (:..)

instance {-# OVERLAPPABLE #-} PushL (n - 1) (m - 1) => PushL n m where
        x .:.. (y :. ys) = x :. (y .:.. ys)
        _ .:.. _ = error "never occur"
```

`n`が`0`のときには`(.:..)`は`(:..)`だ。

`n`が`0`でなければ先頭に追加する要素は必須の要素として追加して、つぎの要素をオプショナルな要素として残りのリストに追加する。この操作は再帰的にくりかえされて、最終的に必須の要素がなくなるところまで続く。

これでうまくいくはずだが、コンパイルするとつぎのようなエラーが出る。

```
% stack build
...
・Couldn't match type '1 GHC.TypeNats.<=? (m + 1)' with `'True'
...

・Couldn't match type `(m - 1) + 1' with `(m + 1) - 1'
...
```

ひとつめは、`1 <= m + 1`が導けないということであり、ふたつめは`(m - 1) + 1 == (m + 1) - 1`が導けないということだ。ひとつめは`m`は「型レベル自然数」であることから自明だし、ふたつめは普通に考えれば自明なことに思える。そのくらいのことは、型チェックで導けてもいいんじゃないだろうか。そこで型チェックプラグインを作成する。エラーの出たインスタンス宣言はコメントアウトしておこう。

変数を含む加算、減算ができる型チェックプラグイン
----------------------------------------

### 何もしない型チェックプラグイン

まずは何もしない型チェックプラグインを書く。パッケージghcが必要なので、つぎのように追加する。

```
% vim package.yaml
...
dependencies:
- base >= 4.7 && < 5
- ghc
...
```

つぎのように、`src/Plugin/TypeCheck/Nat/Simple.hs`を作成する。

```
% mkdir src/Plugin
% mkdir src/Plugin/TypeCheck
% mkdir src/Plugin/TypeCheck/Nat
```

```haskell:src/Plugin/TypeCheck/Nat/Simple.hs
{-# LANGUAGE BlockArguments, OverloadedStrings #-}
{-# OPTIONS_GHC -Wall -fno-warn-tabs #-}

module Plugin.TypeCheck.Nat.Simple where

import GhcPlugins
import TcPluginM
import TcRnTypes

plugin :: Plugin
plugin = defaultPlugin { tcPlugin = const $ Just TcPlugin {
        tcPluginInit = pure (),
        tcPluginSolve = const solve,
        tcPluginStop = const $ pure () } }

solve :: [Ct] -> [Ct] -> [Ct] -> TcPluginM TcPluginResult
solve _ _ [] = pure $ TcPluginOk [] []
solve gs ds ws = do
        tcPluginTrace "!Plugin.TypeCheck.Nat.Simple" ""
        tcPluginTrace "Given: " $ ppr gs
        tcPluginTrace "Derived: " $ ppr ds
        tcPluginTrace "Wanted: " $ ppr ws
        pure $ TcPluginOk [] []
```

stack buildでコンパイルが通ることを確認する。GHCのプラグインは、`Plugin`型の値`plugin`を公開するモジュールとして作成する。`Plugin`型の値には、いろいろなプラグインが含まれるが、`defaultPlugin`を使うことで必要なプラグインだけを指定することができる。今回は型チェックプラグインなので`tcPlugin`フィールドを指定してやればいい。`tcPlugin`フィールドの値の型は、つぎのような型である。

```haskell
[CommandLineOption] -> Maybe TcRnTypes.TcPlugin
```

コマンドライン引数を使わないなら、`const $ Just ...`としておけばいい。で、`...`の部分にはいる`TcRnTypes.TcPlugin`型の値にはみっつのフィールドがある。それぞれ前処理、実際の処理、後処理のようになっている。これも、今回は前処理や後処理は行わないので、実際の処理のところだけが問題になり、そこに関数solveを指定した。

関数solveは`[Ct] -> [Ct] -> [Ct] -> TcPluginM TcPluginResult`であるが、引数は順に

* given
* derived
* wanted

と名づけられる引数である。引数derivedは今回は使わないので無視する。いまのところ何なのか、わからないので後で調べる予定だ。関数solveは引数givenによってあたえられた型制約を利用して、引数wantedの制約が解決できるかどうかを調べる関数だ。その結果は`TcPluginResult`でかえす。関数solveの本体部分では、とりあえず、それぞれの引数についてデバッグ出力するようにした。関数`tcPluginTrace`がデバッグ出力用の関数だ。この「何もしないプラグイン」を試すためにダミーのモジュールを作成する。

```
% mkdir src/Trial
% mkdir src/Trial/TryTypeCheck.hs
```

```haskell:src/Trial/TryTypeCheck.hs
{-# OPTIONS_GHC -Wall -fno-warn-tabs -fplugin=Plugin.TypeCheck.Nat.Simple #-}

module Trial.TryTypeCheck where

import Data.Proxy

foo :: Proxy hoge -> Proxy piyo
foo = id
```

コンパイルすると、つぎのようなエラーがでる。

```
% stack build
...
・Couldn't match type 'hoge' with 'piyo'
...
```

型チェックプラグインのデバッグ出力を見るにはコマンドラインオプション`-ddump-tc-trace`を使う。大量の出力があるので`grep`でしぼりこむ。

```
% stack build --ghc-options=-ddump-tc-trace 2>&1 | grep -A 35 '!Plugin.TypeCheck.Nat.Simple'
```

すると、つぎのような出力が得られる。

```
...
Given: []
Derived: []
Wanted:
  [[WD] hole{co_a5VS} {0}:: hoge_a5VM[sk:1]
                            ghc-prim-0.5.3:GHC.Prim.~# piyo_a5VN[sk:1] (CNonCanonical)}
...
```

わかりやすく本質を抽出すると、つぎのようになる。

```
Given: []
Derived: []
Wanted: [hoge ~ piyo]
```

この場合、`given`として何もあたえられていないなかで、`hoge`と`piyo`が等値であることを導き出すことが求められている。もうすこし試してみよう。モジュール`Trial.TryTypeCheck`を、つぎのように書き換える。

```haskell:src/Trial/TryTypeCheck.hs
{-# LANGUAGE DataKinds, TypeOperators #-}
{-# LANGUAGE GADTs #-}
{-# OPTIONS_GHC -Wall -fno-warn-tabs -fplugin=Plugin.Nat.Simple #-}

module Trial.TryTypeCheck where

import GHC.TypeNats
import Data.Proxy

bar :: (a + 1) ~ (b + 1) => Proxy a -> Proxy b
bar = id
```

おなじように型チェックプラグインのデバッグ出力をみてみる。本質だけにしぼると、つぎのようになっている。

```
Given: [
  fsk_a5Wg ~ fsk_a5Wg,
  (b_a5W4 + 1) ~ fsk_a5Wg,
  (a_a5W3 + 1) ~ fsk_a5We,
  fsk_a5We ~ fsk_a5Wg ]
Wanted: [a_a5W3 ~ b_a5W4]
```

もともとの`(a + 1) ~ (b + 1)`が、いくつかの等式にわけられていることがわかる。この場合はつぎのような`given`から、つぎのような`wanted`が導ければいいことになる。

```
given: [b + 1 == g, a + 1 == e, e == g]
wanted: [a == b]
```

`given`から`wanted`を導くには、つぎのようにして、`wanted`に存在しない変数を消去すればいい。

```
[b + 1 == g, a + 1 == e, e == g]
  | (== 0の形に直す)
  V
[b + 1 - g == 0, a + 1 - e == 0, e - g == 0]
  | (ひとつめの式からみっつめの式を引いて、変数gを消去する)
  V
[a + 1 - e == 0, b + 1 - e == 0]
  | (ひとつめの式から、ふたつめの式を引いて、変数eを消去する)
  V
[a - b == 0]
  |
  V
[a == b]
```

つぎに進む前に関数`bar`はコメントアウトしておこう。

### `Nat`類の式を表すデータ型

引数`given`でわたされる型制約から、引数`wanted`でわたされる型制約を導き出せるかどうかを判定すればいい。引数`given`, `wanted`の型はつぎのようになっている。

```
given :: [Ct]
wanted :: [Ct]
```

`Ct`は`Nat`類の型だけではなく、様々な類の型をあつかう複雑な型だ。そのままだとあつかいにくいので、`Nat`類の型をあつかう型制約の式だけを表す専用の型を用意することにする。

```
% mkdir src/Data/Derivation
```

```haskell:src/Data/Derivation/Expression.hs
{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# OPTIONS_GHC -Wall -fno-warn-tabs #-}

module Data.Derivation.Expression where

data Exp v t where
        Bool :: Bool -> Exp v Bool
        Var :: v -> Exp v a
        Const :: Integer -> Exp v Number
        (:==) :: Exp v a -> Exp v a -> Exp v Bool
        (:<=) :: Exp v Number -> Exp v Number -> Exp v Bool
        (:+) :: Exp v Number -> Exp v Number -> Exp v Number
        (:-) :: Exp v Number -> Exp v Number -> Exp v Number

data Number

deriving instance Show v => Show (Exp v t)
```

`Ct`型の値から`Exp v Bool`型の値に変換して、それを使って`given`の型制約から`wanted`の型制約を導けるかを判定するという方針だ。`Exp v t`型の値構築子はそれぞれ、つぎのようになる。

* `Bool`: 型レベル`Bool値`。`'False`と`'True`
* `Var`: 型変数。`a`とか`foo`とか
* `Const`: 型レベル`Nat`値。`1`とか`2`とか
* `(:==)`: 型レベル等値。`a ~ b`とかの`~`の部分
* `(:<=)`: 型レベル`Nat`値の小なりイコール。`n <=? m`の`<=?`
* `(:+)`: 型レベルNat値の加算。`m + 1`とかの`+`
* `(:-)`: 型レベルNat値の減算。`n - 1`とかの`-`

型レベル比較演算子`(<=)`は`m <= n`が`m <=? n ~ 'True`になるように定義されたシノニムであることに注意する。

型チェックプラグインのデバッグ出力で出力しやすいように型クラス`Outputable`のインスタンスにしておく。まずはモジュール`Outputable`を導入する。

```haskell:src/Data/Derivation/Expression.hs
import Prelude hiding ((<>))

import Outputable (Outputable(..), (<>), (<+>), text)
```

インスタンス宣言を定義する。

```haskell:src/Data/Derivation/Expression.hs
instance Outputable v => Outputable (Exp v t) where
        ppr (Bool b) = text "(Bool" <+> ppr b <> text ")"
        ppr (Var v) = text "(Var" <+> ppr v <> text ")"
        ppr (Const n) = text "(Const" <+> ppr n <> text ")"
        ppr (l :== r) = text "(" <> ppr l <+> text ":==" <+> ppr r <> text ")"
        ppr (l :<= r) = text "(" <> ppr l <+> text ":<=" <+> ppr r <> text ")"
        ppr (l :+ r) = text "(" <> ppr l <+> text ":+" <+> ppr r <> text ")"
        ppr (l :- r) = text "(" <> ppr l <+> text ":-" <+> ppr r <> text ")"
```

### `Ct`型の値から`Exp`型の値への変換

`Ct`型の値にはいろいろあるが、`type1 ~ type2`のような形の型制約のみをあつかうことにする。このときの、`type1`と`type2`を取得する関数を書く。ここは、ちょっと説明する時間がないので、この関数で取得できるとだけ理解してほしい。まずは、エラーメッセージを格納する型を定義する。

```
% mkdir src/Plugin/TypeCheck/Nat/Simple
```

```haskell:src/Plugin/TypeCheck/Nat/Simple/Decode.hs
{-# LANGUAGE BlockArguments, LambdaCase, OverloadedStrings #-}
{-# OPTIONS_GHC -Wall -fno-warn-tabs #-}

module Plugin.TypeCheck.Nat.Simple.Decode where

import Outputable (Outputable(..), SDoc, (<+>), text)
import Data.String

newtype Message = Message SDoc
instance Semigroup Message where Message l <> Message r = Message $ l <+> r
instance Monoid Message where mempty = Message ""
instance IsString Message where fromString = Message . text
instance Outputable Message where ppr (Message msg) = msg
```

デバッグ出力で出力しやすいようなデータ型`Message`を定義した。この`Message`型の値をエラー値として、`type1 ~ type2`のような形の`Ct`型の値から`type1`, `type2`を取り出す関数を定義する。モジュール`Control.Monad.Trans.Except`を導入する。

```
% vim package.yaml
...
dependencies:
- base >= 4.7 && < 5
- ghc
- transformers
...
```

```haskell:src/Plugin/TypeCheck/Nat/Simple.hs
import Control.Monad.Trans.Except

import Plugin.TypeCheck.Nat.Simple.Decode
```

```haskell:src/Plugin/TypeCheck/Nat/Simple.hs
unNomEq :: Ct -> Except Message (Type, Type)
unNomEq ct = case cllassifyPredType . ctEvPred $ ctEvidence ct of
        EqPred NomEq l r -> pure (l, r)
        _ -> throwE "Cannot unNomEq"
```

試してみよう。関数solveを書き換える。つぎの部分を

```haskell:src/Plugin/TypeCheck/Nat/Simple.hs
        tcPluginTree "Given: " $ ppr gs
        tcPluginTree "Derived: " $ ppr ds
        tcPluginTree "Wanted: " $ ppr ws
```

つぎのように書き換える。

```haskell:src/Plugin/TypeCheck/Nat/Simple.hs
        tcPluginTree "Given: " . ppr $ runExcept . unNomEq <$> gs
        tcPluginTree "Derived: " . ppr $ runExcept . unNomEq <$> ds
        tcPluginTree "Wanted: " . ppr $ runExcept . unNomEq <$> ws
```

型チェックプラグインを動かすためには、モジュール`Trial.TryTypeCheck`のコメントアウトした関数`bar`をもとにもどす。型チェックプラグインのデバッグ出力を見てみよう。

```
% stack build --ghc-options=-ddump-tc-trace 2>&1 | grep -A 25 '!Plugin.TypeCheck.Nat.Simple'
```

だいたい、つぎのような出力が得られる。

```
Given: [
  Left Cannot unNomEq, Right (b_a6Vg[sk:1] + 1, fsk_a6Vs[fsk:1]),
  Right (a_a6Vf[sk:1] + 1, fsk_a6Vq[fsk:1]),
  Right (fsk_a6Vq[fsk:1], fsk_a6vs[fsk:1])]
Derived: []
Wanted: [Right (a_6Vf[sk:1], b_a6Vg[sk:1])]
```

本質だけぬきだすと、つぎのようになる。

```
Given: [
  Left Cannot unNomEq, Right (b + 1, s),
  Right (a + 1, q), Right (q, s) ]
Derived: []
Wanted: [Right (a, b)]
```

`type1 ~ type2`のような形の`Ct`型の値から`(type1, type2)`のような値が取り出せている。`type1`と`type2`の型は`Type`なので、`Ct`型の値から`Exp`型の値に変換するには、`Type`型の値ふたつを引数として`Exp`型の値を返り値とする関数を定義すればいいことになる。ただし、どのような`Type`型の値からでも`Exp`型の値が取り出せるわけではないので、結果は`Except Message (Exp Var Bool)`のようになる。つぎのような型の関数`decode`を定義していく。

```haskell
decode :: Type -> Type -> Except Message (Exp Var Bool)
```

まずは`Type`型の値が型変数だった場合に`Exp Var a`型の値に変換する関数を定義する。まずは、必要なモジュールを導入する。

```haskell:src/Plugin/TypeCheck/Nat/Simple/Decode.hs
import GhcPlugins (Var, promotedFalseDataCon, promotedTrueDataCon)
import TyCoRep
import Control.Monad.Trans.Except
import Data.Derivation.Expression
```

関数`exVar`を定義する。

```haskell:src/Plugin/TypeCheck/Nat/Simple/Decode.hs
exVar :: Type -> Except Message (Exp Var a)
exVar = \case TyVarTy v -> pure $ Var v; _ -> throwE "exVar: fail"
```

`Type`型の値のうち`TyVarTy v`が型変数ひとつからなる型を表すので、そのときには`Exp`型の値`Var v`を返す。それ以外の値に対してはエラー値とする。

型レベル自然数であるような型を表す`Type`型の値を`Exp Var Number`に変換する関数を定義する。まずは、モジュール`TcTypeNats`を導入する。

```haskell:src/Plugin/TypeCheck/Nat/Simple/Decode.hs
import TcTypeNats
```

```haskell:src/Plugin/TypeCheck/Nat/Simple/Decode.hs
exNum :: Type -> Except Message (Exp Var Number)
exNum (TyVarTy v) = pure $ Var v
exNum (LitTy (NumTyLit n)) = pure $ Const n
exNum (TyConApp tc [l, r])
        | tc == typeNatAddTyCon = (:+) <$> exNum l <*> exNum r
        | tc == typeNatSubTyCon = (:-) <$> exNum l <*> exNum r
exNum _ = throwE "exNum: fail"
```

型変数は型レベル自然数であるかもしれないので、ここでも取りあつかう。数値リテラル(`LitTy (NumTyLit n)`)は`Const n`に変換。ほかには`a + b`や`a - b`の形の型があるので、それぞれを`a :+ b`や`a :- b`のような値に変換する。`typeNatAddTyCon`は型レベル加算であり、`typeNatSubTyCon`は型レベル減算だ。

型レベル`Bool`値を`Exp Var Bool`型の値に変換する関数を定義する。

```haskell:src/Plugin/TypeCheck/Nat/Simple/Decode.hs
exBool :: Type -> Except Message (Exp Var Bool)
exBool (TyVarTy v) = pure $ Var v
exBool (TyConApp tc [])
        | tc == promotedFalseDataCon = pure $ Bool False
        | tc == promotedTrueDataCon = pure $ Bool True
exBool (TyConApp tc [l, r])
        | tc == typeNatLeqTyCon = (:<=) <$> exNum l <*> exNum r
exBool _ = throwE "exBool: fail"
```

型変数は型レベル`Bool`値であることもあるので、ここでも取りあつかう。型レベル`Bool`値である`'False`や`'True`は、それぞれ`promotedFalseDataCon`と`promotedTrueDataCon`である。小なりイコールは`typeNatLeqTyCon`だ。それぞれ`Exp Var Bool`型の値に変換している。

これらをあわせて、関数`decode`を定義する。ひとつめの`Type`型の値が型変数だった場合には、ふたつめの`Type`型の値の種類によって、`Exp Var a`型の値か、`Exp Var Number`型の値か、`Exp Var Bool`型の値のどれかに決まることに注意が必要だ。演算子(<|>)を使うためにモジュール`Control.Applicative`を導入する。

```haskell:src/Plugin/TypeCheck/Nat/Simple/Decode.hs
import Control.Applicative ((<|>))
```

関数`decode`を定義する。

```haskell:src/Plugin/TypeCheck/Nat/Simple/Decode.hs
decode :: Type -> Type -> Except Message (Exp Var Bool)
decode (TyVarTy l) r = le <$> exVar r <|> le <$> exNum r <|> le <$> exBool r
        where le = (Var l :==)
decode l r = (:==) <$> exNum l <*> exNum r <|> (:==) <$> exBool l <*> exBool r
```

1行目では、つぎの3通りについて変換を行っている。

* 型変数 ~ 型変数
* 型変数 ~ 型レベル自然数
* 型変数 ~ 型レベル`Bool`値

2行目では、つぎの2通りについて変換している。

* 型レベル自然数 ~ 型レベル自然数
* 型レベル`Bool`値 - 型レベル`Bool`値

関数`decode`を試してみよう。モジュール`Plugin.TypeCheck.Nat.Simple`を書き換える。`Control.Monad.(<=<)`を使うので、`Control.Monad`を導入する。

```haskell:src/Plugin/TypeCheck/Nat/Simple.hs
import Control.Monad
```

関数`solve`を3行書き換える。

```haskell:src/Plugin/TypeCheck/Nat/Simple.hs
        tcPluginTrace "Given: " . ppr $ runExcept . (uncurry decode <=< unNomEq) <$> gs
        tcPluginTrace "Derived: " . ppr $ runExcept . (uncurry decode <=< unNomEq) <$> ds
        tcPluginTrace "Wanted: " . ppr $ runExcept . (uncurry decode <=< unNomEq) <$> ws
```

関数`unNomEq`で`type1 ~ type2`から取り出した`type1`と`type2`に対して関数`decode`を適用している。

型チェックプラグインのデバッグ出力をみてみよう。

```
% stack build --ghc-options=-ddump-tc-trace 2>&1 | grep -A 20 '!Plugin.TypeCheck.Nat.Simple'
```

だいたい、つぎのような出力が得られる。

```
Given:
  [Left Cannot unNomEq,
   Right (((Var b_a7xA[sk:1]) :+ (Const 1)) :== (Var fsk_a7xM[fsk:1])),
   Right (((Var a_a7xz[sk:1]) :+ (Const 1)) :== (Var fsk_a7xK[fsk:1])),
   Right (((Var fsk_a7xK[fsk:1]) :== (Var fsk_a7xM[fsk:1]))]
Derived: []
Wanted: [Right ((Var a_a7xz[sk:1]) :== (Var b_a7xA[sk:1]))]
```

これで、`given :: [Ct]`と`wanted :: [Ct]`とを、`Exp`型の値に変換することができた。つぎにすることは、「`given`から`wanted`を導出できるかの判定」である。しばらくはGHC内部の煩雑な型にわずらわされずにすむ。`Exp v Bool`型の値をあつかっていく。

`src/Trial/TryTypeCheck.hs`の関数`bar`をコメントアウトしておこう。

### あたえられた制約から求める制約が導出できるかを判定する

#### O(n)時間で動作する単純なパーサ

複数の`Exp`型の値で表される`given`から、`Exp`型で表される`wanted`を導出できるかどうかを判定する関数を定義していくが、`Exp`型の値を簡単に書けるようにしておいたほうが、作った関数をテストしやすい。文字列から`Exp`型を構成する簡単なパーサを作っておこう。

##### 単純な実装だと最悪で指数関数時間かかる

解析される文法を表現する簡単な記法のひとつにPEGがある。PEGで書かれた文法をHaskellで実装するのは簡単だ。例として、つぎのような文法を考える。

```
Expr <- Term '+' Expr / Term
Term <- '(' Expr ')' / '1'
```

パーサを実装するのに必要なのは、文字列を読み込んで、パースが成功したら「パースされた結果を表す値」と残りの文字列を返す関数だ。つまり、つぎのような型の関数が必要になる。

```haskell
p :: String -> Maybe (Ret, String)
```

より一般的には、つぎのような型になる。

```haskell
p :: s -> Maybe (a, s)
```

このような関数の型と同等な型はモナド変換子で、つぎのように構成することができる。

```haskell
p :: StateT s Maybe a
```

わかりやすいように、このような型を定義したモジュール`Data.Parse`を作成する。モナド変換子`StateT`を使うのでパッケージ`monads-tf`を依存するパッケージに追加する。

```
% vim package.yaml
...
dependencies:
- base >= 4.7 && < 5
- ghc
- transformers
- monads-tf
...
```

モジュール`Data.Parse`を作成する。

```haskell:src/Data/Parse.hs
{-# OPTIONS_GHC -Wall -fno-warn-tabs #-}

module Data.Parse (Parse, parse, unparse) where

import Control.Monad.State

type Parse s = StateT s Maybe

parse :: (s -> Maybe (a, s)) -> Parse s a
parse = StateT

unparse :: Parse s a -> s -> Maybe (a, s)
unparse = runStateT
```

モジュール`TryParse.Exponential`に指数関数時間かかるパーサを定義していこう。

```
% mkdir src/TryParse
```

まずは、'(', ')', '+', '-', '1'を読み込むために「指定された一文字を読み込む関数」を定義する。

```haskell:src/TryParse/Exponential.hs
{-# LANGUAGE BlockArguments, LambdaCase #-}
{-# OPTIONS_GHC -Wall -fno-warn-tabs #-}

module TryParse.Exponential where

import Control.Applicative
import Data.Bool
import Data.List
import Data.Parse

data Expression = One | Expression :+ Expression | Expression :- Expression
        deriving Show

pChar :: Parse String Char
pChar = parse uncons

pick :: Char -> Parse String Char
pick = check . (==)

check :: (Char -> Bool) -> Parse String Char
check p = pChar >>= \c -> bool empty (pure c) (p c)
```

はじめに、データ型`Expression`を定義した。関数`pChar`は文字列のはじめの一文字を読み込む。関数`check`は読み込んだ1文字を条件`p`でチェックして、条件を満たす場合のみ成功にする。関数`pick`は関数`check`の条件`p`を「あたえられた文字と等値(`(==)`)」とすることで、指定した一文字を読み込む動作となる。

「式」と「項」を解析する関数を構成する。

```src/TryParse/Exponential.hs
pExpr, pTerm :: Parse String Expression
pExpr = (:+) <$> pTerm <* pick '+' <*> pExpr <|> pTerm
pTerm = pick '(' *> pExpr <* pick ')' <|> One <$ pick '1'
```

「式」は「項+式」または「項」であり、「項」は「(式)」または「1」である。

試してみる。型チェックプラグインを使用しているので、通常のやりかたでは対話環境が使えないかもしれない。つぎのようなコマンドを打ち込む。

```
% stack ghci --ghc-options -fobject-code
```

つぎのように打ちこんでみよう。

```
> unparse pExpr "(1+1)+1+1"
Just ((One :+ One) :+ (One :+ One),"")
> :set +s
> unparse pExpr "(((((1)))))"
Just (One,"")
(0.00 secs, 691,640 bytes)
> unparse pExpr "(((((((1)))))))"
Just (One,"")
(0.04 secs, 1,238,904 bytes)
> replicate 20 '(' ++ "1" ++ replicate 20 ')'
"((((...(1)...))))"
> unparse pExpr it
Just (One,"")
(1.89 secs, 5,973,198,640 bytes)
> replicate 21 '(' ++ "1" ++ replicate 21 ')'
"((((...(1)...))))"
> unparse pExpr it
Just (One,"")
(3.81 secs, 11,945,887,616 bytes)
```

かっこの入れ子が1段深くなるたびに、実行時間が2倍になっている。

##### O(n)時間で実行可能なパーサ (Packrat Parser)

PEGで表される文法については、O(n)時間で解析できる手法が知られている。Packrat Parsingと呼ばれるこの手法は、メモ化を利用することでO(n)時間での解析を可能にする。うえの文法を解析するPackrat Parserを書いてみよう。まずはモジュールを用意する。

```haskell:src/TryParse/NoExponential.hs
{-# OPTIONS_GHC -Wall -fno-wan-tabs #-}

module TryParse.NoExponential where

import Control.Applicative
import Control.Arrow
import Data.Bool
import Data.List
import Data.Parse
```

データ型`Expression`はおなじように定義する。

```haskell:src/TryParse/NoExponential.hs
data Expression = One | Expression :+ Expression deriving Show
```

Packrat Parserでは、それぞれの文法要素について、それぞれの「解析の対象における位置」での解析の結果として「取得できる値」と「つぎに解析する位置」のペアを保存しておくことで、O(n)時間での解析を可能にする。値と「つぎの位置」を保存するデータ構造を用意しよう。

```haskell:src/TryParse/NoExponential.hs
data Memo = Memo {
        expr :: Maybe (Expression, Memo),
        term :: Maybe (Expression, Memo),
        char :: Maybe (Char, Memo) }
```

再帰的な型として定義されている。すこしわかりにくいが、実装のイメージとしては、文字のリスト(`data Memo = Maybe (Char, Memo)`)があり、それに対して追加の値(`Expression`)と「とびとびの`Memo`に対するリンク」がのっかっている感じだ。

指定した文字を読み込む機能を持つParse型の値を定義する。

```haskell:/sr/TryParse/NoExponential.hs
check :: (Char -> Bool) -> Parse Memo Char
check p = parse char >>= \c -> bool empty (pure c) (p c)

pick :: Char -> Parse Memo Char
pick = check . (==)
```

`char :: Memo -> Maybe (Char, Memo)`は文字列の代わりにデータ型`Memo`を対象として一文字を読み込む関数と考えることができる。関数`parse`を適用することでモナドのわくぐみであつかうことができる。ここでは「一文字読み込み、それを条件pでチェックする」という機能を実装している。関数`pick`はその関数`check`に等値演算子`(==)`をあたえることで「指定した一文字を読み込む機能」を持つ`Parse`型の値とした。

データ型`Memo`を文字列の代わりとして、「式」と「項」を読み込むパーサを定義する。

```haskell:src/TryParse/NoExponential.hs
pExpr, pTerm :: Parse Memo Expression
pExpr = (:+) <$> parse term <* pick '+' <*> parse expr <|> parse term
pTerm = pick '(' *> parse expr <* pick ')' <|> One <$ pick '1'
```

「式」を読み込むパーサである`pExpr`は「項+式」または「項」を読み込む。「項」を読み込むパーサである`pTerm`は「(式)」または「1」を読み込む。関数`pTerm`や`pExpr`をそのまま使うのではなく`parse term`や`perse expr`を使うことで、新たに値を計算するのではなく、メモ用の構造から値を取り出すようにした。

文字列からメモ用の構造を構成する関数を定義する。

```haskell:src/TryParse/NoExponential.hs
memo :: String -> Memo
memo cs = m where
        m = Memo ex tm ch
        ex = unparse pExpr m
        tm = unparse pTerm m
        ch = (memo `second`) <$> uncons cs
```

`ch = (memo second) <$> uncons cs`のところは、つぎのような式とおなじことだ。

```haskell
ch = case cs of
        c : cs' -> Just (c, memo cs')
        "" -> Nothing
```

はじめの文字を「結果の値」として、残りの文字列について再帰的にメモ用の構造を構成している。

ローカル変数`m`は結果のメモ用の構造そのものだ。ローカル変数`ex`に`pExpr`によって、値`m`から、読み込む「式」の値と、それを読み込んだあとに残る「メモ用の構造」を構成している。ローカル変数`tm`も同様だ。

これでだいたい完成だが、使いやすいようにメモ用の構造から必要な値を取り出す関数を定義する。

```haskell:src/TryParse/NoExponential.hs
parseExpr :: String -> Maybe Expression
parseExpr src = fst <$> expr (memo src)
```

試してみよう。

```
% stack ghci --ghc-options -fobject-code
> parseExpr "(1+1)+1+1"
Just ((One :+ One) :+ (One :+ One))
> :set +s
> replicate 21 '(' ++ "1" ++ replicate 21 ')'
"((((...(1)...))))"
> parseExpr it
Just One
(0.01 secs, 537,640 bytes)
> replicate 80 '(' ++ "1" ++ replicate 80 ')'
"((((...(1)...))))"
> parseExpr it
Just One
(0.01 secs, 716,272 bytes)
```

効率が改善している。

##### Exp型の値を構成するパーサ

Exp型の値を読み出すパーサを定義する。まずは、モジュール`Data.Parse`に「否定先読み」用の関数を定義する。モジュール`Control.Applicative`を導入する。

```haskell:src/Data/Parse.hs
import Control.Applicative
```

```haskell:src/Data/Parse.hs
(>>!) :: Parse s a -> Parse s b -> Parse s a
p >>! nla = parse $ unparse p >=> \r@(_, s') ->
        maybe (pure r) (const empty) $ unparse nla s'
```

`p`による解析のあとに`nla`による解析を行い、その結果が`Nothing`だったときだけ、`p`による解析結果を返す。モジュール`Data.Parse`の公開リストに演算子`(>>!)`を追加する。

```haskell:src/Data/Parse.hs
module Data.Parse (Parse, parse, unparse, (>>!)) where
```

`Exp`型の値を読み込むパーサを定義していこう。モジュール`Data.Derivation.Parse`を用意する。

```haskell:src/Data/Derivation/Parse.hs
{-# OPTIONS_GHC -Wall -fno-warn-tabs #-}

module Data.Derivation.Parse where

import Control.Applicative (empty, many, (<|>))
import Control.Arrow
import Data.Function
import Data.Maybe
import Data.List
import Data.Char

import Data.Parse
import Data.Derivation.Expression

import qualified Data.Bool as B
```

メモ用のデータ型を用意する。

```haskell:src/Data/Derivation/Parse.hs
data Memo = Memo {
        constraint :: Maybe (Exp Var Bool, Memo),
        equal :: Maybe (Exp Var Bool, Memo),
        bool :: Maybe (Exp Var Bool, Memo),
        lessEqual :: Maybe (Exp Var Bool, Memo),
        polynomial :: Maybe (Exp Var Number, Memo),
        number :: Maybe (Exp Var Number, Memo),
        token :: Maybe (String, Memo) }

type Var = String
```

ここではパースの基本単位を文字ではなく文字列とした。読み込む文字をチェックする関数と、指定した一単語を読み込む関数を定義する。

```haskell:src/Data/Derivation/Parse.hs
check :: (String -> Bool) -> Parse Memo String
check p = parse token >>= \t -> B.bool empty (pure t) (p t)

pick :: String -> Parse Memo String
pick = check . (==)
```

多項式を解析するパーサを定義する。

```haskell:src/Data/Derivation/Parse.hs
pPolynomial :: Parse Memo (Exp Var Number)
pPolynomial = foldl (&) <$> parse number <*> many (
        flip (:+) <$> (pick "+" *> parse number) <|>
        flip (:-) <$> (pick "-" *> parse number) )

pNumber :: Parse Memo (Exp Var Number)
pNumber =
        Const . read <$> check (all isDigit) <|> Var <$> check (all isLower) <|>
        pick "(" *> parse polynomial <* pick ")"
```

パーサ`pPolynomial`の定義について解説する。式`foldl (&) x [f, g, h, ...]`は、値`x`に関数`f`, `g`,
 `h`, ...をつぎつぎに適用していく式になる。`foldl (&)`に続く式は、`parse number`で数値を読み込み、続く式では「+数」または「-数」という構造の複数の並びを読み込む。解析の結果として、値構築子`(:+)`または`(:-)`によって、つぎつぎに数式が接続されていく構造がかえされる。

パーサ`pNumber`では、`all isDigit`でチェックされる数値リテラル、`all isLower`でチェックされる変数、そして`()`でかこまれた数式のどれかが「数」としてあつかわれることが示される。

試すために、メモ用の型の値を構成する関数memoのうち定義できる部分だけを定義する。

```haskell:src/Data/Derivation/Parse.hs
memo :: [String] -> Memo
memo ts = m where
        m = Memo ct eq bl le pl nm tk
        ct = undefined
        eq = undefined
        bl = undefined
        le = undefined
        pl = unparse pPolynomial m
        nm = unparse pNumber m
        tk = (memo `second`) <$> uncons ts
```

`Memo`型の値のうちフィールド`polynomial`, `number`, `token`だけが定義できる。文字列をトークンに分割する関数`tokens`を定義しておく。

```src/Data/Derivation/Parse.hs
tokens :: String -> [String]
tokens = unfoldr (listToMaybe . lex) 
```

`polynomial`の解析を試してみよう。

```
% stack ghci --ghc-options -fobject-code
> :module Data.Derivation.Parse
> fst <$> polynomial (memo $ tokens "3 + 5 - (9 - 8)")
Just ((:-) ((:+) (Const 3) (Const 5)) ((:-) (Const 9) (Const 8))))
```

つぎは等値や小なりイコールで表される「制約」を解析する部分を書く。変数がブール値である場合と数値である場合とがあるので、すこし複雑だ。PEG形式で見てみよう。

```
constraint <- equal / lessEqual

equal <-
        var '==' var !'+' !'-' !'<=' /
        var '==' polynomial !'<=' /
        var '==' bool /
        polynomial '==' polynomial /
        bool '==' bool

bool <- lessEqual / 'F' / 'T' / var

lessEqual <- polynomial '<=' polynomial
```

制約は等式または不等式だ。等式には、つぎのような種類がある。

* 変数 == 変数 (+, -, <= があとに続かない)
* 変数 == 数式 (<= があとに続かない)
* 変数 == ブール値
* 数式 == 数式
* ブール値 == ブール値

ブール値は不等式、偽、真、変数だ。不等式は、数式 <= 数式である。

これを、そのままコードに落とす。

```haskell:src/Data/Derivation/Parse.hs
pConstraint :: Parse Memo (Exp Var Bool)
pConstraint = parse equal <|> parse lessEqual

pEqual :: Parse Memo (Exp Var Bool)
pEqual =
        (:==) <$> var <* pick "==" <*> var
                >>! (pick "+" <|> pick "-" <|> pick "<=") <|>
        (:==) <$> var <* pick "==" <*> parse polynomial >>! pick "<=" <|>
        (:==) <$> var <* pick "==" <*> parse bool <|>
        (:==) <$> parse polynomial <* pick "==" <*> parse polynomial <|>
        (:==) <$> parse bool <* pick "==" <*> parse bool
        where var = Var <$> check (all isLower)

pBool :: Parse Memo (Exp Var Bool)
pBool = parse lessEqual <|>
        Bool False <$ pick "F" <|> Bool True <$ pick "T" <|>
        Var <$> check (all isLower)

pLessEqual :: Parse Memo (Exp Var Bool)
pLessEqual = (:<=) <$> parse polynomial <* pick "<=" <*> parse polynomial
```

関数memoの定義してなかった部分をうめる。

```haskell:src/Data/Derivation/Parse.hs
memo :: [String] -> Memo
memo ts = m where
        m = Memo ct eq bl le pl nm tk
        ct = unparse pConstraint m
        eq = unparse pEqual m
        bl = unparse pBool m
        le = unparse pLessEqual m
        pl = unparse pPolynomial m
        nm = unparse pNumber m
        tk = (memo `second`) <$> uncons ts
```

関数`memo`や`tokens`をまとめた関数`parseConstraint`と`parsePolynomial`を定義する。

```haskell:src/Data/Derivation/Parse.hs
parseConstraint :: String -> Maybe (Exp Var Bool)
parseConstraint src = fst <$> constraint (memo $ tokens src)

parsePolynomial :: String -> Maybe (Exp Var Number)
parsePolynomial src = fst <$> polynomial (memo $ tokens src)
```

対話環境で試してみよう。

```
% stack ghci --ghc-options -fobject-code
> parseConstraint "n + 3 <= m == T"
Just ((:==) ((:<=) (Var "n") (Const 3)) (Var "m")) (Bool True))
> parsePolynomial "m + n - 3"
Just ((:-) ((:+) (Var "m") (Var "n")) (Const 3))
```

#### 多項式を表す型

`Exp`型のままだと「`given`から`wanted`が導出できるか」をチェックする操作は難しいので、`Exp`型からより操作しやすい型に変換する。はじめに、`Exp v Num`型から多項式を表す型に変換する関数を定義する。それを使って、`Exp v Bool`型から制約を表す型に変換する関数を定義しよう。モジュール`Data.Map.Strict`を使うので、依存パッケージに`containers`を追加しよう。

```
% vim package.yaml
...
dependencies:
- base >= 4.7 && < 5
- ghc
- transformers
- monads-tf
- containers
...
```

モジュール`Data.Derivation.Constraint`を用意する。

```haskell:src/Data/Derivation/Constraint.hs
{-# LANGUAGE BlockArguments, LambdaCase #-}
{-# OPTIONS_GHC -Wall -fno-warn-tabs #-}

module Data.Derivation.Constraint where

import Prelude hiding (null, filter, (<>))

import Control.Monad
import Data.Foldable (toList)
import Data.Maybe
import Data.Map.Strict (Map, null, singleton, (!?), filter, lookupMin)
import Data.Map.Merge.Strict

import qualified Data.Map.Strict as M
```

一次の多項式を表す型`Polynomial`を定義する。多項式が一意に定まるように、変数の名前でソートされた形にするので、データ型`Map`を利用する。

```haskell:src/Data/Derivation/Constraint.hs
type Polynomial v = Map (Maybe v) Integer
```

定数項を`Nothing`で表現し、1次の項は変数名が`x`であれば`Just "x"`のように表現するようにした。

多項式どうしの加算、減算を定義する。これにはモジュール`Data.Map.Merge.Strict`の関数`merge`が使える。

```haskell:src/Data/Derivation/Constraint.hs
(.+), (.-) :: Ord v => Polynomial v -> Polynomial v -> Polynomial v
(.+) = merge preserveMissing preserveMissing
        (zipWithMaybeMatched \_ a b -> rmZero $ a + b)
(.-) = merge preserveMissing (mapMissing $ const negate)
        (zipWithMaybeMatched \_ a b -> rmZero $ a - b)

rmZero :: (Eq n, Num n) => n -> Maybe n
rmZero = \case 0 -> Nothing; n -> Just n
```

関数`merge`では、それぞれのキーについて、かたほうだけ値がある場合と両方に値がある場合とで処理を定義することができる。関数`(.+)`ではかたほうだけに値があったときには、値はそのままとし、両方に値があったときには、それらを加算した値とする。もしも値が0だったら、その値は消去する。関数`(.-)`でも同様の処理をするが、もし後の引数にだけしか値がなかった場合には「そのまま」とするのではなく「符号を反転」する。

#### 制約を表す型

制約を表す型は`Polynomial`型によって表される多項式が0と等しいか、または0以上であるという形で制約を保存するようにする。

```haskell:src/Data/Derivation/Constraint.hs
data Constraint v = Eq (Polynomial v) | Geq (Polynomial v)
        deriving (Show, Eq, Ord)
```

値`Eq p1`は`p1`で表現される多項式が0に等しいという意味であり、値`Geq p2`は`p2`で表現される多項式が0以上であるという意味である。

`Constraint`型の値を構成する関数を定義する。ふたつの多項式について、等値、大なりイコール、大なりの3種の関係について、制約型の値を構成できるようにする。

```haskell:src/Data/Derivation/Constraing.hs
equal :: Ord v => Polynomial v -> Polynomial v -> Constraint v
l `equal` r = Eq . formatEq $ l .- r

greatEqualThan :: Ord v => Polynomial v -> Polynomial v -> Constraint v
l `greatEqualThan` r = Geq . formatGeq $ l .- r

greatThan :: Ord v => Polynomial v -> Polynomial v -> Constraint v
l `greatThan` r = Geq $ formatGeq (l .- r) .- singleton Nothing 1

formatEq :: Polynomial v -> Polynomial v
formatEq p =
        maybe p ((p `divide` divisor p `times`) . signum . snd) $ lookupMin p

formatGeq :: Polynomial v -> Polynomial v
formatGeq p = p `divide` divisor p

times, divide :: Polynomial v -> Integer -> Polynomial v
p `times` n = (* n) <$> p
p `divide` n = (`div` n) <$> p

divisor :: Polynomial v -> Integer
divisor = gcdAll . toList where gcdAll = \case [] -> 1; n : ns -> foldr gcd n ns
```

関数`equal`はふたつの多項式どうしで減算を行い、結果を関数`formatEq`で整えて値構築子`Eq`を適用している。関数`greatEqualThan`も同様だが、結果は関数`formatGeq`で整えたうえで値構築子`Geq`を適用している。関数`greatThan`は`greatEqualThan`と同様だが形を整えたうえで多項式から1(`singleton Nothing 1`)減らしている。

関数`formatEq`では、すべての項を最大公約数で除算したうえで、定数項または`Ord`として最小となる変数が正となるように、必要に応じて`- 1`をかけている。これは同等な制約どうしが一意に表現されるようにするための変換だ。関数`formatGeq`は最大公約数で除算するだけだ。

#### `Exp v Num`型の値を多項式に変換する

`Exp v Num`型の値を多項式に変換する関数を定義する。変換の途中で、たとえば`m - 3`のような式が出てきた場合、`m >= 3`という制約も必要になるので、そのような制約を保存しながら変換する関数とする。もちろん`m`の値も0以上であるので、そのような制約も追加する。これには(いろいろ問題はあるようだが)`Writer`モナドを使用する。

モジュール`Data.Derivation.Expression`に変換用の関数を定義する。まずは、いくつかのモジュールを導入する。

```haskell:src/Data/Derivation/Expression.hs
import Control.Monad.Writer (Writer, runWriter, tell)
import Data.Map.Strict (Map, (!?), empty, singleton, insert)

import Data.Derivation.Constraint
```

関数`poly`を定義する。

```haskell:src/Data.Derivation/Expression.hs
poly :: Ord v => Exp v Number -> Writer [Constraint v] (Polynomial v)
poly (Const n) = pure $ singleton Nothing n
poly (Var v) = p <$ tell [p `greatEqualThan` empty]
        where p = singleton (Just v) 1
poly (l :+ r) = (.+) <$> poly l <*> poly r
poly (l :- r) = (,) <$> poly l <*> poly r >>= \(pl, pr) ->
        pl .- pr <$ tell [pl `greatEqualThan` pr]
```

定数項(`Const n`)ではキー`Nothing`と値`n`のペアをかえす。変数(`Var v`)ではキーが`Just v`で値は`1`のようなペア`p`を定義したうえで、その`p`が0(`empty`)以上であるという制約を追加している。加算(`:+`)では再帰的に関数`poly`を適用した結果どうしを演算子`(.+)`で加算している。減算についても、だいたいおなじだが、減算の結果が0以上であるための制約を追加している。

試してみよう。

```
% stack ghci --ghc-options -fobject-code
> poly <$> parsePolynomial "m + n - 3"
Just (WriterT (Identity (fromList [(Nothing,-3),(Just "m",1),(Just "n",1)],[Geq (fromLIst [(Just "m",1)]),Geq (fromList [(Just "n",1)]),Geq (fromList [(Nothing,-3),(Just "m",1),(Just "n",1)])])))
```

`Writer`モナドの返り値としては、`fromList [(Nothing,-3),(Just "m",1),(Just "n",1)]`となっていて、これは求める多項式の表現である。`Writer`モナドの副産物は以下のみっつになっている。

* `Geq (fromList [(Just "m",1)])`
* `Geq (fromList [(Just "n",1)])`
* `Geq (fromList [(Nothing,-3),(Just "m",1),(Just "n",1)])`

それぞれ、`m >= 0`, `n >= 0`, `-3 + m + n >= 0`を表している。

#### `Exp v Bool`型の値を制約に変換する

まずは、変数と`Bool`値とを対応づける関数を定義する。たとえば、つぎのようになっていたとする。

```
b1 ~ False
b1 ~ b2
```

とすると、`b1 = False`, `b2 = False`ということになる。このような対応づけをする関数を定義する。まずは、必要なモジュールを導入する。

```haskell:src/Data/Derivation/Expression.hs
import Control.Arrow (first, second)
import Data.Maybe
import Data.List (find)
```

関数`mkVarBool`を定義する。

```haskell:src/Data/Derivation/Expression.hs
type VarBool v = Map v Bool

mkVarBool :: Ord v => [Exp v Bool] -> VarBool v
mkVarBool = snd . untilFixed (uncurry vbStep) . vbInit

vbInit :: Ord v => [Exp v Bool] -> ([(v, v)], VarBool v)
vbInit [] = ([], empty)
vbInit (Var l :== Var r : es) = ((l, r) :) `first` vbInit es
vbInit (Var l :== Bool r : es) = insert l r `second` vbInit es
vbInit (Bool l :== Var r : es) = insert r l `second` vbInit es
vbInit (_ : es) = vbInit es

vbStep :: Ord v => [(v, v)] -> VarBool v -> ([(v, v)], VarBool v)
vbStep [] vb = ([], vb)
vbStep ((l, r) : vs) vb = case (vb !? l, vb!? r) of
        (Just bl, _) -> vbStep vs $ insert r bl vb
        (Nothing, Just br) -> vbStep vs $ insert l br vb
        (Nothing, Nothing) -> ((l, r) :) `first` vbStep vs vb

untilFixed :: Eq a => (a -> a) -> a -> a
untilFixed f x = fst . fromJust . find (uncurry (==)) $ zip xs (tail xs)
        where xs = iterate f x
```

関数`vbInit`では、`Exp`型の値のリストから、等値になっている変数のペアと、ブール値として値が確定した変数とを取り出している。関数`vbStep`では、等値になっている変数のペアのかたほうのブール値が定まっている場合に、もうかたほうをその値に確定する。関数untilFixedは、値の変化がなくなるまで何度も関数を適用する。試してみよう。

```
% stack ghci --ghc-options -fobject-code
> :module + Data.Maybe
> mkVarBool $ mapMaybe parseConstraint ["a == F", "a == b", "c == d", "d == e", "d == T"]
fromList [("a",False),("b",False),("c",True),("d",True),("e",True)]
```

`Exp v Bool`型の値を`Constraint`型の値に変換する関数を定義する。

```haskell:src/Data/Derivation/Expression.hs
procProp :: Ord v => VarBool v ->
        Exp v Bool -> Bool -> Writer [Constraint v] (Maybe (Constraint v))
procProp _ (Bool _) _ = pure Nothing; procProp _ (Var _) _ = pure Nothing
procProp _ (l :<= r) False = Just <$> (greatThan <$> poly l <*> poly r)
procProp _ (l :<= r) True = Just <$> (greatEqualThan <$> poly r <*> poly l)
procProp vb (l :== Bool r) b = procProp vb l (r == b)
procProp vb (Bool l :== r) b = procProp vb r (l == b)
procProp vb (l :== Var r) b | Just br <- vb !? r = case l of
        _ :== _ -> procProp vb l (br == b); _ :<= _ -> procProp vb l (br == b)
        _ -> pure Nothing
procProp vb (Var l :== r) b | Just bl <- vb !? l = case r of
        _ :== _ -> procProp vb r (bl == b); _ :<= _ -> procProp vb r (bl == b)
        _ -> pure Nothing
procProp _ (l :== r) True = case (l, r) of
        (Const _, _) -> Just <$> (equal <$> poly l <*> poly r)
        (_ :+ _, _) -> Just <$> (equal <$> poly l <*> poly r)
        (_ :- _, _) -> Just <$> (equal <$> poly l <*> poly r)
        (_, Const _) -> Just <$> (equal <$> poly l <*> poly r)
        (_, _ :+ _) -> Just <$> (equal <$> poly l <*> poly r)
        (_, _ :- _) -> Just <$> (equal <$> poly l <*> poly r)
        (Var v, Var w) -> Just <$> (equal <$> poly (Var v) <*> poly (Var w))
        _ -> pure Nothing
procProp _ (_ :== _) False = pure Nothing
```

関数`procProp`の第1引数は関数`mkVarBool`の返り値であるような「ブール値を表す変数とブール値の対応を表す辞書」だ。第2引数は全体としてブール値になる`Exp`型の値である。第3引数は第2引数が`False`になるべきか、`True`になるべきかを指定する。たとえば`l :<= r`が`False`なら`l`は`r`より大きい。`True`なら`r`は`l`以上になる。

`:==`の左右のどちらかがブール値`b`であるなら、もう一方の値は全体として「第3引数 == `b`」の値になる。`:==`の左右のどちらかが変数であり、それがブール値に対応づけられているなら、対応づけられたブール値に対して同様の処理になる。それ以外で第2引数が`l :== r`という形であり第3引数が`True`ならば、どちらかの辺が`Const _`, `_ :+ _`, `_ :- _`という形であるか、または両辺ともに`Var _`という形であれば、両辺を多項式として両辺が等しいということ。

関数`mkConstraint`は関数`procProp`に必要な引数をあたえて、`Writer`モナドから中身を取り出す。

```haskell:src/Data/Derivation/Expression.hs
mkConstraint :: Ord v =>
        VarBool v -> Exp v Bool -> (Maybe (Constraint v), [Constraint v])
mkConstraint vb e = runWriter $ procProp vb e True
```

試してみる。

```
% stack ghci --ghc-options -fobject-code
> :module + Data.Maybe
> es = catMaybes $ parseConstraint <$> ["m + n <= 8 == b", "b == F"]
> mkConstraint (mkVarBool es) <$> es
[(Just (Geq (fromList [(Nothing,-9),(Just "m",1),(Just "n",1)])),[Geq (fromList ([Just "m",1)]),Geq (fromList [(Just "n",1)])]),(Nothing,[])]
```

つぎのような条件を求み込んだ。

* m + n <= 8 == b
* b == F

結果として、つぎのような条件が得られた。

* -9 + m + n >= 0
* m >= 0
* n >= 0

#### `Constraint`型をあつかういくつかの関数

ここで、`given`から`wanted`を導出できるか判定するのに必要な、いくつかの関数を定義する。

* `getVars`: 制約のなかに含まれるすべての変数
* `hasVar`: その制約が指定した変数を含むかどうか
* `rmNegative`: `Geq`のなかみから負の値を消去する
* `isDeriveFrom`: 第1引数の制約が第2引数の制約から導けるかどうか
* `selfContained`: その制約はそれ自体で成り立っているかどうか

関数`getVars`と`hasVar`を定義する。

```haskell:src/Data/Derivation/Constraint.hs
getVars :: Ord v => Constraint v -> [Maybe v]
getVars (Eq p) = (fst <$>) $ M.toList p
getVars (Geq p) = (fst <$>) $ M.toList p

hasVar :: Ord v => Constraint v -> Maybe v -> Bool
hasVar (Eq p) v = isJust $ p !? v
hasVar (Geq p) v = isJust $ p !? v
```

変数`x`は`Just "x"`のように表される。定数については`Nothing`で表現される。試してみる。

```
% stack ghci --ghc-options -fobject-code
> :module + Data.Map.Strict
> :module + Data.Maybe
> c = fromJust . fst . fromJust $ mkConstraint empty <$> parseConstraint "m + n - p <= 3"
> getVars c
[Nothing,Just "m",Just "n",Just "p"]
> hasVar c (Just "m")
True
> hasVar c (Just "x")
False
```

関数`rmNegative`, `isDerivFrom`, `selfContained`を定義する。

```haskell:src/Data/Derivation/Constraint.hs
rmNegative :: Constraint v -> Constraint v
rmNegative = \case eq@(Eq _) -> eq; Gep p -> Geq $ filter (>= 0) p

isDerivFrom :: Ord v => Constraint v -> Constraint v -> Bool
Eq w `isDerivFrom` Eq g = w == g
Geq w `isDerivFrom` Geq g = w `isGeqThan` g
_ `isDerivFrom` _ = False

isGeqThan :: Ord v => Polynomial v -> Polynomial v -> Bool
l `isGeqThan` r = and $ merge
        (mapMissing \_ nl -> nl >= 0)
        (mapMissing \_ nr -> nr <= 0) (zipWithMatched $ const (>=)) l r

selfContained :: Constraint v -> Bool
selfContained = \case Eq p -> null p; Geq p -> and $ (>= 0) <$> p
```

関数`rmNegative`は`Geq p`の`p`から0以上の値だけ取り出している。自然数をあつかっているので、たとえば`m - n + x - 1 >= 0`であれば、`m + x >= 0`でもあるはずだ。つまり、負の係数をもつ項を削除したものも条件として追加できるということだ。

関数`isDerivFrom`は`Eq w`と`Eq g`であれば`w`と`g`が等値である必要があるが、`Geq w`と`Geq g`であれば`w`が`g`以上ならいい。関数`isGeqThan`では関数`merge`を利用して、すべての係数で第1引数のほうが大きいことをチェックしている。関数`selfContained`では`Eq p`であれば`p`が空であることを、`Geq p`であれば、すべての係数が0以上であることをチェックしている。

#### ふたつの制約で、ひとつ変数を消去する

たとえば、つぎのような、ふたつの制約があるとする。

```
a + b - 3m + n == 0
c + d + 2m - 2n == 0
```

1行目の式を2倍して、2行目の式を3倍して足し合わせることで、変数mを消すことができる。

```
2a + 2b + 3c + 3d - 4n == 0
```

このように、ふたつの式があるときには、変数をひとつ消去できることがある。基本的な戦略としては消そうとする変数の係数をそろえて、符号を逆にして足し合わせることだ。関数`rmVar`を定義する。

```haskell:src/Data/Derivation/Constraint.hs
rmVar ::
        Ord v => Constraint v -> Constraint v -> Maybe v -> Maybe (Constraint v)
rmVar (Eq l) (Eq r) v = Eq . formatEq . uncurry (.+) <$> alignEE l r v
rmVar (Eq l) (Geq r) v = Geq . formatGeq . uncurry (.+) <$> alignEG l r v
rmVar (Geq l) (Geq r) v = Geq . formatGeq . uncurry (.+) <$> alignGG l r v
rmVar l r v = rmVar r l v

type Aligned v = Maybe (Polynomial v, Polynomial v)

alignEE :: Ord v => Polynomial v -> Polynomial v -> Maybe v -> Aligned v
alignEE l r v = (<$> ((,) <$> l !? v <*> r !? v)) \(nl, nr) ->
        (l `times` nr, r `times` (- nl))

alignEG :: Ord v => Polynomial v -> Polynomial v -> Maybe v -> Aligned v
alignEG l r v = (<$> ((,) <$> l !? v <*> r !? v)) \(nl, nr) ->
        (l `times` (- signum nl * nr), r `times` abs nl)

alignGG :: Ord v => Polynomial v -> Polynomial v -> Maybe v -> Aligned v
alignGG l r v = (,) <$> l !? v <*> r !? v >>= \(nl, nr) -> do
        guard $ nl * nr < 0
        pure (l `times` abs nr, r `times` abs nl)
```

ふたつの制約について係数を合わせて、符号を逆にして足し合わせている。不等式については負の値をかけることができないので、「係数を合わせて、符号を逆にする」処理は3通り用意する必要がある。

* 等式と等式: 符号にかかわらず、どちらかの係数の符号を反転すればいい
* 等式と不等式: 不等式のほうには絶対値をかける、等式のほうは係数が不等式のほうの係数の符号を反転させたものになるようにする
    + `signum x`を`x`にかけると符号は正になる(`x`が0でないとき)
    + それに相手側の係数をかけると、両者の係数の正負がそろう
    + さらに`-`で符号を反転させる
* 不等式と不等式: 両者の係数の符号が逆であるときのみ、両方に絶対値をかける

#### あたえられた制約から求める制約が導出できるか

`given`から`wanted`を導出できるかをチェックする関数を定義する。モジュール`Data.Derivation.CanDerive`を用意する。

```haskell:src/Data/Derivation/CanDerive.hs
{-# LANGUAGE BlockArguments #-}
{-# OPTIONS_GHC -Wall -fno-warn-tabs #-}

module Data.Derivation.CanDerive where

import Data.Either
import Data.List ((\\), nub, partition, sort, unfoldr)
import Data.Map.Strict (empty)
import Data.Bool

import Data.Derivation.Constraint (
        Constraint, getVars, hasVar,
        rmNegative, isDerivFrom, selfContained )
import Data.Derivation.Expression

import qualified Data.Derivation.Constraint as C
```

あたえられた制約を表す型`Given`を定義する。

```haskell:src/Data/Derivation/CanDerive.hs
newtype Given v = Given { unGiven :: [Constraint v] } deriving Show

mkGiven :: Ord v => [Exp v Bool] -> Given v
mkGiven es = given . concat
        $ uncurry (maybe id (:)) . mkConstraint (mkVarBool es) <$> es

given :: Ord v => [Constraint v] -> Given v
given zs = Given . nub . sort $ zs ++ (rmNegative <$> zs)

givenVars :: Ord v => Given v -> [Maybe v]
givenVars = nub . sort . concat . (getVars <$>) . unGiven
```

型`Given`は複数の制約から成る型だ。複数の`Exp v Bool`型の値から`mkConstraint`で組み立てた`Constraint`型の値を、整列して重複をなくしている。また`rmNegative`で不等式の負の係数を持つ値を消去したものも、新たな制約として追加している。関数`givenVars`は、あたえられた制約が含むすべての変数を返す。

型Wantedを定義する。

```haskell:src/Data/Derivation/CanDerive.hs
newtype Wanted v = Wanted { unWanted :: [Wanted1 v] } deriving Show

type Wanted1 v = Constraint v

mkWanted :: Ord v => Exp v Bool -> Maybe (Wanted v)
mkWanted = uncurry wanted . mkConstraint empty

wanted :: Maybe (Wanted1 v) -> [Wanted1 v] -> Maybe (Wanted v)
wanted mw ws = Wanted . (: ws) <$> mw
```

関数`mkConstraint`で`Exp`型の値から変換した制約のうち、追加ではない主となる制約は`Maybe Constraint`型でタプルの第1要素として返される。これが`Just`値でなければ、`Wanted`型としては読み込みに失敗したことになる。関数`wanted`はそのあたりを処理している。

`Given`型から変数を消去する関数を定義する。

```haskell:src/Data/Derivation/CanDerive.hs
rmVar :: Ord v => Given v -> Maybe v -> Given v
rmVar (Given g) v =
        Given . sort $ r ++ concat (unfoldUntil null (`rvStep` v) g')
        where (g', r) = partition (`hasVar` v) g

rvStep :: Ord v => [Constraint v] -> Maybe v -> ([Constraint v], [Constraint v])
rvStep [] _ = ([], [])
rvStep (c : cs) v = partitionEithers $ flip (rmVar1 c) v <$> cs

rmVar1 :: Ord v => Constraint v ->
        Constraint v -> Maybe v -> Either (Constraint v) (Constraint v)
rmVar1 c0 c v = maybe (Right c) Left $ C.rmVar c0 c v

unfoldUntil :: (s -> Bool) -> (s -> (r, s)) -> s -> [r]
unfoldUntil p f = unfildr \s -> bool (Just $ f s) Nothing (p s)
```

関数`rmVar1`は第1引数と第2引数の制約で第3引数の変数を消去しようとする。消去できたら結果の制約を`Left`値として返し、消去できなければ第2引数の制約をそのまま`Right`値として返す。

関数`rvStep`はリストの先頭の制約を残りの制約すべてとペアにして、変数の消去を試みる。関数`partitionEither`によって消去できたものについては、結果のタプルの第1要素になり、消去できなかったものについては、結果のタプルの第2要素になる。

関数`unfoldUntil`では状態`s`が条件を満たすまで、値を取り出しながら状態を変化させていく関数を実行し続け、取り出した値をリストにする関数だ。

関数`rmVar`では、これらの関数を合わせることで、消去できなかった制約がなくなるまで、変数の消去を試みる関数となっている。

`given`から`wanted`が導出できるかどうかチェックする関数を定義する。

```haskell:src/Data/Derivation/CanDerive.hs
canDerive :: Ord v => Given v -> Wanted v -> Bool
canCerive g = all (canDerive1 g) . unWanted

canDerive1 :: Ord v => Given v -> Wanted1 v -> Bool
canDerive1 g w = selfContained w ||
        any (isDerivFrom w) (unGiven . foldl rmVar g $ givenVars g \\ getVars w)
```

`Wanted`の制約のひとつについて導出可能かどうか調べる関数`canDerive1`を使って、`Wanted`の制約すべてを導出可能か調べる関数`canDerive`を定義している。関数`canDerive1`がしているのは、`Given`に含まれる複数の制約について、`Wanted`のほうに含まれない変数をすべて消去して、その結果のなかに`Wanted`のほうの制約とおなじか、より厳しいものがあるかどうかを調べている。試してみよう。

```
% stack ghci --ghc-options -fobject-code
> :module + Data.Maybe
> g = mkGiven . catMaybes $ parseConstraint <$> ["m + 1 == k", "n + 1 == j", "k == j"]
> w = fromJust $ mkWanted =<< parseConstraint "m == n"
> canDerive g w
True
> w' = fromJust $ mkWanted =<< parseConstraint "m + 1 == n"
> canDerive g w'
False
```

### 型チェックプラグインの完成

必要なモジュールを導入する。

```haskell:src/Plugin/TypeCheck/Nat/Simple.hs
import TcEvidence
import TyCoRep
import Data.Bool
import Data.Either

import Data.Derivation.CanDerive
```

`given`を表す`Ct`型の値のリストから`Given`型の値を作成し、`wanted`を表す`Ct`型の値から`Wanted`型の値を作成し、導出可能かどうかを調べ、導出可能であれば`(EvTerm, Ct)`をそうでなければエラー値を返す関数を定義する。

```haskell:src/Plugin/TypeCheck/Nat/Simple.hs
result :: [Ct] -> Ct -> Except Message (EvTerm, Ct)
result gs w = unNomEq w >>= \(l, r) ->
        bool (throwE em) (pure (et l r, w)) . canDerive g =<< wnt =<< decode l r
        where
        em = "result: fail"
        g = mkGiven . rights $ runExcept . (uncurry decode =<<) . unNomEq <$> gs
        wnt = maybe (throwE "mkWanted: fail") pure . mkWanted
        et l r = EvExpr . Coercion $
                mkUnivCo (PluginProv "Plugin.TypeCheck.Nat.Simple") Nominal l r
```

`bool (throwE em) (pure (et l r, w))`は続く引数の値が`False`ならエラー値を返し、`True`なら`(et l r, w)`を返すということだ。ローカル関数`et`は`Type`型の値をふたつ引数としてとり、`EvTerm`型の値を返す関数だ。`et l r`とすることで、「`l`と`r`とは同一視できますよ」といった内容を表現している。ローカル変数`g`は`Given`型の値であり、`Ct`型の値のリストから、関数`unNomEq`, `decode`, `mkGiven`によって組み立てられる。`canDerive g =<< wnt =<< decode l r`は、ふたつの`Type`型の値`l`, `r`から`Wanted`型の値を組み立てて、それを`canDerive g`にわたすことで`given`から`wanted`を導出可能か調べている。ローカル関数`wnt`は`mkWanted`について`Maybe`モナドから`Exception`モナドに変換したものだ。

関数`result`を使って、関数`solve`の最終行を書き換える。

```haskell:src/Plugin/TypeCheck/Nat/Simple.hs
        pure $ TcPluginOk (rights $ runExcept . result gs <$> ws) []
```

これで、型チェックプラグインが完成した。モジュール`Trial.TryTypeCheck`で試してみよう。コメントアウトした関数`bar`を、もとにもどそう。

```haskell:src/Trial/TryTypeCheck.hs
bar :: (a + 1) ~ (b + 1) => Proxy a -> Proxy b
bar = id
```

今度は、ちゃんと型チェックが通るだろう。

要素の個数の範囲を型レベルで指定できるリスト: Range
--------------------------------------------

### 要素を左に追加していく構造: RangeL

#### オプショナルな要素を追加する

ようやく、`RangeL`の実装にもどることができる。`OPTIONS_GHC`プラグマにオプション`-fplugin=Plugin.TypeCheck.Nat.Simple`を追加しよう。

```haskell:src/Data/List/Range/RangeL.hs
{-# OPTIONS_GHC -Wall -fno-warn-tabs -fplugin=Plugin.TypeCheck.Nat.Simple #-}
```

コメントアウトしておいた`instance PushL ...`の部分をもとにもどす。

```haskell:src/Data/List/Range/RangeL.hs
instance PushL 0 m where (.:..) = (:..)

instance {-# OVERLAPPABLE #-} PushL (n - 1) (m - 1) => PushL n m where
        x .:.. (y :. ys) = x :. (y .:.. ys)
        _ .:.. _ = error "never occur"
```

試してみよう。

```
% stack ghci --ghc-options -fobject-code
> :set -XDataKinds
> lst = 3 :. 4 :. 5 :. NilL :: RangeL 3 5 Integer
> 2 .:.. lst
2 :. (3 :. (4 :. (5 :.. NilL)))
> 1 .:.. it
1 :. (2 :. (3 :. (4 :.. (5 :.. NilL))))
```

#### 条件のゆるいリストに変換する

要素の個数について、より条件のゆるいリストへの変換は安全だ。条件のゆるいリストに変換する関数を定義する。

##### 最小の個数を減らす

まずは最小の個数を減らしてみよう。型クラス`LoosenLMin`を定義する。

```haskell:src/Data/List/Range/RangeL.hs
class LoosenLMin n m n' where loosenLMin :: RangeL n m a -> RangeL n' m a
```

`n`, `m`がもとのリストの要素の最小値と最大値であり、`n'`が新しく返されるリストの要素の最小値である。まずは最小値が操作の前後でどちらも`0`の場合を定義する。

```haskell:src/Data/List/Range/RangeL.hs
instance LoosenLMin 0 m 0 where
        loosenLMin NilL = NilL
        loosenLMin xa@(_ :.._) = xa
        loosenLMin _ = error "never occur"
```

この場合、変化はないので「そのまま」返せばいい。つぎに、新しいリストの要素の最小値が`0`の場合を定義する。

```haskell:src/Data/List/Range/RangeL.hs
instance {-# OVERLAPPABLE #-}
        LoosenLMin (n - 1) (m - 1) 0 => LoosenLMin n m 0 where
        loosenLMin (x :. xs) = x :.. loosenLMin xs
        loosenLMin _ = error "never occur"
```

新しいリストの要素はすべてオプショナルなので、値構築演算子`(:.)`をすべて`(:..)`に変換すればいい。最後に定義するのは、新しいリストの要素の最小値が`0`ではない場合だ。

```haskell:src/Data/List/Range/RangeL.hs
instance {-# OVERLAPPABLE #-}
        LoosenLMin (n - 1) (m - 1) (n' - 1) => LoosenLMin n m n' where
        loosenLMin (x :. xs) = x :. loosenLMin xs
        loosenLMin _ = error "never occur"
```

このように定義することで、新しいリストの要素の最小値が`0`でないあいだは値構築演算子`(:.)`でつなぎ、`0`になってからは`(:..)`でつなぐような処理とすることができる。試してみる。

```
% stack ghci --ghc-options -fobject-code
> :set -XDataKinds
> l = 1 :. 2 :. 3 :. 4 :. 5 :.. 6 :.. NilL :: RangeL 4 8 Integer
> loosenLMin l :: RangeL 2 8 Integer
1 :. (2 :. (3 :.. (4 :.. (5 :.. (6 :.. NilL)))))
```

##### 最大の個数を増やす

つぎは、最大の個数を増やしてみる。ますは型クラスを定義する。

```haskell:src/Data/List/Range/RangeL.hs
class LoosenLMax n m m' where loosenLMax :: RangeL n m a -> RangeL n m' a
```

`n`, `m`がもとのリストの要素の個数の最小値、最大値。`m'`は新しいリストの要素の個数の最大値だ。もとのリストの要素の個数が最小値、最大値ともに`0`である場合から定義していこう。

```haskell:src/Data/List/Range/RangeL.hs
instance LoosenLMax 0 0 m where
        loosenLMax NilL = NilL
        loosenLMax _ = error "never occur"
```

最小値、最大値ともに`0`なので、もとのリストの取り得る値は`NilL`だけだ。新しいリストも`NilL`になる。もとのリストの最小値が`0`で最大値が`0`でない場合の定義を続ける。

```haskell:src/Data/List/Range/RangeL.hs
instance {-# OVERLAPPABLE #-}
        LoosenLMax 0 (m - 1) (m' - 1) => LoosenLMax 0 m m' where
        loosenLMax NilL = NilL
        loosenLMax (x :.. xs) = x :.. loosenLMax xs
        loosenLMax _ = error "never occur"
```

リストの要素の個数の最小値が`0`なので取り得る値は`NilL`または`_ :.. _`だ。`NilL`に到達するまで値構築演算子を`(:..)`からおなじ`(:..)`に置き換えていけばいい。最後にリストの要素の個数の最小値が`0`でない場合を定義する。

```haskell:src/DAta/List/Range/RangeL.hs
instance {-# OVERLAPPABLE #-}
        LoosenLMax (n - 1) (m - 1) (m' - 1) => LoosenLMax n m m' where
        loosenLMax (x :. xs) = x :. loosenLMax xs
        loosenLMax _ = error "never occur"
```

リストの要素の個数の最小値が`0`になるまで値構築演算子`(:.)`をおなじ`(:.)`に置き換えていけばいい。試してみよう。

```
% stack ghci --ghc-optionhs -fobject-code
> :set -XDataKinds
> l = 1 :. 2 :. 3 :.. 4 :.. NilL :: RangeL 2 6 Integer
> loosenLMax l :: RangeL 2 8 Integer
1 :. (2 :. (3 :.. (4 :.. NilL)))
```

##### 最小、最大の個数をともにゆるくする

関数`loosenLMin`と`loosenLMax`とを組み合わせれば最小値、最大値をともにゆるくする関数が定義できる。

```haskell:src/Data/List/Range/RangeL.hs
loosenL :: (LoosenLMin n m n', LoosenLMax n' m m') =>
        RangeL n m a -> RangeL n' m' a
loosenL = loosenLMax . loosenLMin
```

試してみる。

```
% stack ghci --ghc-options -fobject-code
> :set -XDataKinds
> l = 1 :. 2 :. 3 :. 4 :. 5 :.. 6 :.. NilL :: RangeL 4 8 Integer
> loosenL l :: RangeL 2 10 Integer
1 :. (2 :. (3 :.. (4 :.. (5 :.. (6 :.. NilL)))))
```

#### リストの結合

リストの結合も型クラスを定義して、クラス関数として定義する。

```haskell:src/Data/List/Range/RangeL.hs
infixr 5 ++.

class AddL n m n' m' where
        (++.) :: RangeL n m a -> RangeL n' m' a -> RangeL (n + n') (m + m') a

instance AddL 0 0 n' m' where NilL ++. ys = ys; _ ++. _ = error "never occur"

instance {-# OVERLAPPABLE #-} (
        LoosenLMax n' m' (m + m'), PushL n' (m + m' - 1),
        AddL 0 (m - 1) n' m' ) => AddL 0 m n' m' where
        (++.) :: forall a .
                RangeL 0 m a -> RangeL n' m' a -> RangeL n' (m + m') a
        NilL ++. ys = loosenLMax ys
        x :.. xs ++. ys = x .:.. (xs ++. ys :: RangeL n' (m + m' - 1) a)
        _ ++. _ = error "never occur"

instance {-# OVERLAPPABLE #-}
        AddL (n - 1) (m - 1) n' m' => AddL n m n' m' where
        x :. xs ++. ys = x :. (xs ++. ys)
        _ ++. _ = error "never occur"
```

基本的には標準的な関数`(++)`の定義と同様だ。左辺のリストの要素の個数の最小値が`0`で最大値が`0`でないときが、やや複雑になる。まず左辺のリストが空だったときには右辺のリストの要素の個数の最大値を増やしたものが返り値になる。空でないときには、左辺のリストのはじめの要素はオプショナルなので、右辺に追加するときもオプショナルなものとして追加する。演算子`(.:..)`を使った。試してみよう。

```
% stack ghci --ghc-options -fobject-code
> :set -XDataKinds
> l = 1 :. 2 :. 3 :.. NilL :: RangeL 2 4 Integer
> r = 4 :. 5 :.. 6 :.. 7 :.. NilL :: RangeL 1 5 Integer
> lr = l ++. r
> lr
1 :. (2 :. (3 :. (4 :.. (5 :.. (6 :.. (7 :.. NilL))))))
> :type lr
lr :: RangeL 3 9 Integer
```

### 要素を右から追加する構造: RangeR

要素を右から追加する構造を定義する。データ型`RangeR`とそれをあつかう関数を定義していく。データ型`RangeL`での定義と、ほとんどおなじだ。

#### データ型`RangeR`

まずはモジュール`Data.List.Range.RangeR`を用意する。

```haskell:src/Data/List/Range/RangeR.hs
{-# LANGUAGE DataKinds, KindSignatures, TypeOperators #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE MultiParamTypeClasses, FlexibleContexts, FlexibleInstances,
        UndecidableInstances #-}
{-# OPTIONS_GHC -Wall -fno-warn-tabs -fplugin=Plugin.TypeCheck.Nat.Simple #-}

module Data.List.Range.RangeR where

import GHC.TypeLits
```

データ型`RangeR`を定義する。

```haskell:src/Data/List/Range/RangeR.hs
infixl 6 :+, :++

data RangeR :: Nat -> Nat -> * -> * where
        NilR :: RangeR 0 m a
        (:++) :: 1 <= m => RangeR 0 (m - 1) a -> a -> RangeR 0 m a
        (:+) :: RangeR (n - 1) (m - 1) a -> a -> RangeR n m a

deriving instance Show a => Show (RangeR n m a)
```

新しい要素を追加する位置が左ではなくて右になっている。それ以外は`RangeL`とおなじだ。値を定義してみよう。

```
% stack ghci --ghc-options -fobject-code
> :set -XDataKinds
> :module Data.List.Range.RangeR
> NilR :++ 1 :++ 2 :+ 3 :+ 4 :: RangeR 2 6 Integer
(((NilR :++ 1) :++ 2) :+ 3) :+ 4
```
#### 型クラス`Foldable`のインスタンスにする

```haskell:src/Data/List/Range/RangeR.hs
instance Foldable (RangeR 0 0) where
        foldr _ z NilR = z
        foldr _ _ _ = error "never occur"

instance {-# OVERLAPPABLE #-}
        Foldable (RangeR 0 (m - 1)) => Foldable (RangeR 0 m) where
        foldr _ z NilR = z
        foldr (-<) z (xs :++ x) = foldr (-<) (x -< z) xs
        foldr _ _ _ = error "never occur"

instance {-# OVERLAPPABLE #-}
        Foldable (RangeR (n - 1) (m - 1)) => Foldable (RangeR n m) where
        foldr (-<) z (xs :+ x) = foldr (-<) (x -< z) xs
        foldr _ _ _ = error "never occur"
```

右から出し入れするリストでは、左から出し入れする通常のリストと比較して、関数`foldr`と`foldl`の定義が逆になっている。右から出し入れするリストでの関数`foldr`の定義は、通常のリストの関数`foldl`の定義と似ている。試してみよう。

```
% stack ghci --ghc-options -fobject-code
> :set -XDataKinds
> :module Data.List.Range.RangeR
> sum (NilR :++ 1 :++ 2 :+ 3 :+ 4 :: RangeR 2 6 Integer)
10
```

#### オプショナルな要素の追加

一般的な`RangeR n m a`型の値に必須の要素を追加するには`(:+)`が使える。必須の要素のない`RangeR 0 m a`型のリストにオプショナルな要素を追加するには`(:++)`が使える。一般的な`RangeR n m a`型の値にオプショナルな要素を追加する演算子`(.:++)`を定義しよう。

```haskell:src/Data/List/Range/RangeR.hs
infixl 5 .:++

class PushR n m where (.:++) :: RangeR n m a -> a -> RangeR n (m + 1) a

instance PushR 0 m where (.:++) = (:++)

instance {-# OVERLAPPABLE #-} PushR (n - 1) (m - 1) => PushR n m where
        xs :+ x .:++ y = (xs .:++ x) :+ y
        _ .:++ _ = error "never occur"
```

試してみよう。

```
% stack ghci --ghc-options -fobject-code
> :set -XDataKinds
> :module Data.List.Range.RangeR
> l = NilR :++ 1 :++ 2 :+ 3 :+ 4 :: RangeR 2 6 Integer
> l .:++ 5
((((NilR :++ 1) :++ 2) :++ 3) :+ 4) :+ 5
> :type it
it :: RangeR 2 7 Integer
```

#### 条件のゆるいリストに変換する

最小の個数を減らす`loosenRMin`を定義する。

```haskell:src/Data/List/Range/RangeR.hs
class LoosenRMin n m n' where loosenRMin :: RangeR n m a -> RangeR n' m a

instance LoosenRMin 0 m 0 where
        loosenRMin NilR = NilR
        loosenRMin xa@(_ :++ _) = xa
        loosenRMin _ = error "never occur"

instance {-# OVERLAPPABLE #-}
        LoosenRMin (n - 1) (m - 1) 0 => LoosenRMin n m 0 where
        loosenRMin (xs :+ x) = loosenRMin xs :++ x
        loosenRMin _ = error "never occur"

instance {-# OVERLAPPABLE #-}
        LoosenRMin (n - 1) (m - 1) (n' - 1) => LoosenRMin n m n' where
        loosenRMin (xs :+ x) = loosenRMin xs :+ x
        loosenRMin _ = error "never occur"
```

`RangeL`での定義とだいたいおなじだ。試してみよう。

```
% stack ghci --ghc-options -fobject-code
> :set -XDataKinds
> :module Data.List.Range.RangeR
> l = NilR :++ 1 :++ 2 :+ 3 :+ 4 :+ 5 :+ 6 :: RangeR 4 8 Integer
> loosenR l :: RangeR 2 8 Integer
(((((NilR :++ 1) :++ 2) :++ 3) :++ 4) :+ 5) :+ 6
```

最大の個数を増やす`loosenRMax`を定義する。

```haskell:src/Data/List/Range/RangeR.hs
class LoosenRMax n m m' where loosenRMax :: RangeR n m a -> RangeR n m' a

instance LoosenRMax 0 0 m where
        loosenRMax NilR = NilR
        loosenRMax _ = error "never occur"

instance {-# OVERLAPPABLE #-}
        LoosenRMax 0 (m - 1) (m' - 1) => LoosenRMax 0 m m' where
        loosenRMax NilR = NilR
        loosenRMax (xs :++ x) = loosenRMax xs :++ x
        loosenRMax _ = error "never occur"

instance {-# OVERLAPPABLE #-}
        LoosenRMax (n - 1) (m - 1) (m' - 1) => LoosenRMax n m m' where
        loosenRMax (xs :+ x) = loosenRMax xs :+ x
        loosenRMax _ = error "never occur"
```

`RangeL`で定義したのとだいたいおなじだ。試してみる。

```
% stack ghci --ghc-options -fobject-code
> :set -XDataKinds
> :module Data.List.Range.RangeR
> l = NilR :++ 1 :++ 2 :+ 3 :+ 4 :: RangeR 2 6 Ingteger
> loosenRMax l :: RangeR 2 8 Integer
(((NilR :++ 1) :++ 2) :+ 3) :+ 4
```

最小の個数、最大の個数をともにゆるくする`loosenR`を定義する。

```haskell:src/Data/List/Range/RangeR.hs
loosenR :: (LoosenRMin n m n', LoosenRMax n' m m') =>
        RangeR n m a -> RangeR n' m' a
loosenR = loosenRMax . loosenRMin
```

### 左リストと右リストの相互変換

#### 左リストから右リストへの変換

左リストから右リストへの変換関数を定義していく。この変換関数を定義するには「右リストと左リストを結合して、結果を右リストとして返す」関数を定義して、その関数に空右リスト`NilR`をわたせばいい。まずはモジュールを用意する。

```haskell:src/Data/List/Range.hs
{-# LANGUAGE ScopedTypeVariables, InstanceSigs #-}
{-# LANGUAGE DataKinds, TypeOperators #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses, FlexibleContexts, FlexibleInstances,
        UndecidableInstances #-}
{-# OPTIONS_GHC -Wall -fno-warn-tabs -fplugin=Plugin.TypeCheck.Nat.Simple #-}

module Data.List.Range where

import GHC.TypeNats

import Data.List.Range.RangeL
import Data.List.Range.RangeR
```

型クラスを用意する。

```haskell:src/Data/List/Range.hs
infixl 5 ++.+

class LeftToRight n m v w where
        (++.+) :: RangeR n m a -> RangeL v w a -> RangeR (n + v) (m + w) a
```

右辺の左リストが空の場合は、そのまま返せばいい。

```haskell:src/Data/List/Range.hs
instance LeftToRight 0 m 0 0 where n ++.+ _ = n

instance {-# OVERLAPPABLE #-} LeftToRight n m 0 0 where n ++.+ _ = n
```

左辺の右リストにも右辺の左リストにも必須の要素がない場合を定義する。

```haskell:src/Data/List/Range.hs
instance {-# OVERLAPPABLE #-}
        (LoosenRMax 0 m (m + w), LeftToRight 0 (m + 1) 0 (w - 1)) =>
        LeftToRight 0 m 0 w where
        (++.+) :: forall a . RangeR 0 m a -> RangeL 0 w a -> RangeR 0 (m + w) a
        n ++.+ NilL = loosenRMax n :: RangeR 0 (m + w) a
        n ++.+ x :.. v = (n :++ x :: RangeR 0 (m + 1) a) ++.+ v
        _ ++.+ _ = error "never occur"
```

右辺の左リストが空リストならば、左辺の右リストの要素の個数の最大値を増やしたものをかえす。右辺の左リストが空でないときには、その先頭の要素を左辺の右リストの末尾に追加してやればいい。

つぎは、右辺の左リストの要素の最小値だけが`0`の場合を定義する。

```haskell:src/Data/List/Range.hs
instance {-# OVERLAPPABLE #-} (
        LoosenRMax n m (m + w), PushR (n - 1) (m - 1),
        LeftToRight n (m + 1) 0 (w - 1) ) =>
        LeftToRight n m 0 w where
        (++.+) :: forall a . RangeR n m a -> RangeL 0 w a -> RangeR n (m + w) a
        n ++.+ NilL = loosenRMax n :: RangeR n (m + w) a 
        n ++.+ x :.. v = (n .:++ x :: RangeR n (m + 1) a) ++.+ v
        _ ++.+ _ = error "never occur"
```

両辺のリストの要素の最小の個数が`0`だったときと同様だが、要素の追加に値構築演算子`(:++)`ではなく、代わりに演算子`(.:++)`を使っている。

両辺のリストがどちらも一般的な`RangeR n m a`、`RangeL v w a`だった場合を定義しよう。

```haskell:src/Data/List/Range.hs
instance {-# OVERLAPPABLE #-}
        LeftToRight (n + 1) (m + 1) (v - 1) (w - 1) =>
        LeftToRight n m v w where
        (++.+) :: forall a .
                RangeR n m a -> RangeL v w a -> RangeR (n + v) (m + w) a
        n ++.+ x :. v = (n :+ x :: RangeR (n + 1) (m + 1) a) ++.+ v
        _ ++.+ _ = error "never occur"
```

だいたいおなじだが、値の取り出しのパターンマッチに値構築演算子`(:.)`を使い、値の追加には値構築演算子`(:+)`を使っている。試してみよう。

```
% stack ghci --ghc-options -fobject-code
> :set -XDataKinds
> :module Data.List.Range Data.List.Range.RangeL Data.List.Range.RangeR
> n = NIlR :++ 1 :++ 2 :+ 3 :+ 4 :: RangeR 2 6 Integer
> v = 5 :. 6 :. 7 :.. 8 :.. NilL :: RangeL 2 6 Integer
> n ++.+ v
(((((((NilR :++ 1) :++ 2) :++ 3) :++ 4) :+ 5) :+ 6) :+ 7) :+ 8
> :type it
it :: RangeR 4 12 Integer 
```

左リストから右リストへの変換関数`leftToRight`を定義する。

```haskell:src/Data/List/Range.hs
leftToRight ::
        forall n m a . LeftToRight 0 0 n m => RangeL n m a -> RangeR n m a
leftToRight = ((NilR :: RangeR 0 0 a) ++.+)
```

#### 右リストから左リストへの変換

右リストから左リストへの変換も、同様に右リストと左リストを結合して結果を左リストにして返す関数を使って定義する。右リストと左リストを結合して左リストにして返す関数は、つぎのようになる。

```haskell:src/Data/List/Range.hs
infixr 5 ++..

class RightToLeft n m v w where
        (++..) :: RangeR n m a -> RangeL v w a -> RangeL (n + v) (m + w) a

instance RightToLeft 0 0 0 w where _ ++.. v = v

instance {-# OVERLAPPABLE #-} RightToLeft 0 0 v w where _ ++.. v = v

instance {-# OVERLAPPABLE #-}
        (LoosenLMax 0 w (m + w), RightToLeft 0 (m - 1) 0 (w + 1)) =>
        RightToLeft 0 m 0 w where
        (++..) :: forall a . RangeR 0 m a -> RangeL 0 w a -> RangeL 0 (m + w) a
        NilR ++.. v = loosenLMax v :: RangeL 0 (m + w) a
        n :++ x ++.. v = n ++.. (x :.. v :: RangeL 0 (w + 1) a)
        _ ++.. _ = error "never occur"

instance {-# OVERLAPPABLE #-} (
        LoosenLMax v w (m + w), PushL (v - 1) (w - 1),
        RightToLeft 0 (m - 1) v (w + 1) ) =>
        RightToLeft 0 m v w where
        (++..) :: forall a . RangeR 0 m a -> RangeL v w a -> RangeL v (m + w) a
        NilR ++.. v = loosenLMax v :: RangeL v (m + w) a
        n :++ x ++.. v = n ++.. (x .:.. v :: RangeL v (w + 1) a)
        _ ++.. _ = error "never occur"

instance {-# OVERLAPPABLE #-}
        RightToLeft (n - 1) (m - 1) (v + 1) (w + 1) =>
        RightToLeft n m v w where
        (++..) :: forall a .
                RangeR n m a -> RangeL v w a -> RangeL (n + v) (m + w) a
        n :+ x ++.. v = n ++.. (x :. v :: RangeL (v + 1) (w + 1) a)
        _ ++.. _ = error "never occur"
```

`LeftToRight`の定義とだいたいおなじだ。左辺の右リストから右辺の左リストに要素をひとつずつわたしていく形になっている。右リストから左リストに変換する関数`rightToLeft`を定義しておこう。

```haskell:src/Data/List/Range.hs
rightToLeft ::
        forall n m a . RightToLeft n m 0 0 => RangeR n m a -> RangeL n m a
rightToLeft = (++.. (NilL :: RangeL 0 0 a))
```

試してみよう。

```
% stack ghci --ghc-options -fobject-code
> :set -XDataKinds
> :module Data.List.Range Data.List.Range.RangeL Data.List.Range.RangeR
> rightToLeft (NilR :++ 1 :++ 2 :+ 3 :+ 4 :: RangeR 2 6 Integer)
1 :. (2 :. (3 :.. (4 :.. NilL)))
> :type it
it :: RangeL 2 6 Integer
```

### モジュール`Data.List.Range`のAPI

モジュール`Data.List.Range`から必要な型や関数を公開する。

```haskell:src/Data/List/Range.hs
module Data.List.Range (
        RangeL(..), PushL, AddL, LoosenLMin, LoosenLMax,
        (.:..), (++.), loosenLMax, loosenL,
        RangeR(..), PushR, LoosenRMin, LoosenRMax,
        (.:++), loosenRMax, loosenR,
        LeftToRight, (++.+), leftToRight,
        RightToLeft, (++..), rightToLeft ) where
```

両端に対する追加・取り出しが償却定数時間でできて、結合が対数時間でできる並びを表すデータ構造: Finger Tree
------------------------------------------------------------------------------------------

ここまで定義してきた型`RangeL`, `RangeR`を利用してFinger Treeを定義する。また、Finger Treeに対する操作として、つぎのものを定義する。

* 左への要素の追加
* 左からの要素の取り出し
* 右への要素の追加
* 右からの要素の取り出し
* 結合

### データ型`FingerTree`

データ型`FingerTree`を定義する。まずは、モジュール`Data.FingerTree`を用意する。

```haskell:src/Data/FingerTree.hs
{-# LANGUAGE ScopedTypeVariables, InstanceSigs #-}
{-# LANGUAGE DataKinds, TypeOperators #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses, FlexibleContexts, FlexibleInstances,
        UndecidableInstances #-}
{-# OPTIONS_GHC -Wall -fno-warn-tabs -fplugin=Plugin.TypeCheck.Nat.Simple #-}

module Data.FingerTree where

import GHC.TypeNats

import Data.List.Range
```

データ型`FingerTree`を定義する。

```haskell:src/Data/FingerTree.hs
data FingerTree a
        = Empty
        | Single a
        | Deep (DigitL a) (FingerTree (Node a)) (DigitR a)
        deriving Show

type Node = RangeL 2 3
type DigitL = RangeL 1 4
type DigitR = RangeR 1 4
```
`FingerTree a`型の値は空(`Empty`)か要素ひとつだけ(`Single _`)か、あるいは値構築子`Deep`による再帰的な値である。再帰的な値では、左右に1から4個のa型の値があり、a型の値が2個から3個でできた`Node a`型の値を要素とするFinger Treeになっている。型`Node`、`DigitL`、`DigitR`はそれぞれ、つぎのようになっている。

* `Node a`: 要素が2個か3個である左リスト
* `DigitL a`: 要素が1個から4個ある左リスト
* `DigitR a`: 要素が1個から4個ある右リスト
 
### 型クラス`Foldable`のインスタンスにする

型クラス`Foldable`のインスタンスにする。まずは、補助的な関数を定義する。

```src/Data/FingerTree.hs
reducer :: Foldable t => (a -> b -> b) -> t a -> b -> b
reducer = flip . foldr

reducel :: Foldable t => (b -> a -> b) -> b -> t a -> b
reducel = foldl
```

関数`reducer`と`reducel`は、それぞれ`foldr`、`foldl`とだいたいおなじだが、意味合いがちがう。つぎのように書くと、関数`reducer`、`reducel`が演算子の引数のひとつを`a`型から`t a`型に置き換える働きを持つことがわかる。

```haskell
reducer :: (a -> b -> b) -> (t a -> b -> b)
reducel :: (b -> a -> b) -> (b -> t a -> b)
```

型`FingerTree`を型クラス`Foldable`のインスタンスにする。

```haskell:src/Data/FingerTree.hs
instance Foldable FingerTree where
        foldr :: forall a b . (a -> b -> b) -> b -> FingerTree a -> b
        foldr _ z Empty = z
        foldr (-<) z (Single x) = x -< z
        foldr (-<) z (Deep pr m sf) = pr -<. (m -<.. (sf -<. z))
                where
                (-<.) :: forall t . Foldable t => t a -> b -> b
                (-<.) = reducer (-<)
                (-<..) :: forall t t' .
                        (Foldable t, Foldable t') => t (t' a) -> b -> b
                (-<..) = reducer (-<.)
```

型`DigitL`も`Node`も`DigitR`も、なかみは`RangeL n m`なので、型クラス`Foldable`のインスタンスだ。なので、関数`foldr`の第1引数である`(-<)`を`reducer`で持ち上げた`(-<.)`や、さらにそれを持ち上げた`(-<..)`で`pr -<. (m -<.. (sf -<. z))`のように書くことができる。それぞれの演算子の型は順に、つぎのようになっている。

```haskell
(-<.) :: DigitL a -> b -> b
(-<..) :: FingerTree (Node a) -> b -> b
(-<.) :: DigitR a -> b -> b
```

単純なFingerTreeを手書きして、試してみよう。

```
% stack ghci --ghc-options -fobject-code
> :module Data.FingerTree Data.List.Range
> sum $ Deep (1 :. 2 :.. NilL) Empty (NilR :+ 3)
6
```

### 左からの要素の追加

左から要素を追加する関数を定義する。考えかたとしては、左側の`DigitL`型のリストに空きがあれば、そこに追加する。リストがいっぱいである、つまり4個の要素がすでにはいっている場合には、追加する1個と合わせて5個の要素を、2個と3個にわけて、前者は`DigitL`型のリストとして左に置き、後者は`Node`型のリストにして、まんなかの`FingerTree (Node a)`に再帰的に追加する。

左側の`DigitL`型のリストに左から値を追加する演算子`(<||)`を定義する。

```haskell:src/Data/FingerTree.hs
infixr 5 <||

(<||) :: a -> DigitL a -> Either (DigitL a) (DigitL a, Node a)
a <|| b :. NilL = Left $ a :. b :.. NilL
a <|| b :. c :.. NilL = Left $ a :. b :.. c :.. NilL
a <|| b :. c :.. d :.. NilL = Left $ a :. b :.. c :.. d :.. NilL
a <|| b :. c :.. d :.. e :.. NilL =
        Right (a :. b :.. NilL, c :. d :. e :.. NilL)
_ <|| _ = error "never occur"
```

もとのリストの要素数が1から3個のときは、ひとつ追加したリストを`Left`値としてかえす。もとのリストの要素数が4個のときには`Right値`として、2個と3個にわけて、それぞれ`DigitL a`型のリストと`Node a`型のリストにいれてかえす。これを使って、`FingerTree a`型の値に対して左から要素を追加する演算子`(<|)`を定義する。

```haskell:src/Data/FingerTree.hs
infixr 5 <|

(<|) :: a -> FingerTree a -> FingerTree a
a <| Empty = Single a
a <| Single b = Deep (a :. NilL) Empty (NilR :+ b)
a <| Deep pr m sf = case a <|| pr of
        Left pr' -> Deep pr' m sf
        Right (pr', n3) -> Deep pr' (n3 <| m) sf
```

もとの`FingerTree`型の値が`Empty`や`Single`だったときと、`Deep pr m sf`の`pr`の要素数が3個以下だったときの定義はかんたんだ。`pr`の要素数が4個だったときは、終わりの3個が`Node`型の値にまとめられて、まんなかの`FingerTree (Node a)`型の値に対して再帰的に追加されている。

リストなど`Foldable`クラスのインスタンスである並びのすべての要素を順に左から追加できると便利なので、そのような演算子`(<|.)`も定義しておく。

```haskell:src/Data/FingerTree.hs
infixr 5 <|.

(<|.) :: Foldable t => t a -> FingerTree a -> FingerTree a
(<|.) = reducer (<|)
```

空の値に対して左から値を追加していくことで、`FingerTree`型の値を構成する関数`mkFingerTree`を定義しておく。

```haskell:src/Data/FingerTree.hs
mkFingerTree :: Foldable t => t a -> FingerTree a
mkFingerTree = (<|. Empty)
```

試してみよう。

```
% stack ghci --ghc-options -fobject-code
> :m Data.FingerTree
> mkFingerTree [1 .. 10]
...
> mkFingerTree "Hello, world!"
...
```

### 左からの要素の取り出し

左から要素を取り出す関数`uncons`を定義する。

```haskell:src/Data/FingerTree.hs
uncons :: FingerTree a -> Maybe (a, Fingertree a)
uncons Empty = Nothing
uncons (Single x) = Just (x, Empty)
uncons (Deep (a :. pr') m sf) = Just (a, deepL pr' m sf)

deepL :: RangeL 0 3 a -> FingerTree (Node a) -> DigitR a -> FingerTree a
deepL NilL m sf = case uncons m of
        Nothing -> mkFingerTree sf
        Just (n, m') -> Deep (nodeToDigitL n) m' sf
deepL (a :.. pr) m sf = Deep (loosenL $ a :. pr) m sf
deepL _ _ _ = error "never occur"

nodeToDigitL :: Node a -> DigitL a
nodeToDigitL = loosenL
```

関数`uncons`と`deepL`とは相互再帰の関係になっている。関数`uncons`は左側のリストからひとつ取り出して、取り出した結果として0個から3個のリストになってしまった左側のリストと、まんなかの`FingerTree`型の値と、右側のリストとから関数`deepL`で新しい`FingerTree`型の値を構成する。

関数`deepL`は1個足りない左側のリスト(`RangeL 0 3 a`)と、まんなかの部分と右側の部分から新しい`FingerTree`型の値を構成する関数だ。左側のリストにひとつでも値があれば、関数`loosenL`を使って左側のリスト(`RangeL 1 4 a`)を作ることはかんたんだ。左側のリストが`NilL`のときだけが問題だ。このときには、まんなかの`FingerTree (Node a)`型の値から関数`uncons`で、ひとつ取り出してやり、それを関数`nodeToDigitL`で`DigitL a`型の値に変換して、それを左側のリストにする。試してみよう。

```
% stack ghci --ghc-options -fobject-code
> mkFingerTree "Hello, world!"
> uncons it
Just ('H', Deep ...)
```

### 右への要素の追加

右への要素の追加は、左への要素の追加とだいたいおなじだ。

```haskell:src/Data/FingerTree.hs
infixl 5 ||>, |>, |>.

(||>) :: DigitR a -> a -> Either (DigitR a) (Node a, DigitR a)
NilR :+ a ||> b = Left $ NilR :++ a :+ b
NIlR :++ a :+ b ||> c = Left $ NilR :++ a :++ b :+ c
NilR :++ a :++ b :+ c ||> d = Left $ NilR :++ a :++ b :++ c :+ d
NilR :++ a :++ b :++ c :+ d ||> e =
        Right (a :. b :. c :.. NilL, NilR :++ d :+ e)
_ ||> _ = error "never occur"

(|>) :: FingerTree a -> a -> FingerTree a
Empty |> a = Single a
Single a |> b = Deep (a :. NilL) Empty (NilR :+ b)
Deep pr m sf |> a = case sf ||> a of
        Left sf' -> Deep pr m sf'
        Right (n3, sf') -> Deep pr (m |> n3) sf'

(|>.) :: Foldable t => FingerTree a -> t a -> FingerTree a
(|>.) = reducel (|>)
```

向きがちがうだけで、だいたいおなじ。試してみよう。

```
% stack ghci
> t = mkFingerTree "Hello, "
> t |>. "world!"
Deep ...
> :module + Data.Foldable
> toList it
"Hello, world!"
```

### 右からの要素の取り出し

左からの要素の取り出しと、だいたいおなじだ。

```haskell:src/Data/FingerTree.hs
unsnoc :: FingerTree a -> Maybe (FingerTree a, a)
unsnoc Empty = Nothing
unsnoc (Single x) = Just (Empty, x)
unsnoc (Deep pr m (sf' :+ a)) = Just (deepR pr m sf', a)

deepR :: DigitL a -> FingerTree (Node a) -> RangeR 0 3 a -> FingerTree a
deepR pr m NilR = case unsnoc m of
        Nothing -> mkFingerTree pr
        Just (m', a) -> Deep pr m' (nodeToDigitR a)
deepR pr m (sf :++ a) = Deep pr m (loosenR $ sf :+ a)
deepR _ _ _ = error "never occur"

nodeToDigitR :: Node a -> DigitR a
nodeToDigitR = loosenR . leftToRight
```

`Node`が左リストで`DigitR`が右リストなので、関数`nodeToDigitR`には`leftToRight`が必要。それ以外は、だいたいおなじ。試してみよう。

```
% stack ghci
> t = mkFingerTree "Hello, world!"
> unsnoc t
Just (Deep ..., '!')
```

### 結合

`FingerTree`型の値どうしの結合を定義する。言ってみれば、ここがクライマックスと言えるかもしれない。「3個から12個までの`a`型の値のリストを1個から4個までの『2個か3個の`a`型の値のリスト』のリストにわける」という処理を書くことになる。`FingerTree`型の値どうしの結合は、その途中に「`FingerTree a`型の値と、`a`型の値のリストと`FingerTree a`型の値」の3者の結合という処理が出てくる。その中間に出てくるリストの持つ要素の個数は3個から12個である。また、その3個から12個の`a`型の値を`Node a`型の値のリスト1個から4個に変換する処理も出てくる。

このようにアルゴリズムの特性として、取り得る値の範囲が型で表現できることになる。

`FingerTree`型の値どうしを結合する関数`(><)`を定義するのだが、そのためにあいだの仲介するリストを含めて3者を結合する関数`app3`を定義する。その関数`app3`の定義の途中に使われる。つぎのような型の関数を定義したい。

```haskell
f :: RangeL 3 12 a -> RangeL 1 4 (Node a)
```

これを定義するには順につぎのような関数を定義していけばいい。

```haskell
g0 :: RangeL 3 3 a -> RangeL 1 1 (Node a)
g1 :: RangeL 3 6 a -> RangeL 1 2 (Node a)
g2 :: RangeL 3 9 a -> RangeL 1 3 (Node a)
g3 :: RangeL 3 12 a -> RangeL 1 4 (Node a)
```

つまり、`RangeL 3 3 a -> RangeL 1 1 (Node a)`を定義したうえで、`RangeL 3 (m - 3) a -> RangeL 1 (w - 1) a`を利用して`RangeL 3 m a -> RangeL 1 w a`が定義できればいいということだ。

```haskell:src/Data/FingerTree.hs
class Nodes m w where nodes :: RangeL 3 m a -> RangeL 1 w (Node a)

instance Nodes 3 1 where nodes = (:. NilL) . loosenL

instance {-# OVERLAPPABLE #-} (2 <= w, Nodes (m - 3) (w - 1)) => Nodes m w where
        nodes :: forall a . RangeL 3 m a -> RangeL 1 w (Node a)
        nodes (a :. b :. c :. NilL) = (a :. b :. c :.. NilL) :. NIlL
        nodes (a :. b :. c :. d :.. NilL) =
                (a :. b :. NilL) :. (c :. d :. NilL) :.. NilL
        nodes (a :. b :. c :. d :.. e :.. NilL) =
                (a :. b :. c :.. NilL) :. (d :. e :. NilL) :.. NilL
        nodes (a :. b :. c :. d :.. e :.. f :.. xs) =
               (a :. b :. c :.. NilL) .:..
                        (nodes (d :. e :. f :. xs :: RangeL 3 (m - 3) a)
                                :: RangeL 1 (w - 1) (Node a))
        nodes _ = error "never occur"
```

`m = 3`, `w = 1`のときは、引数の型は`RangeL 3 3 a`になるので、これを関数`loosenL`で`RangeL 2 3 a`にする。これは`Node a`とおなじなので、これひとつだけのリストを作ればいい。`(:. NilL) . loosenL`はそういうことだ。ふたつめのインスタンス宣言ではより一般的な`m`, `w`について定義している。もとのリストの要素の数が3個のときには、`Node a`を1個だけ含むリストを返せばいい。4個のときには「2個の`a`型の値を含む`Node`型の値」を2個返す。5個のときには「3個の`a`型の値を含む`Node`型の値と2個の`a`型の値を含む`Node`型の値」をかえす。6個以上のときには「最初の3個で`Node a`型の値を作り、残りについては再帰的に関数nodesを適用すれば」いい。試してみよう。

```
% stack ghci --ghc-options -fobject-code
> :set -XDataKinds
> t = 1 :. 2 :. 3 :. 4 :.. 5 :.. 6 :.. 7 :.. 8 :.. 9 :.. 10 :.. NilL :: RangeL 3 12 Integer
> nodes t :: RangeL 1 4 (Data.FingerTree.Node Integer)
(1 :. (2 :. (3 :.. NilL))) :. ((4 :. (5 :. (6 :.. NilL))) :.. ((7 :. (8 :. NilL)) :.. ((9 :. (10 :. NilL)) :.. NilL)))
```

10個の整数からなるリストが4個の`Node Integer`型の値にわけられた。これを使って関数`app3`を定義する。

```haskell:src/Data/FingerTree.hs
app3 :: forall a . FingerTree a -> RangeL 1 4 a -> FingerTree a -> FingerTree a
app3 Empty m xs = m <|. xs
app3 xs m Empty = xs |>. m
app3 (Single x) m xs = x <| m <|. xs
app3 xs m (Single x) = xs |>. m |> x
app3 (Deep pr1 m1 sf1) m (Deep pr2 m2 sf2) =
        Deep pr1 (app3 m1 (nodes $ sf1 ++.. m ++. pr2) m2) sf2
```
うえの4行はかんたんだ。5行目は再帰的な定義になっている。新しいFinger Treeの左側と右側のリストは、それぞれ左辺のFinger Treeの左側のリストと右辺のFinger Treeの右側のリストをそのまま使っている。まんなかの部分で再帰的に関数`app3`を呼び出して`m1`と`m2`とそれを仲介するリストとを結合している。仲介するリストは左辺の右側のリストと、もともとの仲介するリストと、右辺の左側のリストを結合したリストを`Node a`型のリストに変換している。

Finger Treeを結合する演算子`(><)`は関数`app3`の第2引数に値ひとつかならるリストをいれるために右辺のFinger Treeの先頭の値を取り出している。

```haskell:src/Data/FingerTree.hs
(><) :: FingerTree a -> FingerTree a -> FingerTree a
l >< r = case uncons r of Nothing -> l; Just (x, r') -> app3 l (x :. NilL) r'
```

試してみよう。

```
% stack ghci
> l = mkFingerTree "Hello, "
> r = mkfingerTree "world!"
> l >< r
Deep ...
> :module + Data.Foldable
> toList it
"Hello, world!"
```

まとめ
-----

型レベルで要素の個数の範囲を指定できるリスト(`RangeL`, `RangeR`)を使ってFinger Treeを実装した。`RangeL`や`RangeR`型の値に対する演算には、GHCのデフォルトの型チェックの機構では型が解決できないものがあったので、型チェックプラグインを定義した。型チェックプラグインに使うモジュールの関数を試すためにパーサが必要だったのでPackrat Parserを書いた。

`RangeL`や`RangeR`型のリストを使って、Finger Treeを実装したが、アルゴリズムの特徴として、リストの要素の個数の範囲が決まっているが、それが型レベルで表現できるのが気持ちいい。実行効率はO記法的には問題ないはずだ。