challenge ciphertext

uezato yuya
@ranha C++のtemplateは良く知らないけど、全部判明してからじゃないと一致性チェック出来ない?(多分部分特殊化された状態でふにゃふにゃしたものをstructuralに見てくれない?)のでこれでヤるのは無理かなーと思った。(2009-10-18 17:52:09) link uezato yuya
@ranha うーんなんかC++ではむりぽいのう… http://d.hatena.ne.jp/ranha/20091018/1255857502(2009-10-18 18:22:49) link Kazuhiro Inaba
@kinaba #proofparty C++でa+0=0+aの怪しげな証明をば… http://codepad.org/L4feGX1J(2009-10-19 17:40:01) link Kazuhiro Inaba
@kinaba proposition用テンプレートを特殊化して勝手にインスタンス作られると破綻する。もちろん型安全性を壊す様なことをされると破綻する。停止しない計算を書かれても破綻する。そもそもグローバル変数を使い回すせいで二重帰納法されると破綻する。(2009-10-19 17:42:47) link Kazuhiro Inaba
@kinaba addみたいなinductiveな関数を汎用に追加できるようにするのは、やればできるけど面倒なのでやってないだけ。(2009-10-19 17:44:26) link kikx
@kikx ふむふむ、これは型theoremのインスタンスpが作れたから証明できたってことだな(2009-10-19 18:49:40) link kikx
@kikx *pfがNULLでもいいところがなんか問題なきもしなくもないがよくわからん(2009-10-19 18:58:58) link kikx
@kikx このままだと、forall y , (forall x, x+0=0+x) -> y+0=0+y. にできないなあ。(2009-10-19 19:15:03) link めどすけ
@heppoko_maid @kikx なるほど。ざっとしか見てませんが、induction stepは関数になるので*がついてると。たしかにNULLだと困りそうですが、NULLにはならないように見えますので問題ないのでは。(static assertでNULLチェックできれば追加するといいかも)(2009-10-19 19:28:21) link kikx
@kikx あーわかったぞ、templateはforallする変数名とPropの引数名がまじってるからよくないんだな(2009-10-19 20:07:42) link めどすけ
@heppoko_maid @kikx これは正確には、forallという名前付けの問題(?)のように見えます。nat::forallはinductionに特化した証明になっているので、沖句さんの使っているforallのような(functor的な)使い方はできないですね。(2009-10-19 21:00:52) link kikx
@kikx こんな感じでforall に apply をつけてみたんだけど、NとYが違うのでまだうまくいってないのです。http://codepad.org/d3ELuDVL(2009-10-19 21:23:21) link kikx
@kikx たぶん、T -> Y -> subs::type のインスタンスがあれば残りは埋められるんじゃないかなと思っているのです(2009-10-19 21:25:43) link めどすけ
@heppoko_maid @kikx こうやろうとすると、forall::applyの証明がパラメータYの構造に依存してしまうような。forallは普通の定義にして、inductionからforallまたはsubtypeが出てくるようにすればいいのかなーと、なんとなく思ってます(2009-10-19 21:32:52) link uezato yuya
@ranha Conceptあったら状況は変わったんだろうか・・・。うひっ。(2009-10-19 23:41:10) link Kazuhiro Inaba
@kinaba 先程のa+0=0+aを少し説明すると、「X=Yの時に限りeq型の値が作れる」ように型を作ってます。eq_refl/tran/symm等だけがeqを作れる”公理”。他の(真っ当な)手段では作れない。（確かにそう作ってある、とは誰も保証してないので、ここはそう信じる部分。）(2009-10-20 00:05:52) link uezato yuya
@ranha C++は中身書かなくて良いから型さえ書けりゃあ証明した事に成る。ぶもも。(2009-10-20 00:08:54) link Kazuhiro Inaba
@kinaba その準備の上で、inductive_proof::base()はeq<0+0,0+0>型の値を作っていて、同step()は、eq<0+N,N+0>の値が与えられれば、eq<0+s(N),s(N)+0>の値を作れるよ、という関数。あとは合わせて帰納法。(2009-10-20 00:10:43) link Kazuhiro Inaba
@kinaba ただし、帰納法を回す側は、「eq<0+s(N),s(N)+0> step( eq<0+N,N+0> ) という型のつく関数があるなら、確かにeq<0+N,N+0>からeq<0+s(N),s(N)+0>は作れるんだろう」と仮定しちゃっているんだけどこれは本当は間違いで(2009-10-20 00:12:49) link Kazuhiro Inaba
@kinaba というのは、eq<略1> step( eq<略0> x ) { return step(x); } としてしまえば型チェックは通るけど、これじゃ無限ループして eq<略1> 型の値は作れてない。間違い。これを避けるために、本物の証明記述言語は、無限ループは書けないようになってる。(2009-10-20 00:15:55) link uezato yuya
@ranha .@kinaba 面白かったので、私が勝手に面白いみたいなエントリをはてなに書こうと思ってたんですけどそれはちょっとクオリティ下げて他の人に刺される気がするので、良かったらblogで解説してください！(2009-10-20 00:17:28) link Kazuhiro Inaba
@kinaba @ranha さんが刺されて大惨事流血沙汰になったブログは面白そうなのでちょっと見てみたい…じゃなくて、はい、後でまとめておきます。たぶん水曜の夜になります(2009-10-20 00:43:11) link めどすけ
@heppoko_maid 前に書いていたのは、nat_ind P := P 0 -> (forall x. P (S x)) -> forall x. P x が帰納法なので、forallをbasisとして用意しておいてそれをsubstに適用したほうが簡単じゃないかと思った次第。(2009-10-20 01:40:59) link めどすけ
@heppoko_maid 帰納法をつかって(natに特化した)forallを言ううまいやり方はどうも思いつかないなあ。(2009-10-20 01:41:37) link めどすけ
@heppoko_maid substが完全一致ではなくて、ちょっと弱めてeqなのは言えるのかもしれない。(2009-10-20 01:44:16) link uezato yuya
@ranha うーん　多分加算可換性をC++のコンパイルタイムに証明出来た気がする・・・。Lemma毎に取りあえずnamespace分けていたのだけれども、そうするとパターン変数(何の意味も無い兎に角パターン変数だけ表す)が全部別々になって悲しいので、共通に括りだしてやり直せば・・・。(2009-10-20 04:39:46) link uezato yuya
@ranha forallの形でやりにくい(forallな変数が2つとか出てくると)ので、9個ぐらいまでの場合を準備しておいてどうこう、とやるか、やっぱりパターン変数をglobalに置いてどっこいしょみたいな感じなのかなぁ・・・。という。(2009-10-20 04:41:00) link uezato yuya
@ranha namespaceってtemplate引数持てないのかぁ。なんかもう普通に依存型のモジュールとかではぼそぼそとか思ったけど。(2009-10-20 12:21:21) link Kazuhiro Inaba
@kinaba 可換性もやってみようとしたけどめんどうだ。http://codepad.org/DydSnKP0 (途中)。nat::forall から Prop[X/N] を導くには N がzeroとsuccからinductiveに作られてることの証明が必要。つまりNの型が…。(2009-10-20 12:33:06) link uezato yuya
@ranha ただforall tな所に型が潜り込んでで縛りが無い(例えばzeroとsuccに関係性が無い)ので、ダメダメだなーと思います。ふーみゅ・・・。一応証明テンプレート(baseとstep)があるのでユーザはそれに則る様にすれば・・・とは思うんですが。(2009-10-20 14:37:45) link uezato yuya
@ranha なんだろう、Conceptは知らないんですけど、Conceptがあればtype family的な事が出来て、一見無関係な型に制約を付けて無関係では無くしたり、後は明らかに違法なものが渡ってくる事を防いだりは出来るのかなぁ・・・。(2009-10-20 14:38:30) link uezato yuya
@ranha struct Dummy{}; struct zero{}; template struct succ {}; これだと、succみたいなのも出来るのがソレっていう感じなんですが、一方succみたいなパターンを表す型も渡したいので…(2009-10-20 14:56:15) link Kazuhiro Inaba
@kinaba @kikx (forall x, P x) の証明オブジェクトが帰納法のベースとステップの証明をメンバ変数に持っておくのが正攻法なんですけど、帰納法ステップって多相型の関数なので、型を一度もごまかさないで変数にとっとくのってC++だと無理なんですよね、これ。(2009-10-20 16:27:04) link Kazuhiro Inaba
@kinaba forallを帰納法に特化させない場合も同じことで、template P operator()(X x) な関数テンプレートを値として持たねばならぬ。C++/DよりJavaかScala辺りでやった方が多分楽。(2009-10-20 16:33:59) link Kazuhiro Inaba
@kinaba @ranha forall::conv が、返値型がPropだけど実際にはProp型のオブジェクトを作れてないので、その辺がよろしくないです。(2009-10-20 16:40:54) link uezato yuya
@ranha . @kinaba そこはもう完全に不味い匂いがぷんぷんぷんぷんする所なんですが、そもそも不味いですけども、C++的にどのタイミングでどのくらいテンプレート周りが固まって行くかとか分からないので全体が霧掛かって分からない感です。取りあえずソコを考え直します。(2009-10-20 16:48:25) link kikx
@kikx http://codepad.org/AjZoGD52 やっとコンパイル通ったよー ＞@kinaba @ranha @heppoko_maid(2009-10-20 17:39:59) link uezato yuya
@ranha forallの形を辞めて、template引数で渡って来た値の意味を全称変数にしちゃって、帰納的操作を全部隠蔽してそこに投げさせる感じかなー(2009-10-20 17:49:21) link Kazuhiro Inaba
@kinaba @kikx ∀x(0+x=x+0) の証明オブジェクトじゃなくて 任意のxに対して(0+x=x+0)の証明オブジェクトを返すジェネレータを作ってる感じですかね。これで ∀x∀y(y+x=x+y) の二重帰納法回せるかな…(2009-10-20 17:50:52) link kikx
@kikx A->B は全部 template struct AimplB { static B proof() {}; }; で表現しないと、どうしようもない気がするけど、実際にインスタンシエートされないと型があってるのかわからんなあ(2009-10-20 17:53:33) link kikx
@kikx やっぱりインスタンシエートしないと型チェックされないのがいかんなあ。コンセプトとか使えばいいわけ？(2009-10-20 18:01:02) link uezato yuya
@ranha 私のヤツは実際に値入れてまわすと死ぬなぁ・・・。これは良く無い・・・。あとLeibniz Equalityも書こうと思ったけど酷い感じになる取りあえず晩ご飯！！(2009-10-20 18:01:17) link Kazuhiro Inaba
@kinaba 具体的な値が与えられたときだけ動くんだから、そりゃ二重帰納法でもなんでもできるか。それもそうだ。genericsじゃなくてtemplateなC++でやるなら、forallの証明をチェックするのは諦めてforallをインスタンス化したらチェックが初めて走る、の方がとっても自然だ(2009-10-20 18:01:26) link kikx
@kikx C++だと証明されたプログラムとして使うなら、結局有限個のインスタンスに対して証明できれば十分だし、これでいいのかなあ(2009-10-20 18:07:35) link uezato yuya
@ranha Conceptは一体何が出来たんだろう夢膨らむ。いや膨らまないけど…(2009-10-20 18:16:19) link uezato yuya
@ranha ていうかテンプレート引数はソレ自体の型が無い(情報が無い)ので、依存型みたく出来ない(あいつらは一応Πx∈T.P(x)みたいな感じで情報はある)のでそういう所でC++は違うのかなーっていうか。(2009-10-20 18:20:38) link kikx
@kikx struct forall { template FroallImpl::prop proof(ForallImpl proofed); } にすればいい気がしてきた(2009-10-20 19:11:07) link uezato yuya
@ranha C++で再びNat上での加算の可換性の証明を行った。 http://d.hatena.ne.jp/ranha/20091021/1256055346(2009-10-21 01:16:24) link uezato yuya
@ranha 物凄くどっち付かずに成っている・・・。kinabaさんの方法だとコンパイル時に強めのチェックが掛かるけれども今のままだと少し手厳しいのと、私が１つ前に張ったconv付き(forallの全称変数を具体化)のヤツはまぁ何とか残念にくぐり抜ける系だったので、もうそれを認めるとか…(2009-10-21 01:44:39) link uezato yuya
@ranha kikxさんのと今張ったものは、コンパイル時の「証明本体」の部分のチェックがゆるゆるガバガバすぎ。はふぅ。(2009-10-21 01:45:50) link uezato yuya
@ranha ああー でもaddの定義を変えて、元のeq_addにすれば何とか成るかも…(2009-10-21 01:50:05) link Kazuhiro Inaba
@kinaba http://bit.ly/O3ywA にっきかいた。#proofparty の人たちには別に新しいことは何も書いてないですが(2009-10-22 02:20:51) link

