参考： MLソースを扱うとき - 檜山正幸のキマイラ飼育記 メモ編 デスクトップにIsabelle2016（少し古い）のアイコンがある。 このアイコンは C:\Installed\Isabelle2016\Isabelle2016.exe を指している。 Isabelle2016.exeの実体は、jEditをフロント、PolyML…

型クラスのパラメータ問題（トラブルっぽい話）が出てくるのは、指標とモデルの相対性の考察が不足しているせいだと思う。グロタンディーク平坦化を“積分”とみなしてのフビニに定理だと思う。繰り返し積分と同時多重積分の同値性。直積領域の積分ではなくて…

MLのモジュールシステムは禁欲的で、必要最小限の機能だけだが、スッキリしていて好きだ。だが： signatureにパラメータを付けられない。functorは当然にパラメータ（引数）を持つが、functorの値はstructureであってsignatureを値には取れない。 これは当然…

昨日の 型クラスの比較 - 檜山正幸のキマイラ飼育記 メモ編 への補足説明。既存のものに後からゴチャゴチャ文句を言うのは簡単だ。だから文句言う。コアージョン（coercion - 檜山正幸のキマイラ飼育記 メモ編）は必要悪という意味で必須だから、使うのはい…

Standard MLが圧倒的に良くできているな。オーバーロードを意図してない、型システムじゃない、という問題点はあるが、許せる、許せる。Haskellは「悪いお薬」をキメている。当座はとても元気が出るが、いずれは心身を蝕むアレ。型名に対するコアージョンを…

fun plus x y = x + y; (* OK *) val plus = fn x => fn y => x + y; (* OK *) val plus = fn (x, y) => x + y; (* OK *) val plus = fn x y => x + y; (* NG *) 最後がNGなのが納得がいかない！ が、そうなんだから仕方ない。最初のような書き方をするしか…

32bitのMinGW/MSYSを入れなおした configureは成功 makeは、CONDITION_VARIABLEで失敗 次にMinGW32のposix pthreadライブラリをインストールしてみる。だが、Cygwinでないとpthreadが存在しても使ってくれないようだ。次に、/mingw へのマウントを TDB-GCCに…

ちゃんと記録をとってなくて、記憶だが：CONDITION_VARIABLEとは、Windowsが定義する型なのだが、 gcc 4.6.2 付属のwindows.hでは定義されてない。 gcc 4.9.3 付属のwindows.hでも定義されてない。 gcc 5.1.0 (tdm-gcc) 付属のwindows.hでは定義されている。…

configureは終わって、makeするとエラーする。 make[2]: Entering directory `/c/Installed/polyml-github/libpolyml' /bin/sh ../libtool --tag=CXX --mode=compile g++ -DHAVE_CONFIG_H -I. -I.. -O3 -mthreads -I../libffi/include -DUNICODE -D_UNICODE …

Isabelleの ./conrib/polyml-5.6-1/x86[_64]-windows/ のlibgmp*.dllは、 GNU Multi-Precision Library（GMP）のライブラリだ。

Isabelleの ./conrib/polyml-5.6-1/x86-windows/polyc を手直しして ~/bin/polyc32 とした。動くようになったが、色々とまだ不便。 #!/bin/sh IsabelleHome=/c/Installed/Isabelle2016/ PolymlVer=5.6-1 Missing=missing PolySuffix=poly prefix=${IsabelleH…

言語仕様がちゃんと定義されていて、処理系もたくさんある ( http://sml-family.org/) のに、なんか残念感がただよう。 パッケージマネージャがあるにはあるが (https://github.com/standardml/smackage)、使われている形跡がない。 パッケージングの方法が…

WikiPedia Isabelle -- https://en.wikipedia.org/wiki/Isabelle_%28proof_assistant%29 Isabelle -- https://isabelle.in.tum.de/ https://isabelle.in.tum.de/community/Main_Page http://isabelle.in.tum.de/repos/isabelle/ http://www.isa-afp.org/ htt…

2016-05-27 - 檜山正幸のキマイラ飼育記 メモ編の日からQuantomaticのメモがある。この日より前にインストールはしてるはず。日付は忘れたが、 Quantomaticをインストール Isabelleと関係ありそうだと気づく。 Isabelleをインストール Isabelleすごい！ と感…

Standard MLは、標準のパッケージマネージャもインターネット上のモジュールアーカイブサイトも持ってない（モジュールアーカイブとパッケージマネージャ - 檜山正幸のキマイラ飼育記 メモ編）。プログラミング言語にとって、ライブラリやツールは、言語仕様…

$ git clone https://github.com/polyml/polyml.git polyml-githubでソースも入れた。ビルドはGNU Autotoolsだ。configure; make 方式ね。とりあえずconfigureしたが、なんか色々やったようだが、よくワカラン。PolyML.slnがあったので、startさせると Visua…

Isabelle2016をインストールしたら、PolyMLが付いていた、つうか、PolyMLはIsabelleの実装言語。PolyMLはStandard MLの実装。PolyMLのFAQ http://www.polyml.org/FAQ.html によると、IsabelleとPolyMLの歴史はほぼ一緒らしい。https://en.wikipedia.org/wiki…