More than 3 years have passed since last update.

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

Last updated at 2020-12-22Posted at 2020-12-17

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

はじめにの前に

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

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

なんか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

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

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

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

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に左から値を追加する関数を定義する。

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

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のインスタンスにしてみよう。

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型のリストの先頭にオプショナルな要素を追加する演算子(.:..)を定義する。この演算子の型はつぎのようになる。

(.:..) :: 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のときとちがって、もとになる型クラスがないので、ここで定義する。

src/Data/List/Range/RangeL.hs

infixr 5 .:..

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

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

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

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フィールドの値の型は、つぎのような型である。

[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

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を、つぎのように書き換える。

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

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を導入する。

src/Data/Derivation/Expression.hs

import Prelude hiding ((<>))

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

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

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

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
...

src/Plugin/TypeCheck/Nat/Simple.hs

import Control.Monad.Trans.Except

import Plugin.TypeCheck.Nat.Simple.Decode

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を書き換える。つぎの部分を

src/Plugin/TypeCheck/Nat/Simple.hs

        tcPluginTree "Given: " $ ppr gs
        tcPluginTree "Derived: " $ ppr ds
        tcPluginTree "Wanted: " $ ppr ws

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

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を定義していく。

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

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

src/Plugin/TypeCheck/Nat/Simple/Decode.hs

import GhcPlugins (Var, promotedFalseDataCon, promotedTrueDataCon)
import TyCoRep
import Control.Monad.Trans.Except
import Data.Derivation.Expression

関数exVarを定義する。

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を導入する。

src/Plugin/TypeCheck/Nat/Simple/Decode.hs

import TcTypeNats

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型の値に変換する関数を定義する。

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を導入する。

src/Plugin/TypeCheck/Nat/Simple/Decode.hs

import Control.Applicative ((<|>))

関数decodeを定義する。

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を導入する。

src/Plugin/TypeCheck/Nat/Simple.hs

import Control.Monad

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

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'

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

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

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

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

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

p :: StateT s Maybe a

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

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

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

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'を読み込むために「指定された一文字を読み込む関数」を定義する。

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を書いてみよう。まずはモジュールを用意する。

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はおなじように定義する。

src/TryParse/NoExponential.hs

data Expression = One | Expression :+ Expression deriving Show

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

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型の値を定義する。

/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を文字列の代わりとして、「式」と「項」を読み込むパーサを定義する。

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を使うことで、新たに値を計算するのではなく、メモ用の構造から値を取り出すようにした。

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

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のところは、つぎのような式とおなじことだ。

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

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

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

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

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を導入する。

src/Data/Parse.hs

import Control.Applicative

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の公開リストに演算子(>>!)を追加する。

src/Data/Parse.hs

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

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

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

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

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

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

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 . (==)

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

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のうち定義できる部分だけを定義する。

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

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

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

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

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

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の定義してなかった部分をうめる。

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を定義する。

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を用意する。

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を利用する。

src/Data/Derivation/Constraint.hs

type Polynomial v = Map (Maybe v) Integer

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

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

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以上であるという形で制約を保存するようにする。

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種の関係について、制約型の値を構成できるようにする。

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に変換用の関数を定義する。まずは、いくつかのモジュールを導入する。

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を定義する。

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ということになる。このような対応づけをする関数を定義する。まずは、必要なモジュールを導入する。

src/Data/Derivation/Expression.hs

import Control.Arrow (first, second)
import Data.Maybe
import Data.List (find)

関数mkVarBoolを定義する。

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型の値に変換する関数を定義する。

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モナドから中身を取り出す。

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を定義する。

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を定義する。

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を定義する。

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を用意する。

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を定義する。

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を定義する。

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型から変数を消去する関数を定義する。

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が導出できるかどうかチェックする関数を定義する。

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

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

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

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)をそうでなければエラー値を返す関数を定義する。

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の最終行を書き換える。

src/Plugin/TypeCheck/Nat/Simple.hs

        pure $ TcPluginOk (rights $ runExcept . result gs <$> ws) []

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

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を追加しよう。

src/Data/List/Range/RangeL.hs

{-# OPTIONS_GHC -Wall -fno-warn-tabs -fplugin=Plugin.TypeCheck.Nat.Simple #-}

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

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を定義する。

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の場合を定義する。

src/Data/List/Range/RangeL.hs

instance LoosenLMin 0 m 0 where
        loosenLMin NilL = NilL
        loosenLMin xa@(_ :.._) = xa
        loosenLMin _ = error "never occur"

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

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ではない場合だ。

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)))))

最大の個数を増やす

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

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である場合から定義していこう。

src/Data/List/Range/RangeL.hs

instance LoosenLMax 0 0 m where
        loosenLMax NilL = NilL
        loosenLMax _ = error "never occur"

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

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でない場合を定義する。

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とを組み合わせれば最小値、最大値をともにゆるくする関数が定義できる。

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)))))

リストの結合

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

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を用意する。

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を定義する。

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`のインスタンスにする

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型の値にオプショナルな要素を追加する演算子(.:++)を定義しよう。

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を定義する。

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を定義する。

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を定義する。

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をわたせばいい。まずはモジュールを用意する。

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

型クラスを用意する。

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

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

src/Data/List/Range.hs

instance LeftToRight 0 m 0 0 where n ++.+ _ = n

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

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

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の場合を定義する。

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だった場合を定義しよう。

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を定義する。

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) ++.+)

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

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

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を定義しておこう。

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から必要な型や関数を公開する。

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を用意する。

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を定義する。

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型に置き換える働きを持つことがわかる。

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

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

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))のように書くことができる。それぞれの演算子の型は順に、つぎのようになっている。

(-<.) :: 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型のリストに左から値を追加する演算子(<||)を定義する。

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型の値に対して左から要素を追加する演算子(<|)を定義する。

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

src/Data/FingerTree.hs

infixr 5 <|.

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

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

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を定義する。

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 ...)

右への要素の追加

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

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!"

右からの要素の取り出し

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

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の定義の途中に使われる。つぎのような型の関数を定義したい。

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

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

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が定義できればいいということだ。

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を定義する。

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の先頭の値を取り出している。

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記法的には問題ないはずだ。

You get articles that match your needs
You can efficiently read back useful information
You can use dark theme

What you can do with signing up

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

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

はじめにの前に

はじめに

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

Finger Tree

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

型チェックプラグイン

Packrat parser

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

RangeLの実装

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

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

Nat類の式を表すデータ型

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

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

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

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

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

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

多項式を表す型

制約を表す型

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

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

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

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

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

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

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

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

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

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

最小の個数を減らす

最大の個数を増やす

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

リストの結合

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

データ型RangeR

型クラスFoldableのインスタンスにする

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

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

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

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

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

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

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

データ型FingerTree

型クラスFoldableのインスタンスにする

左からの要素の追加

左からの要素の取り出し

右への要素の追加

右からの要素の取り出し

結合

まとめ

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

`RangeL`の実装

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

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

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

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

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

データ型`RangeR`

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

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

データ型`FingerTree`

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