http://twitter.com/ranha/status/4963443406
http://twitter.com/ranha/status/4963710852
http://twitter.com/ranha/status/4992309733
http://twitter.com/ranha/status/4992902814
http://twitter.com/ranha/status/4993087027
http://twitter.com/ranha/status/4998693697
http://twitter.com/ranha/status/4998668844
http://twitter.com/ranha/status/5012168330
http://twitter.com/ranha/status/5012178660
http://twitter.com/ranha/status/5012427153
http://twitter.com/ranha/status/5013852410
http://twitter.com/ranha/status/5014581387
http://twitter.com/ranha/status/5014724694
http://twitter.com/ranha/status/5014907543
http://twitter.com/ranha/status/5014961041
http://twitter.com/ranha/status/5021794451
http://twitter.com/ranha/status/5022366059
http://twitter.com/ranha/status/5022390225
http://twitter.com/ranha/status/5022477888
http://twitter.com/ranha/status/5009375909
http://twitter.com/kinaba/status/4986574175
http://twitter.com/kinaba/status/4986609522
http://twitter.com/kinaba/status/4986629525
http://twitter.com/kinaba/status/4992837647
http://twitter.com/kinaba/status/4992942470
http://twitter.com/kinaba/status/4992987276
http://twitter.com/kinaba/status/4993053072
http://twitter.com/kinaba/status/4993650737
http://twitter.com/kinaba/status/5009660665
http://twitter.com/kinaba/status/5013585023
http://twitter.com/kinaba/status/5013673067
http://twitter.com/kinaba/status/5013758164
http://twitter.com/kinaba/status/5014600290
http://twitter.com/kinaba/status/5014726804
http://twitter.com/kinaba/status/5048073877
http://twitter.com/kikx/status/4987449708
http://twitter.com/kikx/status/4987553208
http://twitter.com/kikx/status/4987765703
http://twitter.com/kikx/status/4988486871
http://twitter.com/kikx/status/4989678555
http://twitter.com/kikx/status/4989716060
http://twitter.com/kikx/status/5014473813
http://twitter.com/kikx/status/5014632634
http://twitter.com/kikx/status/5014721330
http://twitter.com/kikx/status/5014803334
http://twitter.com/kikx/status/5015583215
http://twitter.com/heppoko_maid/status/4987936670
http://twitter.com/heppoko_maid/status/4989307974
http://twitter.com/heppoko_maid/status/4989831474
http://twitter.com/heppoko_maid/status/4994894814
http://twitter.com/heppoko_maid/status/4994908081
http://twitter.com/heppoko_maid/status/4994963273

