full-sessions を hackageDB にアップロードしました！
初回に， Sessionモナドは indexed monad だと説明しましたが具体的にどういう制約が入っているのかをちゃんと説明しませんでした． すべてを一度に説明するのは難しいのですが，とりあえずおおざっぱに説明を試みます 事前条件・事後条件 と プロトコルの差…
セッション型の読み方について説明します． セッション型の種類 私のfull-sessionsにおけるセッション型を次のTable 2に示す： セッション型は論文によって表記法が著しく異なるが，多かれ少なかれだいたいここで示した機能(と再帰)がすべてである． Send / …
セッション型を備えた 「型付きErlang」みたいなのがあればいいのになあ、と思うんですが(ある？)、一から型推論やら多相性やらを作り上げるのは面倒でしょうしHaskellやMLよりも便利で安全な型システムなんてあろうはずもないので(ぉぃ)、私たちはHaskellで…
セッション型のような型は，関数型言語の型システムでは作れないのが普通だ．しかしながらセッション型の機能の一部を関数型言語で実現しようとする試みはいくつか存在する． つい最近では， Kiselyov, Peyton Jones, Shanの Fun with type functions のよう…
セッション型は プロトコルを表現する型で， 15年くらい前から π計算の型理論の1つとして研究されてきました(文献リスト(一部))．並行・分散ソフトウェアの普及を鑑みるに，セッション型のような仕組みは次世代の型安全かつ表現力の高いプログラミングのため…
# トラックバックをバラまいてしまいました m(_ _)m スミマセン…型レベルプログラミング会議 に行ってきました。 帰りの新幹線でこれを書いています。随時更新予定。 私の発表 最後の TCast がメインなのですがそれはソース参照 スライド1とHaskellソース ht…
sumiiさんの記事によれば，どうも私は [お勉強]とタグをつけたのをいいことにデマを振りまいていたようなので訂正しました．型付きλ計算の型でcharacterizeしてるから論理的，というのなら，正直 Curry-Howard同型による，という説明でもそれほど間違ってな…
Windows Server の話． 背景 ActiveDirectory は LDAP プロトコルで認証できる． LDAPでは， CN=hogehoge,OU=foobar,... という形(DN)で エントリを一意に指定する． 現象 某F社検疫が通らない 原因 Windows の 「ActiveDirectory ユーザとコンピュータ」か…
ATTAPL続き． 論理関係とは 論理関係は λ計算の項の間の2項関係で, 型でインデックスがついている(つまり型を含めれば3項関係). 論理関係は「論理的」な関係である(Curry-Howard的な意味で). すなわち，論理関係とは R(s1, t1, T1->T2) かつ R(s2, t2, T1) …
ATTAPLの6章は 論理関係という方法を使ったプログラムの等価性検査について書いてある．6.3節では, 前準備として, 基本型がプログラムの等価性に影響を与える場合について述べている．ここではλ計算にUnit型を入れてプログラムの等価性を議論している. Unit…
ここ読んでいる人で知らない人はいないと思いますが、 型レベルプログラミングの会 というものが開催される予定で、 既に満員で、場所も決まっていて、すごい感じです。 いろいろとすごい人とか一度会ってみたかった人とかPPLでお世話になった人とかがいらっ…
ぜひやりたいですね！ ただ、私は他の言語で何ができるのかイマイチ私はよくわかってないのですが そんな界隈が(国内で？)存在しうるという時点ですごい。開催地は普通に東京が良いんでしょうねえ。
マジメな話は省略、主に自分の話だけメモ飲み会は2日目だけ参加しました。 kinabaさん→id:osiire さん、 「リストの重複を省く関数(多相的)を作るときに Setモジュールが使えない」 OCaml の Set モジュールが多相的に使えない問題。 let uniq xs cmp = let …
π計算の型に セッション型というのがあって、そいつを Haskell上に実装して PPL2009 で発表しました。 ソースコードはこちら 発表論文はこちら 質問 なぜ Associated Types や Type Families ではなく Functional Dependencies か？ 他の言語に応用可能か？ …
背景 MacPorts は、 OCaml周りのいろんなライブラリのダウンロード・ビルド・インストールを "port install パッケージ名" 一発でこなしてくれる。 Findlib に、 OCaml のライブラリを登録しておけば、 "ocamlfind ocamlc -package パッケージ名" で パッケ…
Alloyを使ってみた。 数年前に使ったときはなんでこんなの使うのと思っていたけど考えが変わったのだ。 ちょっとした規模のプログラムを書くには設計が必要だ。 コードを書く前に、問題の本質的な部分を知っておこう。 本質がわかっていれば、 適切な部分に…
FAQだろうけど、 crontabの話 crontab の標準出力を 日付入りファイル名で保存 30 2 * * * pdumpfs /backups/latest /backups >/backups/backup-`date '+%Y%m%d%H%M'`.txtという crontabを書いた。 2時30分に pdumpfsを起動し、 その標準出力を backup-20090…
ほとんどカスタマイズしないんですがこれだけはなぜかやっている。 ジャンクションを使って Documents and Settings とか デスクトップ とか My Documents の別名を作成してそれを使う。 特に日本語フォルダ名が化けたり、空白を含むパスをうまく扱えないツ…
絶賛現実逃避中。先のエントリ PHOAS - Parametric Higher Order Abstract Syntax - を Haskellで - keigoiの日記 は phantom typeやら GADTやらを含んでいてわかりにくかったので もっと簡単にした FOAS {-# LANGUAGE FlexibleInstances #-} import Control…
GADTは証拠みたいなもの(というか証明)なので この証拠さえあれば 型を存在限量で隠蔽しても パターンマッチングで復元できてしまうのであった。 コード {-# LANGUAGE GADTs #-} {-# LANGUAGE ExistentialQuantification #-} {-# LANGUAGE KindSignatures #-…
当該タイトルの論文は http://dx.doi.org/10.1145/1411203.1411226 論文では Coqで書いてあるが、同じことが Haskell (+GADT) でもできるようで、Haskell-cafe に投稿されていた： http://www.mail-archive.com/haskell-cafe@haskell.org/msg48913.html HOAS…
と、自分でも何を言ってるのか分からねーですが、タイトルに継続と書けばとアクセス数とブクマが増えるのでそう書く(←最低)。あながち遠くはないはずだけどOCamlでHaskellのforall を使うような存在型を直接書く事はできないらしい。 そこで #002 存在型 - K…
2008-12-23 で思い出したのですが、 strtotime('now + seconds') という式でハマったことがあります。 コード
型レベル計算で、zipWith をやりたい。 ちなみに zipWith :: (a -> b -> c) -> [a] -> [b] -> [c] で、まあそういう関数だ。しかし まともに使える関数を作るには、陽に型を指定せずとも型が推論されてくれないと困る。そこで zipWithに渡す関数の種類を、引…
型レベルの数値と、引き算Sub, 型レベルのconsリスト、リストの長さを求める型クラスLengthと関数length_tを定義する。 data S n data Z class Sub n n' n'' | n n' -> n'' instance Sub n Z n instance Sub n n' n'' => Sub (S n) (S n') n'' class Length …
やってみた 訂正: id:athos くんの指摘により。 やりたいこと 木を深さ幅優先探索して n 番目の要素を取得する。 関数型言語でならこんな風に継続渡し形式(CPS)で書けばよい： data Tree a = Tree a :*: Tree a | Leaf a nth :: Int -> Tree a -> a nth n t …
htree は柔軟というかpermissiveだと謳われているのでスクレイピングにはちょうどよさげ。 hpricotは全然xpathをサポートしていなかったのでこのhtree+rexmlを使う。 require "rexml/document" require 'htree' doc = HTree('<div><p>abc</p><div><p>def</p><p>ghi</p></div><p>jkl</p></div>').to_rexml names …
htreeはxmlやhtmlをparseするための rubyのライブラリらしい。 ruby install.rb とやったらば、 install.rb:19:in `target_directory': could not find target install directory (RuntimeError) となってこけた。ruby初心者なのでよくわからないけど、 def …
REXMLのXPathを使ってみたが、今のところあまり使えない。作者いわく： Some of the XPath functions are untested8. Any XPath functions that don't work are also bugs... please report them. If you send a unit test that illustrates the problem, I'…
