今週やったこと

  1. ゴルフ
  2. Befungeプログラマとしてのレベルが0から1に
  3. WhitespaceインタプリタをHaskellで書いてたら途中で公式サイトにHaskellソースがあるのを発見orz
  4. 織田信長を実装したくなって調べる

つまり、何もしてない

    Haskell→PerlとRuby強すぎ
    Befunge→パズルっぽくて意外と面白い。あと意外と強い
    Whitespace→見掛け倒しで面白くない。めんどくさいだけ
    織田信長→名前の割に難しそう。よくわからん
名前の割にっても、AdaとOdaってあんま変わらんよね。


名前といえば、人の名前が付いてる言語として、haskell,Pascal,Curry,Adaあたりがあるけど、こういうのって、あっちの人には違和感ないのかねー。日本人だったらプログラム言語YamadaとかMatsumotoとかありえんよなー。もっとも、英語でも、JohnとかSmithは、ねーよって感じだけど。日本語でも、OdaとかNobunagaはアリな気がする。織田信長は長い。David Hilbertとかだと、Hilbertはいけるけど、Davidはないな〜。ということを考えると、名前がプログラミング言語に使われるかは、親近感湧く名前だとダメということかもしれない。まー、自分の名前が言語名になってたら、キモイな〜

結論:Linusはキモイ(言語じゃない)

Haskell Curryさんは、ミドルネームがBrooksらしい。プログラミング言語Brooksってのもアリな気がするので、誰かつくらんかな〜

C--とcmm

C--

C--ってGHC専用の中間言語だと勝手に思ってた。
http://www.cminusminus.org/によると

コンパイラ書く時に、機械語の生成どうする？自前でコードジェネレータ書くのは、めがっさ大変だし(いやまあ移植性を考えないでプラットフォーム決めうちならそうでもないかも)、VPO(って何?)やMLRISC(って何?)やgcc backendを利用するには、こいつらは巨大で複雑できちんとドキュメント化されてない上に、MLRISCを使うにはフロントエンドをMLで書かねばならないし、gccを利用するにはフロントエンドをCを書かねばならないとか、問題は山積み。あるいは、レジスター、末尾再帰最適化、computed gotos(って何のことだろう?)、GC、効率的な例外処理etcに関する沢山の結果を必要としないんなら、Cコードを生成するのもいいかもね。

でも、portableなアセンブリ言語があれば、もっとhappyになれんじゃね?そんな言語があれば高レベル言語のコンパイラとretargetableな最適化コード生成器のよい橋渡しになり、フロントエンド書きとコードジェネレータ書きは容易く協力できる。C--はそんな言語だ

とか、そんな感じらしい。まあ言ってることは、割とみんな思ってそうなことだよな〜


C--に関する最初の論文は、Simon Peyton Jones等によるC-: A Portable Assembly Languageらしい。けど、これは、コンセプトだけで、大したことは書いてないので、C--: a portable assembly language that supports garbage collectionとか読むほうがいい(一本だけ選ぶならこれにしろと論文リストに書いてあった)。C--自体は、GCとか、そういう機能は一切持ってなくて、そうしたruntimeのためのインターフェースのみがあるらしい。なので、runtimeの実装は自力でやらんといかん模様(それって、まあまあ大変な気が)。そういう風になってるのは、例外処理とか、GCとか、どういう設計にするのがいいかは言語によって違うから、ということらしい。HaskellやMLやPrologをJavaバイトコードに落としてJVMで走らせても、どう控えめに見てもパフォーマンスがいいとはいえない、結局JVMはJavaのためのVMだよねとか(そうなのか・・・)


GHCのcmmの説明はGHC Commentaryに割と詳しく載ってる。cmmは、GHCのC--実装ですとか書いてあるけど、全然C--じゃないような。C--は、まだCに近いっぽいけど(Quick C--のインストールが面倒で一個も動かしてないけど)、cmmはreturnもないし、関数も原則として引数取れなくて単なるラベルだし、処理はレジスター(Sp,Hp,R1,R2,..,L1,..)の操作を介して行うし、要するにSTGマシンのアセンブラという感じな。

構成的圏論

Coq 圏論

Constructive Category Theory

圏論を知ってれば、Coqの記号がキモイ以外は読みやすい論文だった。一般の型に属する値は等しいかどうかの判定が可能とは限らないので、ある型とその型の上の同値関係のペアとしてSetoidというのを導入する。同値な要素は、等しいとみなす。まあ、HaskellのEqクラスみたいなもんかなぁ(Haskellの==は全然同値関係になってなくてもいいけど)。例えば、自然数型はCoqでもNat=Z|Suc Natみたく定義できて(記法は違うけど)、自然にSetoidとみなせる。このSetoidを集合の代わりに使って、圏を構成する。Objectの「集合」は、もはや集合ではなく、単なる型で(Object同士が等しいかどうか判定できる必要はない)、一方、射の集合は、Setoidとなっている。以下、普通の圏論のように、Setoidの圏や、圏(普通の圏じゃないので、何か呼び方考えた方がいい気が)の圏を作ることができて、こんとき、ある圏Cからある圏Dへの関手の全体にSetoidの構造が自然に入るので、圏の圏もきちんと圏になる。Objectの全体が集合やSetoidではなくて、単なる型なので、small-categoryとかbig-categoryとかいうデリケートな問題は発生しないというのが面白い。あとは、なんか適当に米田の補題まで