http://twitter.com/ranha/status/4126621880

http://twitter.com/ranha/status/4126639529

http://twitter.com/ranha/status/4126669748

この辺が参考になる?

http://www.haskell.org/pipermail/haskell/2006-July/018172.html

http://guppy.eng.kagawa-u.ac.jp/~kagawa/PVH/

http://twitter.com/ranha/status/3598749459
http://twitter.com/asm__/status/3598819573
http://twitter.com/m0h1can/status/3598890839
http://twitter.com/ranha/status/3599046158
http://twitter.com/ikegami__/status/3598831349
http://twitter.com/ranha/status/3599115276
http://twitter.com/ranha/status/3599164655
http://twitter.com/m0h1can/status/3599115357
http://twitter.com/m0h1can/status/3599238569
http://twitter.com/m0h1can/status/3599286928
http://twitter.com/m0h1can/status/3599297298
http://twitter.com/ranha/status/3599244158
http://twitter.com/ranha/status/3599258696
http://twitter.com/ranha/status/3599348816
http://twitter.com/ranha/status/3599373755
http://twitter.com/ranha/status/3599396533
http://twitter.com/ranha/status/3599457002
http://twitter.com/ikegami__/status/3598877012
http://twitter.com/alohakun/status/3600138039
http://twitter.com/alohakun/status/3600156447
http://twitter.com/alohakun/status/3600185237
http://twitter.com/ikegami__/status/3600201641
http://twitter.com/ikegami__/status/3600214738

