Paraisoが生成するC++コードのAPI
今回はParaisoが生成するコードの使い方を見ていきます。HelloWorldフォルダでGenerator.hsを実行すると、distというフォルダが作られてその下にC++のヘッダやソースが生成されているはずです。まずはヘッダを見てください。
class TableMaker{ private: std::vector<int> om_s0_table; private: int om_s1_total; private: std::vector<int> om_m0_5; public: TableMaker () : om_s0_table(om_memory_size()), om_m0_5(om_memory_size()) { }
このように、静的変数のための記憶領域やコンストラクタが定義されています。Paraisoの生成するクラスは、この他にもいくつかのアクセッサ関数を定義します。まずは、OMのサイズを取得するための関数がこちらです。全領域のサイズおよび、各次元ごとのサイズを取得できます。（これサイズがint型なのはまずいな・・・）
public: int om_size () { return 200; } public: int om_size_0 () { return 10; } public: int om_size_1 () { return 20; }
Paraisoが副次的に生成する関数の名前はすべてom_から始まるようになっています。ユーザーは静的変数やカーネルに、すべて異なり、かつどれもom_から始まらないような名前をつけてください。そうすればコード生成時に名前が衝突することはありません。
今のHelloWorldカーネルにはありませんが、配列変数で、近傍の値をとってくるshift命令を含むカーネルをコンパイルすると、Paraisoは通信のための余白領域を確保し、[0..size-1]までの領域が無事に計算できるようにします。この場合、実際に確保されたメモリの大きさはom_size()等が返す値よりも大きくなります。このメモリサイズを取得できる関数群がom_memory_size()などです。
public: int om_memory_size () { return 200; } public: int om_memory_size_0 () { return 10; } public: int om_memory_size_1 () { return 20; }
そしてこれが余白を取得する関数群です。
public: int om_lower_margin_0 () { return 0; } public: int om_lower_margin_1 () { return 0; } public: int om_upper_margin_0 () { return 0; } public: int om_upper_margin_1 () { return 0; }
Array変数に対しては要素へのアクセッサが、Scalar変数に対しては単なるアクセッサが定義されます。
public: int & table (int i0, int i1) { return (om_s0_table)[((om_lower_margin_0()) + (i0)) + ((om_memory_size_0()) * ((om_lower_margin_1()) + (i1)))]; } public: int & total () { return om_s1_total; }
また、配列の生データへのアクセッサも提供されますが、「生」データが具体的にどんなフォーマットなのかは実装の詳細に依存します。
public: std::vector<int> & table () { return om_s0_table; }
最後に、OMの定義で与えたカーネルに対応するメソッドが生成されます。
public: void create () ; };
はじめてのParaisoプログラミング
Paraisoは、一様メッシュ上での偏微分方程式の陽解法という分野に特化し、その分野の計算を、直胞機械(OrthotopeMachineの訳語、今決めた)と呼ばれる仮想機械のプログラムとして表します。直胞機械は、配列変数とその操作を表現する仮想機械であり、解きたい問題の内包する並列性をなるべく生かすように設計されています。たとえば、配列変数の要素を格納する順序や、アクセスする順序は自由。命令どうしの依存関係もはじめから明確で、依存性のない命令を実行する順序も、同時に実行することも自由です。Paraisoは、この直胞機械のプログラムを記述し、それを既存の言語のプログラムに翻訳し、さらに自動チューニングを行うための様々なメカニズムを備えたフレームワークです。より詳しい用語の解説などはParaisoの論文を見てください。
しかし、Paraisoにコードを生成させるためにユーザーがすべきことを、具体的に一言でいうなら、「OM型の値を作り、コードジェネレータに渡すこと」となります。
ハローワールドの中身
前回掲載したサンプルexamples/HelloWorld/Generator.hsには、Paraisoにコードを生成させるための全てが記されています。順にみていきましょう。
最初の十数行は#include みたいなもんで、必要なモジュールをインクルードしています。
#!/usr/bin/env runhaskell {-# LANGUAGE NoImplicitPrelude, OverloadedStrings #-} {-# OPTIONS -Wall #-} import Data.Tensor.TypeLevel import qualified Data.Text.IO as T import Language.Paraiso.Annotation (Annotation) import Language.Paraiso.Generator (generateIO) import qualified Language.Paraiso.Generator.Native as Native import Language.Paraiso.Name import Language.Paraiso.OM import Language.Paraiso.OM.Builder import Language.Paraiso.OM.DynValue (f2d, DynValue) import Language.Paraiso.OM.Value (StaticValue(..)) import Language.Paraiso.OM.PrettyPrint (prettyPrintA1) import Language.Paraiso.OM.Realm import qualified Language.Paraiso.OM.Reduce as Reduce import Language.Paraiso.Optimization import NumericPrelude import System.Process (system)
まずはmainから見ていきましょう。一行目は"output"というフォルダを作っています。二行目では、myOMという名の直胞機械のデータフロー・グラフを出力しています。これは参考のために出力しているのであって、コード生成に必須の過程ではありません。三行目では、myOMの定義とmySetupというコード生成時の設定を渡してC++のコードを生成しています。
-- the main program main :: IO () main = do _ <- system "mkdir -p output" T.writeFile "output/OM.txt" $ prettyPrintA1 $ myOM _ <- generateIO mySetup myOM return ()
直胞機械を定義する時には使わないが、コード生成時にはじめて必要になる情報はLanguage.Paraiso.Generator.NativeモジュールにあるSetup型でまとめて指定します。ここでは具体的な計算のサイズや、ライブラリを生成するフォルダを指定しています。コード生成対象の言語はデフォルトではC++です。
-- the code generation setup mySetup :: Native.Setup Vec2 Int mySetup = (Native.defaultSetup $ Vec :~ 10 :~ 20) { Native.directory = "./dist/" }
次はいよいよmyOMの定義です。直胞機械を定義するには、名前(tableMaker)、マシン全体の注釈、静的変数のリスト、カーネルのリストの4つをmakeOM関数に渡します。
-- the orthotope machine to be generated myOM :: OM Vec2 Int Annotation myOM = optimize O3 $ makeOM (mkName "TableMaker") [] myVars myKernels
myOMには、九九の表を保持するためのtableと、その合計を計算するためのtotalという2つの変数があります。2つの変数のRealmは、それぞれArrayとScalarです。Array変数は解きたい問題の解像度とおなじサイズをもつ配列変数で、Scalar変数は普通に1つしかない値です。それぞれの変数はNameも持っています。
-- the variables we use table :: Named (StaticValue TArray Int) table = "table" `isNameOf` StaticValue TArray undefined total :: Named (StaticValue TScalar Int) total = "total" `isNameOf` StaticValue TScalar undefined myVars :: [Named DynValue] myVars = [f2d table, f2d total]
Paraisoでは、Language.Paraiso.Nameモジュールで定義されているName型を識別子の名前として使います。これは、ただの文字列と区別するために、Data.Textモジュールの提供するマルチバイト文字列型Textをnewtypeしたものです。
次にカーネルの定義です。OMのカーネルとは、一度に実行される計算のかたまりです。myOMにはcreateという名前のカーネルがひとつだけあります。
-- the only kernel our OM has myKernels :: [Named (Builder Vec2 Int Annotation ())] myKernels = ["create" `isNameOf` createBuilder]
カーネルを作るにはBuilder Monadを使います。ここでは、x軸とy軸の添字を読み込んでその積を計算するカーネルを作っています。ついでに九九の表の総計も求めてみましょう。
-- the kernel builder monad createBuilder :: Builder Vec2 Int Annotation () createBuilder = do x <- bind $ loadIndex (Axis 0) y <- bind $ loadIndex (Axis 1) z <- bind $ x*y store table z store total $ reduce Reduce.Sum z
Paraisoで始める数値流体力学
Paraisoの論文がAcceptしました。確かにこれで、偏微分方程式の解法を記述する数式を処理し、並列仮想マシンを経てCPU/GPU向けのコードを生成し、さらに遺伝的アルゴリズムで自動チューンするまでを一つのシステムとして実証するという一歩を進めることができました。が、現在のParaisoは生後まもない言語で、いろいろとアドホックな箇所が残っています。
インターフェイスも、生成されるコードの速度もまだまだ洗練の余地があり、たくさんのドキュメントを整備していくことで、おそらく誰にも（私にも！）使えない言語という状態を脱してゆきたいと思います。
そのために、数値流体力学の入門記事をParaisoで書いてみようと思います。無論数値流体力学のずっと良い教科書は沢山ありますがParaisoで書いてあるのは初めてなんじゃないかな！インターフェイスというのはみんなで作るものなので、どうかコメントください。
この記事を試すには、ひとまずGitとHaskell Platformが必要です。
また、GPU版を試すにはCUDAが必要になるでしょう。
新しいブランチ
論文の時点からの改良をいれたdonutブランチで、Paraiso 0.3.0.0を作ってゆきます。詳しくはHaddockやParaisoのサイトを参照してください。donutブランチをゲットするにはバージョン管理ソフトウェアgitをインストールした上で次のように入力します。
$ git clone -b donut https://github.com/nushio3/Paraiso.git Cloning into 'Paraiso'... remote: Counting objects: 4743, done. remote: Compressing objects: 100% (1815/1815), done. remote: Total 4743 (delta 2885), reused 4637 (delta 2779) Receiving objects: 100% (4743/4743), 2.65 MiB | 411 KiB/s, done. Resolving deltas: 100% (2885/2885), done. $ cd Paraiso/ $ git branch * donut $
論文執筆時点とくらべ、すでに
- 不評だったLocalとGlobalという用語を、普通にArrayとScalarと呼ぶことにした
- Paraisoが生成するクラスのメソッド名を変更
などの違いが生まれ始めているのでご注意下さい＆手間かけてすいません。とまれ、ここで以下のように唱えれば、Paraisoがインストールされるはずです。
Paraiso$ cabal install (...a few minutes...) Registering Paraiso-0.3.0.0... Paraiso$
ここに最初のサンプルがあります。
Paraiso$ cd examples/HelloWorld/
HelloWorld$ cat Generator.hs
#!/usr/bin/env runhaskell {-# LANGUAGE NoImplicitPrelude, OverloadedStrings #-} {-# OPTIONS -Wall #-} import Data.Dynamic import Data.Tensor.TypeLevel import qualified Data.Text.IO as T import Language.Paraiso.Annotation (Annotation) import Language.Paraiso.Generator (generateIO) import qualified Language.Paraiso.Generator.Native as Native import Language.Paraiso.Name import Language.Paraiso.OM import Language.Paraiso.OM.Builder import Language.Paraiso.OM.DynValue as DVal import Language.Paraiso.OM.PrettyPrint (prettyPrintA1) import Language.Paraiso.OM.Realm import qualified Language.Paraiso.OM.Reduce as Reduce import Language.Paraiso.Optimization import NumericPrelude import System.Process (system) -- the names we use table, total, create, tableMaker :: Name table = mkName "table" total = mkName "total" create = mkName "create" tableMaker = mkName "TableMaker" main :: IO () main = do _ <- system "mkdir -p output" T.writeFile "output/OM.txt" $ prettyPrintA1 $ myOM _ <- generateIO mySetup myOM return () mySetup :: Native.Setup Vec2 Int mySetup = (Native.defaultSetup $ Vec :~ 10 :~ 20) { Native.directory = "./dist/" } myOM :: OM Vec2 Int Annotation myOM = optimize O3 $ makeOM tableMaker [] myVars myKernels myVars :: [Named DynValue] myVars = [Named table $ DynValue Array (typeOf (undefined::Int)), Named total $ DynValue Scalar (typeOf (undefined::Int))] myKernels :: [Named (Builder Vec2 Int Annotation ())] myKernels = [Named create createBuilder] createBuilder :: Builder Vec2 Int Annotation () createBuilder = do x <- bind $ loadIndex (undefined::Int) (Axis 0) y <- bind $ loadIndex (undefined::Int) (Axis 1) z <- bind $ x*y store table z store total $ reduce Reduce.Sum z
これは、実行すると九九の表を表示してくれるサンプルです。
HelloWorld$ make runhaskell Generator.hs g++ main.cpp dist/TableMaker.cpp -o main.out HelloWorld$ ./main.out 0 0 0 0 0 0 0 0 0 0 0 1 2 3 4 5 6 7 8 9 0 2 4 6 8 10 12 14 16 18 0 3 6 9 12 15 18 21 24 27 0 4 8 12 16 20 24 28 32 36 0 5 10 15 20 25 30 35 40 45 0 6 12 18 24 30 36 42 48 54 0 7 14 21 28 35 42 49 56 63 0 8 16 24 32 40 48 56 64 72 0 9 18 27 36 45 54 63 72 81 0 10 20 30 40 50 60 70 80 90 0 11 22 33 44 55 66 77 88 99 0 12 24 36 48 60 72 84 96 108 0 13 26 39 52 65 78 91 104 117 0 14 28 42 56 70 84 98 112 126 0 15 30 45 60 75 90 105 120 135 0 16 32 48 64 80 96 112 128 144 0 17 34 51 68 85 102 119 136 153 0 18 36 54 72 90 108 126 144 162 0 19 38 57 76 95 114 133 152 171 total:8550 HelloWorld$
Scrap Your Boilerplate ことはじめ2
昨日のやつのモナド版を作ってみます。
recMapM :: forall a b m. (Data a, Data b, Monad m) => (b -> m b) -> a -> m a recMapM f x = do let recurse = gmapM (recMapM f) x case cast x of Nothing -> recurse Just bx -> do z <- f bx case cast z of Nothing -> recurse Just az -> return az
途中Maybe (m (Maybe b))という型になるため、Maybeを手で扱う必要が出てくる必要があっていやーんな感じです。何とかならないものでしょうか。二つのMaybeの文脈は結合したいし、かといってmがMonadMaybeであることを要求したくはないわけで。
ともかくこれがあればモナド無双できます。倍精度実数の部分にちょっとだけ乱数を足すとか。
ghci> recMapM (\x -> getRandomR (x,(1.01::Double)*x)) a1 >>= print Abc (Bca (Cab (A "Happy") (B 4.215734581306111)) (Abc (B 5.627533165698871) (C 512))) (Cab (Abc (B 8.482016322000884) (C 208)) (Bca (C 2012) (A "New Year!")))
文字列パートを強調する方法をすべて列挙するとか。
ghci> mapM_ print $ recMapM (\str -> [str, "Very " ++ str, "Extremely " ++ str]) a1 Abc (Bca (Cab (A "Happy") (B 4.2)) (Abc (B 5.6) (C 512))) (Cab (Abc (B 8.4) (C 208)) (Bca (C 2012) (A "New Year!"))) Abc (Bca (Cab (A "Happy") (B 4.2)) (Abc (B 5.6) (C 512))) (Cab (Abc (B 8.4) (C 208)) (Bca (C 2012) (A "Very New Year!"))) Abc (Bca (Cab (A "Happy") (B 4.2)) (Abc (B 5.6) (C 512))) (Cab (Abc (B 8.4) (C 208)) (Bca (C 2012) (A "Extremely New Year!"))) Abc (Bca (Cab (A "Very Happy") (B 4.2)) (Abc (B 5.6) (C 512))) (Cab (Abc (B 8.4) (C 208)) (Bca (C 2012) (A "New Year!"))) Abc (Bca (Cab (A "Very Happy") (B 4.2)) (Abc (B 5.6) (C 512))) (Cab (Abc (B 8.4) (C 208)) (Bca (C 2012) (A "Very New Year!"))) Abc (Bca (Cab (A "Very Happy") (B 4.2)) (Abc (B 5.6) (C 512))) (Cab (Abc (B 8.4) (C 208)) (Bca (C 2012) (A "Extremely New Year!"))) Abc (Bca (Cab (A "Extremely Happy") (B 4.2)) (Abc (B 5.6) (C 512))) (Cab (Abc (B 8.4) (C 208)) (Bca (C 2012) (A "New Year!"))) Abc (Bca (Cab (A "Extremely Happy") (B 4.2)) (Abc (B 5.6) (C 512))) (Cab (Abc (B 8.4) (C 208)) (Bca (C 2012) (A "Very New Year!"))) Abc (Bca (Cab (A "Extremely Happy") (B 4.2)) (Abc (B 5.6) (C 512))) (Cab (Abc (B 8.4) (C 208)) (Bca (C 2012) (A "Extremely New Year!")))
Scrap Your Boilerplate ことはじめ
折角ですから、Haskellで新年の挨拶をしてみましょう。以下のコードをMain.hsといったファイル名で保存し、ghciから読み込んでみてください。
{-# LANGUAGE DeriveDataTypeable, RankNTypes#-} {-# OPTIONS -Wall #-} import Data.Data import Data.Maybe(maybeToList) import Data.Generics.Schemes data ABC = ABC Int Double String deriving (Eq, Show, Data, Typeable) data A = A String | Abc B C deriving (Eq, Show, Data, Typeable) data B = B Double | Bca C A deriving (Eq, Show, Data, Typeable) data C = C Int | Cab A B deriving (Eq, Show, Data, Typeable) abc1 :: ABC abc1 = ABC 2012 1.1 "Tatsu" a1 :: A a1 = Abc (Bca (Cab (A "Happy") (B 4.2)) (Abc (B 5.6) (C 512))) (Cab (Abc (B 8.4) (C 208)) (Bca (C 2012) (A "New Year!")))
上記のようなa1やabc1のようなデータ構造を作ってしまってから、中の文字列とかをいじりたくなったらどうすればいいのでしょう？私はこういう操作をするにはHaskellのソースを操ることが必要と思っていましたが、そんなことはなかったぜ！
Scrap Your Boilerplate
Data.Dataモジュールにあるgmapなんちゃらという名前の関数が使えるそうです。まずは、これに注目：
gmapQ :: (forall d. Data d => d -> u) -> a -> [u]
どうにかして、任意の型をとってu型を返す関数(forall d. Data d => d -> u)なんつう難しいものを作る必要があるそうです。と、とりあえず、const？
ghci> gmapQ (const "homu") abc1 ["homu","homu","homu"] ghci> gmapQ (const "homu") a1 ["homu","homu"]
オブジェクトの子要素がいくつあるか、みたいな情報が取れたようです。ドキュメントにしつこくimmediate subtermsとあるように、gmapなんちゃらたちは引数に与えられた値の直下の要素を処理します。いっぽう、a1やabc1にはもっと沢山の要素が詰まっています。
ghci> (gdepth abc1, gsize abc1) (7,14) ghci> (gdepth a1, gsize a1) (14,51) ghci> (gdepth "", gsize "") (1,1) ghci> (gdepth "a", gsize "a") (2,3) ghci> (gdepth "ab", gsize "ab") (3,5)
おもにStringがかさばってるようです。
さて、要素に対して有用な操作を施そうと思ったら、型が(forall d. Data d => d)のままでは困ります。これはcastの出番です！
cast :: (Typeable a, Typeable b) => a -> Maybe b
こいつはぶっちゃけ、aが特定の型bだった時にJust xとして取りだせる関数です。こいつを使えば
ghci> gmapQ (fmap (+(1::Int)) . cast) abc1 [Just 2013,Nothing,Nothing] ghci> gmapQ (fmap (+1.1) . cast) abc1 [Nothing,Just 2.2,Nothing] ghci> gmapQ (fmap (++"onotoshigo") . cast) abc1 [Nothing,Nothing,Just "Tatsuonotoshigo"]
いっぽう、取りだす代わりに、データ構造の中をいじりたかったら、こうです。
gmapT :: (forall b. Data b => b -> b) -> a -> a
gmapTに、俺はすべてのデータを操れる能力がある(forall b. Data b => b -> b)とかいう厨二的関数を与えると、(a -> a)というより厨二的関数が返ってきます。ここで、普通の関数(f :: a -> a)を取って、fが処理できる型についてはf、それ以外の型についてはidとして振る舞う関数を返す補助関数casterを作りましょう。
caster :: (Typeable a) => (a -> a) -> (forall b. Typeable b => b -> b) caster f x = case (cast =<<) $ fmap f $ cast x of Just y -> y Nothing -> x
もちろん使うのはモナド。なぜならMaybeもまた、文脈の一種だからです。
ghci> gmapT (caster (+(1::Int))) abc1 ABC 2013 1.1 "Tatsu" ghci> gmapT (caster (+1.1)) abc1 ABC 2012 2.2 "Tatsu" ghci> gmapT (caster (++"onotoshigo")) abc1 ABC 2012 1.1 "Tatsuonotoshigo"
なんと、ABCの中に入っているIntやStringといった型を、パターンマッチで取りだしたりすることなく、外からいじることができました。しかし、この方法では、a1のようにimmediateじゃないsubtermのところに入っている文字列は操作できません。
ghci> gmapT (caster (++"onotoshigo")) a1 Abc (Bca (Cab (A "Happy") (B 4.2)) (Abc (B 5.6) (C 512 ...
こういう物体を操作するにはデータ構造の中に再帰的に踏み入る必要があります。
再帰的にScrap Your Boilerplate
関数 f::(a1->a) と値xを受けとって、xの中のあらゆるa1にfを適用したものをリストとして回収する関数を作りましょう。それは、xそのものにfを適用してみる部分と、xの子要素に再帰していく部分から書けるはずです：
recMapQ' :: forall a a1 a2. (Data a1, Data a2) => (a1 -> a) -> a2 -> [a] recMapQ' f x = (maybeToList $ fmap f (cast x)) ++ concat (gmapQ (recMapQ' f) x)
使ってみましょう：
ghci> recMapQ' ("Very "++) a1 ["Very Happy","Very appy","Very ppy","Very py", ...
ってあれ？文字列はCharのリスト構造であることから、目当ての文字列だけでなく全てのサフィックスが検出されてしまいました。最初にマッチした所で止めるには、こうします：
recMapQ :: forall a a1 a2. (Data a1, Data a2) => (a1 -> a) -> a2 -> [a] recMapQ f x = case fmap f (cast x) of Just y -> [y] Nothing -> concat (gmapQ (recMapQ f) x)
これで無事、めあての文字列だけを取りだせます：
ghci> recMapQ ("Very "++) a1 ["Very Happy","Very New Year!"]
おめでとう！さらに、元のデータ構造を保ったまま、文字列だけをいじるには、こんな関数をつくるとよいです：
recMapT :: forall a b. (Data a, Data b) => (b -> b) -> a -> a recMapT f x = let y = gmapT (recMapT f) x in case (>>= cast) $ fmap f $ cast x of Just z -> z Nothing -> y
これで、こうなります。
ghci> recMapT ("Very "++) a1 Abc (Bca (Cab (A "Very Happy") (B 4.2)) (Abc (B 5.6) (C 512))) (Cab (Abc (B 8.4) (C 208)) (Bca (C 2012) (A "Very New Year!")))
それ、Data.Generics.Schemesにアルヨー
-- | Apply a transformation everywhere in bottom-up manner everywhere :: (forall a. Data a => a -> a) -> (forall a. Data a => a -> a) -- Use gmapT to recurse into immediate subterms; -- recall: gmapT preserves the outermost constructor; -- post-process recursively transformed result via f -- everywhere f = f . gmapT (everywhere f) -- | Apply a transformation everywhere in top-down manner everywhere' :: (forall a. Data a => a -> a) -> (forall a. Data a => a -> a) -- Arguments of (.) are flipped compared to everywhere everywhere' f = gmapT (everywhere' f) . f
それっぽいのがアッタヨー
しかし、この二つは思ったように動いてくれません。まずeverywhereは
ghci> print $ everywhere (caster $ ("Very " ++)) a1 Abc (Bca (Cab (A "Very HVery aVery pVery pVery yVery ") (B 4.2)) ...
そしてeverywhere'は
ghci> print $ everywhere' (caster $ ("Very " ++)) a1 Abc (Bca (Cab (A "VVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVV VVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVV VVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVV^CVInterrupted.
というわけで、Scrap Your Boilerplate (Data.DataのgmapQとかgmapT)で文字列やリストを処理する場合には、無限ループに陥らないよう若干の手心を加えてやる必要がありますが、それにしても「任意のデータ構造をなめて、既知の型の部分だけ変更を加える」関数がこんなに簡単に書けてしまうとは驚きです。
今回使ったコードです： http://ideone.com/O9K2l http://codepad.org/9teQkUu4 どちらのサービスもData.Dataすらないのでコンパイルできてませんが…
皆様ことしもよろしくお願いします。
Simon Peyton-JonesがPFIにやってくる！
http://www.ustream.tv/recorded/17411671 （本編は31:46頃から）
Simon先生が「そっちの話も何か聞かせてよ」というので不束ながら前座をつとめさせていただくことに。サイモンさんはすごく気さくで何事にも前向きな人（あの台風でも却ってはしゃいでいた位）でこの人にしてGHCあり、というのがしみじみ分かりました。
GADTは恐れていたよりもずっとシンプルで親しみやすいものだった（定理証明に使うものとばかり・・・）
Nikolaの論文は見直さないといけないな・・・
DPHはNESLからだいぶ進化していてツリーも扱えるそうだが、スライドと疑似コードと口頭で聞いたことから僕が理解したことが少しづつ違っている。7.4から入るらしいので使ってみよう。
