Haskell
セッション型を備えた 「型付きErlang」みたいなのがあればいいのになあ、と思うんですが(ある？)、一から型推論やら多相性やらを作り上げるのは面倒でしょうしHaskellやMLよりも便利で安全な型システムなんてあろうはずもないので(ぉぃ)、私たちはHaskellで…
セッション型のような型は，関数型言語の型システムでは作れないのが普通だ．しかしながらセッション型の機能の一部を関数型言語で実現しようとする試みはいくつか存在する． つい最近では， Kiselyov, Peyton Jones, Shanの Fun with type functions のよう…
セッション型は プロトコルを表現する型で， 15年くらい前から π計算の型理論の1つとして研究されてきました(文献リスト(一部))．並行・分散ソフトウェアの普及を鑑みるに，セッション型のような仕組みは次世代の型安全かつ表現力の高いプログラミングのため…
# トラックバックをバラまいてしまいました m(_ _)m スミマセン…型レベルプログラミング会議 に行ってきました。 帰りの新幹線でこれを書いています。随時更新予定。 私の発表 最後の TCast がメインなのですがそれはソース参照 スライド1とHaskellソース ht…
マジメな話は省略、主に自分の話だけメモ飲み会は2日目だけ参加しました。 kinabaさん→id:osiire さん、 「リストの重複を省く関数(多相的)を作るときに Setモジュールが使えない」 OCaml の Set モジュールが多相的に使えない問題。 let uniq xs cmp = let …
π計算の型に セッション型というのがあって、そいつを Haskell上に実装して PPL2009 で発表しました。 ソースコードはこちら 発表論文はこちら 質問 なぜ Associated Types や Type Families ではなく Functional Dependencies か？ 他の言語に応用可能か？ …
絶賛現実逃避中。先のエントリ 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…
型レベル計算で、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 …
前回の OCaml-Nagoyaで Haskellの遅延評価とvalue recursionを使ったネタの記事を紹介したら皆けっこうおもしろがってくれた。 で、OCaml や SML といった 遅延評価モジュールがある言語ではどう書く？ というネタで さらに少し盛り上がった。rp_min は lazy…
気をとりなおして。 Haskell用の C言語のパーザライブラリ Language.C の意味解析機能を使ってみる。まずはグローバルスコープのシンボルテーブルを表示してみる。 こんなことができる 入力 (sample.c) enum enum1 {x, y, z}; void fundec1(); struct st1 { …
jhcが生成した手元のコードを gcc 2.95でコンパイルするにはもうひとつ障害があった．JHCはサンクを以下の構造体で管理するようだ： typedef struct node { fptr_t head; sptr_t rest[]; } A_MAYALIAS node_t; typedef struct dnode { what_t what; sptr_t r…
Language.CはHaskell用の、C言語のソースコードを構文解析するライブラリである。 Language.CはパーザとともにC言語の構文木に相当するデータ型を提供しており、C言語のソースコードをHaskellのデータとして操作可能である。このため、Language.CはC言語のコ…
存在型+型クラスでduck typing. 参照：http://www.haskell.org/haskellwiki/Existential_type 既に言及されてますが、このやり方だとHaskellはnonintrusive-explicit-dynamic に該当しますね。 テーブル修正しました。 class Duck a where quack :: a -> IO …
と におけるColって同じと違うのか…？ちゃんと勉強しなおさないと...
Strongly typed heterogeneous collectionsの論文では、Haskellの型クラスで使える種々のテクニックが解説されている。なかでも、型クラスTypeCastで型推論の向きをプログラマが指定する(type improvement)というテクニックがとてもおもしろい (8節の直前)。…
これ、バグといっていいのかどうか．Hugsで class TypeCast a b | a->b, b->a where typeCast :: a->b instance TypeCast a a where typeCast = id class Col' a b where inCol' :: a -> b instance TypeCast a b => Col' a [b] where inCol' x = [typeCast …
まずは元論文にもある リストの appendを限定継続で書く例。この時点でついて行けてなかった。実はOlegさんのソースにもあるのだけど自分で書き直してみる。 -- -fno-implicit-prelude を指定すること (GHC 6.6) import ShiftResetGenuine import Prelude hi…
GHC で -fno-implicit-prelude オプションを与えると do記法を再定義できる。 上の Delimited Continuationをdo記法で書いてみた。 こんな感じかなあ {- ghciかghcに -fno-implicit-prelude (GHC6.6以前?) か -XNoImplicitPrelude (GHC6.8以降?) を指定する…
限定継続フェスタ があると聞きまして，私もちょっぴり勉強しています。 Schemeには馴れていないし、僕のPCには処理系も入ってないので、Haskellでやります。Olegさんの投稿 (http://www.mail-archive.com/haskell@haskell.org/msg20758.html ) から、Haskll…
import Control.Monad.State ten = [0..9] getNum :: StateT [Int] [] Int getNum = StateT $ ?ns -> do{n <- ns; return (n, filter (n/=) ns)} sendmory = do s <- getNum if s==0 then lift [] else return () m <- getNum if m==0 then lift [] else ret…
(追記： http://haskell.g.hatena.ne.jp/nobsun/20061019/alphametic のほうがとてもスマート。) ten = [0..9] getNum :: [Int] -> [(Int,[Int])] getNum ns = do{n <- ns; return (n, filter (n/=) ns)} sendmory l0 = do (s,l1) <- getNum l0 if s==0 then…
名大では、学部生向けのocamlの授業が (情報工学コースではなく) 理学部数学科であるらしい (しかしセミナーとかぶっていて見に行けないので伝聞)。 そこで今日出た演習問題： S E N D + M O R E ---------- M O N E Y (S,M != 0)S,E,N,D,M,O,R,Yはユニーク…