uezato yuya
@ranha 初期の頃の、静的型付け言語っていうのは、何か理由があってそうなってたんだろうか。型チェックに基づく安全性とか、最適化とか、そういう事は考えられてなくて、自然と型っていう発想がただそこにあったんじゃないかなぁみたいな。うーん。50,60年前・・・?(2009-08-28 17:02:31) link asm
@asm__ @ranha 型付けというより何バイト割り当てるか だったんじゃないかな C++からやたら厳しくなった理由は…なんかあった気がする(2009-08-28 17:09:45) link Ikegami Daisuke
@ikegami__ 確かに、型理論と論理学や圏論が合流したのは最近である(2009-08-28 17:10:53) link Ikegami Daisuke
@ikegami__ でも、型付き Lisp は 50 年前くらいからあるのかな?(2009-08-28 17:15:25) link モヒカンではない
@m0h1can 最初ってビット幅が型で、まぁとりあえずデータ壊さない為の目印だった、とか勝手に思ってるんだけど、こんなテキトーな嘘かけば賢人が教えてくれるかなー(2009-08-28 17:16:51) link uezato yuya
@ranha 1958年、ALGOL 58とか想像しにくいぐらい昔で何が起こっていたんだろう。むしろ単に、区別を無くす、っていうような発想が無かったんじゃないだろうか。(2009-08-28 17:33:19) link uezato yuya
@ranha そういう事考えると、1960ぐらいのLispとかおめがヤバい感じが・・・。(2009-08-28 17:40:42) link モヒカンではない
@m0h1can FORTRAN I(1954)の時点で型あったんじゃない？整数や小数点を区別したり、コンパイラだからか？(2009-08-28 17:40:43) link uezato yuya
@ranha FORTRANに型があるのは、なんか単純にアセンブリのインストラクションにあるのをそのまま持って来た感じかなーみたいな。浮動小数点命令セットとか、数値命令セットとか・・・。その区別を持ち上げると自然とああはならないのか。お分かりだろうか?分かりません。(2009-08-28 17:45:51) link モヒカンではない
@m0h1can まともにデータ型区別するのは66以降ですね(2009-08-28 17:53:39) link uezato yuya
@ranha 「機械語とのセマンティクスギャップが少ない」「一般的には機械語やアセンブリ言語を指す。」絶望があった　http://bit.ly/EFD6x(2009-08-28 17:54:16) link uezato yuya
@ranha ランタイムエラーとか起こされると資源的な意味で多分暴動が起きるので、そういう事を許さない為にチェックとかなって、チェックするのには型が使えるから型チェックみたいな・・・。(2009-08-28 17:55:48) link モヒカンではない
@m0h1can ただ少くともラッセルの型みたいな抽象的な何かを導入する発想はコンピュータ以前に広まってたと思ったりしますね(2009-08-28 17:58:55) link モヒカンではない
@m0h1can 型を明確に意識した最初の実装は何で誰だろ？(2009-08-28 18:00:01) link uezato yuya
@ranha 少なくとも、LCF MLの頃は、今で言う　型　をそれだと言っても問題は無い気がしていて、でもそれは70年最後、80年頭ですしその間になんか。simply typed λcalculusとか普通にどうなのかなぁ・・・。(2009-08-28 18:05:10) link uezato yuya
@ranha Simulaとかあの辺はジャストミートなのでは無いかとか思ったけど分かりません。型とかいうよりは、オブジェクトと、その関係とかなのかなぁ。でもそういうのは多分それだと思う。(2009-08-28 18:07:48) link uezato yuya
@ranha untyped λ-calculusから、typed λ-calculusにresearchが移ったなんかみたいなのは、全然知りませんけど、そうなのかなぁ。結局そこに在ったけど、見ていた/考えていたものが違えばそれは別なので、そういう事で見ると…?(2009-08-28 18:10:14) link uezato yuya
@ranha そもそも研究と、実用では、要請が違うんだろう。でも今は、それらが結びついているのだとすると、それは良い世界なのでは無いかとちょっと思います。元々意図していなくても、結局同じ事をやってればいつか繋がる時が来るんだろうか。(2009-08-28 18:16:38) link ザイロリック錠
@alohakun 型の発想って、群論とかそこらへんなんじゃないですかね。集合に対して許される演算の集合が規定される。(2009-08-28 19:28:09) link ザイロリック錠
@alohakun 望ましい性質を備えたプログラムの集合を定義しようと思うと、自然と型理論の発想に行き着く気がするけど。昔は、プログラムを動かすだけで精一杯だったから、プログラムの性質についての議論が深まるのは、少し時代が進んでからだと思う。(2009-08-28 19:30:04) link ザイロリック錠
@alohakun 計算機械や初期の言語にも、「型」そのものの概念はあったのだろうけど、まだ「理論」は無かったんだろうね。(2009-08-28 19:32:48) link Ikegami Daisuke
@ikegami__ 型付けされた言語の型は、群ほどきれいな構造を持ってないですよ。もっとしょうもない性質しかない。だから、圏論とか論理学に近い(2009-08-28 19:34:28) link Ikegami Daisuke
@ikegami__ 圏論や論理学がしょうもない、とは言ってません。圏論や論理学のしょうもない部分を型の理論の裏付けとして使ってる(2009-08-28 19:35:46) link