疑問
・有限の概念が扱いづらそう。有限Setoidとか有限圏とかどうやって定義するんだろう
・上の流儀でもToposが定義できて、Setoidの圏はToposになるんだろうか。とりあえず、有限極限とか素直に定義できなそうなので、Toposが定義できるか分からん
・Coqのライブラリ見たら普通にSetoidとかあるけど、それとは別にSetsもある。Setsは、要素が集合に含まれるか否か判定する「関数」を与える通常の集合論に近い方法(っても型理論ベースだけど)っぽい。Setoidが、型の「商」を集合とみなす感じで、Setsは、型の「部分集合」を集合にする感じ。で、Setsをベースにした圏論ってのもできると思うんだけど、それはどうなんだろう。個人的にはSetoidの方が自然だと感じる。


もっとCoq力があれば自分であれこれしたいけど、無理っぽいし、そこまでやる気も起きないな。あともっと普通の数学(群とか環考えて、表現の圏とか加群の圏とか)との接点が見えないから、あれ。

なろーいんぐ

http://www.jaist.ac.jp/library/thesis/is-master-1997/abstract/matsuno/jabstract.pdf
によると、E-単一化問題を解くのがnarrowingと書いてあるけど、なんでE-単一化と呼ばないのか


Higher-Order Equational Logic
面白いな〜。Basic Narrowingとかは、多分first-orderの問題しか扱えないので、mapとかくると弱い気がする。高階関数をinline展開して一階に持ち込める場合もあると思うけど。例としてあがってた

father(mary) = john
father(john) = art

から、F(mary)=artの解Fを求めるとかいうのは、結構印象的。こういうのはPrologでは書けない(多分)。あと、微分は適切な関係式を与えておくと、
\x->diff(\y->ln(F(y)) , x)=\x->cos(x)/sin(x)
の解Fが見つけれるとか。数式処理で便利かもしれんな〜

■

雑談 雑談

Haskell数値計算が遅すぎるな〜とか思ったら、型指定しないで、x=1.56とか書いたら、x=156/100のように内部で扱われるっぽい。そら遅いわorz浮動小数点使うときは、型をFloatかDoubleか完全に指定しないとダメらしい。そこらへんいくと、Cleanは割と基本型は潔い。多倍長整数ないし、Realは64bit倍精度浮動小数点数らしいし、文字列はHaskellと違ってリストではないらしい

http://www.geocities.jp/lethevert/clean/gettingStarted03.html

Cleanでは、文字列は文字の配列として、"{#Char}"という型で表されます。"#"という記号は効率性を高める指定ですが、今は気にしないでください。

文字列は、よく使われる型なので、"{#Char}"には"String"という別名がつけられています。

Cleanの方がHaskellより速いとかって、こういうのが効いてんのかなー

型クラス

Haskell

Preludeの関数と、ByteStringの関数は、名前と機能が重複してるものが大量にあるのだけど、普通に両方使おうとすると

Prelude> :m + Data.ByteString
Prelude Data.ByteString> :t length

<interactive>:1:0:
    Ambiguous occurrence `length'
    It could refer to either `length', imported from Prelude
                          or `length', imported from Data.ByteString
Prelude Data.ByteString> :t Data.ByteString.length
Data.ByteString.length :: ByteString -> Int
Prelude Data.ByteString> :t Prelude.length
Prelude.length :: [a] -> Int

とかなってうざい件。

This module is intended to be imported qualified, to avoid name clashes with Prelude functions. eg.

 import qualified Data.ByteString as B

と書いてあるけど、両者のアルゴリズムはしばしば共通して使えるんでないのかな〜という気がするので(例えば、あまり意味はないけど、getContents>>=putStrとか)、B.lengthとlengthを区別せずに済む方法があればいいのにと思う。


で、型クラス使えばいいような気がして

{-# OPTIONS -fglasgow-exts #-}
module Container where
import Data.Word
import qualified Data.ByteString  as S
import Data.ByteString hiding  (length,map,null)
import qualified Prelude as P
import Prelude hiding          (length,map,null)

class Container s a where
 length :: s -> Int
 map :: (a -> a) -> s -> s

instance Container [t] t where
 length = P.length
 map = P.map

instance Container ByteString Word8 where
 length = S.length
 map = S.map

とか書いてみたんだけど

*Container> length [1,2,3]

<interactive>:1:0:
    No instance for (Container [t] a)
      arising from use of `length' at <interactive>:1:0-13
    Possible fix: add an instance declaration for (Container [t] a)
    In the expression: length [1, 2, 3]
    In the definition of `it': it = length [1, 2, 3]

しょぼーん(´・ω・｀)こういうの何とかなんないかな〜。後付けで、こういう拡張をしたいという状況はしばしばあると思うんだけど

どーでもいいけど、型クラスって普段あんまり自分で型クラス定義したりしないような。それとも、みんなバリバリ定義してるんだろうか。

Befunge

まあ、Befungeなら晒しても怒られなさそう。一応、Hello,worldとecho。delete_blank_linesは2個目のテストがtimeoutするんだよな〜orzまあ、Befungeのサンプルコード少ないしねッ。増やしていかないと(何のために?)。

続きを読む