プログラミング
これから書くのは、言葉や論理と、その意味に関する話だ。フレーゲらによる、物事を厳密に考える言葉の探求は、現代論理学や分析哲学の出発点になった。まずは、その哲学を探りながら、関数プログラミングの話でよく耳にする「参照透過性」という概念を理解…
僕は、プログラムを哲学したい。その動機のひとつに、用語の統一がある。現状、プログラムにおいて使われる用語は、対象言語によって色々と異なってしまっている。たとえば、似たような概念に、あるプログラム言語ではポインターという用語を使い、別の言語…
Hagino’s Categorical Programming Language について紹介します。wikipedia:CPL (圏論プログラミング言語)によれば、 CPL (正式名称:Categorical Programming Language) は圏論に基づいたデータ型の定義と計算モデルを持つ関数型プログラミング言語であり…
Tao3Dは、インタラクティブなスライドやアニメーションが作成できるプログラミング言語および開発プラットフォーム。Windows版, OS X版, Linux版のパッケージが用意されている。Tao3D Libre EditionはGPLv3でライセンスされている*1。Tao3Dを起動すると、Wel…
こわくない Idris (6) - M59のブログ こわくない Idris (6) - M59のブログ 1年前に書いた記事を読み返していたら、証明がすぐには理解できなかった。証明の内容を言葉で分かるように書いておきたいと思う。次のコードのMyHead.headは、全域函数だ。 %default…
を読んで、思ったことを書く。「プログラムは思った通りに動かない。書いた通りに動く。」いったい誰が言ったのかは分からないこの箴言だが、ただ当たり前のことを言っただけでは箴言にはならなくて、ここには意外性がある。つまり、この箴言に出会う前の人…
本の虫: 2014-05-pre-Rapperswil mailingのレビュー N4015でHaskellのdo記法風っぽいdo式を入れる提案があるわけなのだけれども、そもそも手続き型の記法でプログラミングができるC++の上にさらにモナドを使って手続き型風記法でプログラミングするためのdo…
javac 1.8.0_05を使っていたところ、意味不明なwarningが出た。 Test3a.java:9: 警告: [unchecked] raw型Listのメンバーとしてのadd(E)への無検査呼出しです ln.add(10); ^ Eが型変数の場合: インタフェース Listで宣言されているEはObjectを拡張します原文…
Haxeには複数のターゲットがあり、文字列のAPIは共通だが、それぞれで文字列の内部表現が異なっている。普通にプログラムを書いても、ターゲットによって結果が変わってくる。 class Main { public static function main() { var s = "\u{20000}𩸽あëa"; tra…
ネタ元: performance - What is the overhead of Rust's Option type? - Stack OverflowRustにはnull値がなく、代わりにOptionを使う。このOptionは、ポインタ型に対しては最適化されるそうだ。確認してみる。(rustc 0.10を使った。) use std::mem::size_of;…
現状Rustにはランタイムライブラリーが2つ実装されていて、ネイティブスレッドを使うlibnativeとグリーンスレッドを使うlibgreenがある。詳細はA Guide to the Rust Runtimeにある。実際にそれぞれのランタイムライブラリーを使ったFizzBuzzを作って試してみ…
毎度おなじみFizzBuzzでRustの変更点を確認しよう。 fn main() { let (tx, rx) = channel::<(int, std::str::MaybeOwned<'static>)>(); for i in range(0, 100) { let tx = tx.clone(); spawn(proc() { let i = i + 1; let b = match (i % 3, i % 5) { (0, 0…
RustにはEnum std::send_str::SendStrがあって、これは送信可能な文字列型である~strか&'static strのどちらかを保持する。Trait std::send_str::IntoSendStrのメソッド fn into_send_str(self) -> SendStr を使って、それらをSendStrに変換できる。例のFizz…
自然言語を主語(S)・目的語(O)・動詞(V)の語順で分類するように、プログラミング言語もオブジェクト(O)・実引数(A)・メソッド(M)の語順で分類できる。(Smalltalk, C++など)よくある語順オブジェクト指向言語風の語順はOMA型だ。一方で、(GObject/C, CLOS/…
例のごとくFizzBuzz // for Rust 0.9 fn main() { let (port, chan) = SharedChan::new(); for i in range(0, 100) { let chan = chan.clone(); do spawn { let i = i + 1; let b = match (i % 3, i % 5) { (0, 0) => ~"FizzBuzz", (0, _) => ~"Fizz", (_, 0…
こんなプログラミング言語を考えている。Shiba fact: { @ if ( = 0 ) :x { 1 } { * :x fact ( - 1 ) :x } x: } fact 10 even: { @ if ( = 0 ) :x { true } { odd ( - 1 ) :x } x: } odd: { @ if ( = 0 ) :x { false } { even ( - 1 ) :x } x: } even 42 even…
マイナー言語 Advent Calendar 2013 のネタにしました。 Kittenでスタックと戯れる - Qiita [キータ]Kittenって子猫って意味なんだけど、それ以前にCatって言語があったみたいだ。concatenateのcatなのかな。
https://github.com/mandel59/hxcpp/commit/703b0f7129edc72fdead9ff9f034f42cc2ba1ec9 - return ((c & 0x0F) << 18) | ((c2 & 0x7F) << 12) | ((c3 << 6) & 0x7F) | ((*ioPtr++) & 0x7F); + return ((c & 0x0F) << 18) | ((c2 & 0x7F) << 12) | ((c3 & 0x7F…
Ceylon 1.0.0がリリースされました。 米Red Hat、新言語「Ceylon 1.0」発表、初のプロダクションリリースに | SourceForge.JP MagazineRedHadがCeylonって言語を作っていることはどこかで読んで知っていました。でも、JVMをターゲットにした言語だし、ウェブ…
こういうバージョンの処理系で試した。 $ go version go version go1.1.2 linux/amd64 $ rustc --version rustc 0.9-pre (825b127 2013-11-12 18:56:13 -0800) host: x86_64-unknown-linux-gnu// Go package main import ( "fmt" "sort" "strconv" ) type T …
C言語後方互換性 TerraはClangの機能を使って、C言語との後方互換性を実現しているので、C言語から使えるライブラリならTerraからも使うことができる。 試しにTcl/TkをTerraから使ってみる。 libtcl = "libtcl8.5.so.0" libtk = "libtk8.5.so.0" includepath…
実行時コンパイル LuaからTerraの関数を呼べるし、TerraからLuaの関数を呼べる。 -- hello2.t stdio = terralib.includec("stdio.h") function hello_lua() print("Hello from Lua!") end terra hello_terra() stdio.printf("Hello from Terra!\n") end terr…
今年5月ごろに公開されて、Twitterではちょっとは流れてきたのだけれども、日本語の情報が全然流れないままのTerraという言語があって、ちょっと気が向いたのでもう一度調べてみることにした。Terra どんな言語なのか 説明によれば、TerraはLuaと同時に使え…
Go言語でEitherモナドは無理がありすぎる感じがした。では、他の言語ではどうだろうか? C言語では関数の戻り値でエラーかどうかを判定しなければならないことが多いわけですけど、&&演算子の短絡評価を使えば、簡潔にこのように簡潔に書くことさえ可能だ。 #…
Goとerror monads - moriyoshiの日記ちょっとそれをモナドって呼んだらHaskellerやってきますよ? (太宰メソッド) こういうふうにやらないとモナドを使ったとは認めません。 package main import ( "log" "os" ) type right struct { val interface{} } typ…
Idrisみたいに、函数プログラミングを前提にしている言語には函数を合成する演算が標準で用意されているよね。 (.) : (b -> c) -> (a -> b) -> a -> cこの演算子を使うと、函数を合成してくれる。函数の合成を使えば、プログラムを変数を使わないで書くこと…
帰納と余帰納 制限された再帰 Idrisには函数が全域函数であるかチェックする機能があるのだけれども、プログラムに制限なく再帰が使われていると、その函数が値を返すのか、それとも停止しないで値が返らないままなのか判定する方法が存在し得ない。そこで、…
表明から証明へ (3) headを証明する HaskellのPrelude.headとは異なり、IdrisのPrelude.List.headは、引数にコンスセルである証明をとるので、全域函数になっている。Idrisのシステムでは次のように、%assert_total宣言によって、全域函数であることが「表明…
表明から証明へ (2) 型と命題 カリー゠ハワード同型対応により、プログラムと証明が対応すると述べた。実際にはどのように対応しているのだろうか? 実は、恒真である命題は、空でない(その型である値を持つ)型に対応しているのだ。 型と命題の対応関係を見…
表明から証明へ 表明とテスト バグの原因のひとつとして、プログラム実行時に守るべき条件が守られていないことが挙げられるだろう。プログラムが一体どのような場合に正常に動作し、どのような場合に望まない結果をもたらすのかが分かっていなければ、バグ…