FLTVの発表資料が全力でイバヤーバイ

http://twitter.com/ranha/status/3397159331

http://twitter.com/ranha/status/3397286509

自分で言っててなんですけど、これとかは割と当てになる指針だと思います。

あと、大体の人は難しいもの/難し「そうな」ものが出てくると「後で読む」を志して二度と読まないのでそういう人騙しにも出来そうですよね。

まぁ別に騙してないんですけど・・・気持ちの問題があるとするならばそういうの抑えるのにも一役買うんじゃないでしょうか。

http://twitter.com/ranha/status/3397189809

それはまぁ取りあえず

http://twitter.com/ranha/status/3397376357

とかで良いと思います。

そして何よりも

http://twitter.com/ranha/status/3397318132

コレ！！コレだよコレ！！

http://twitter.com/ranha/status/3397456341

分かんにゃい・・・。

http://twitter.com/m0h1can/status/3397390526

この成果をなんとかして育成シミュレーション、恋愛アドベンチャー型言語に活かしたい。

でもそういうのは割と冗談じゃなくて、現場の方が苦しいよー苦しいよーって成った時に苦しい部分を解決したいだろうから、という意味で大体良いものが出来る時もあるんじゃないかなーと。

基礎研究所だとしかしながら結局偉そうな人が来るのでうーんむみたいな。

http://twitter.com/m0h1can/status/3397441968

はい。

http://twitter.com/ranha/status/3397579051

これはホントやりたいです。

発端

http://twitter.com/ranha/status/3318384175

http://twitter.com/ranha/status/3318729080

この発言は、

MakeProd :: 圏A → 圏B → 圏AxB(これが直積カテゴリ)

みたいなMakeProdを作れないかなーという事です。

これだと、2引数とったり、関手レベルでカリー化出来ないと行けないのでムムム。

それに対して

http://twitter.com/bonotake/status/3319122903

確かにコレなら！！

http://twitter.com/ranha/status/3319488961

ただしこれだと、元々直積したかった圏D,圏Eに加えて、圏Cと圏C→圏Dの関手、圏C→圏Eの関手を作らないといけないので大変そう。

http://twitter.com/ranha/status/3319828800

http://twitter.com/ranha/status/3319846689

「元々直積したかった圏D,圏Eに加えて、圏Cと圏C→圏Dの関手、圏C→圏Eの関手を作らないといけないので大変そう。」でやるとすると、多分こんな感じ?

http://twitter.com/bonotake/status/3319486001

これは良く分かりません・・・。

http://twitter.com/ranha/status/3319802225

http://twitter.com/bonotake/status/3319730332

2階圏の対象を1階圏として、そうすると射は事実上1階圏から1階圏へ、となりますが、そのとき射って関手になるのかなーとか。

あと、関手じゃないと実装が書けないみたいなイメージがあるんですけど、そうでも無い?

Catの関手書く時にしたって、arityは1だからどっちみち同じ問題に遭遇するんでは無かろうか・・・。

Cat x Cat → Cat　の時は、でも、Cat x Catを「関手に任せるんじゃなくて」「定義に従って手でやれば良い」感じなのかな。でも対象が多く成ると結局定義に従って手でやるとかは無理な気がする。手でやるってその範囲はどこからよ、みたいな・・・。

Catの「射」として、実装を伴わせた「parametric polymorphism」な射を作って、そいつで「カリー化」すればいけそうな雰囲気ですけど・・・。

LCF MLについての一冊。

http://www.amazon.com/Edinburgh-LCF-Mechanized-Computation-Computer/dp/3540097244

Polymorphic type inference and assignment

http://gallium.inria.fr/~xleroy/publi/polymorphic-assignment.pdf

“Further reading”

http://caml.inria.fr/pub/docs/manual-caml-light/node20.html

CAML Primer

http://hal.inria.fr/inria-00070045/en/

全てcamlspotterさん情報

“Edinburgh-LCF-Mechanized-Computation-Computer”はちょっと大学の演習のからみがあるので優先して読みたいですね。