ヒビルテ(2009-05)

(<<) :: [a -> b] -> [a] -> [b]
(f:fs) << (a:as) = f a : (fs << as)
_ << _ = []

zero :: [a] -> [a]
zero = id

succ :: ([b] -> c) -> [a -> b] -> [a] -> c
succ = \n fs as -> n (fs << as)

one = succ zero :: [a -> b] -> [a] -> [b]
two = succ one :: [a -> b -> c] -> [a] -> [b] -> [c]

zipWith :: ([a] -> b) -> a -> b
zipWith n f = n (repeat f)

zipWith2 :: (a -> b -> c) -> [a] -> [b] -> [c]
zipWith2 = zipWith two

あと、(<<) は Applicative ZipList の <*> と同じかな。

Tags: 論文 haskell

本日のツッコミ(全2件) [ツッコミを入れる]

ψ osiire [集いお疲れさまでしたー。モナドの話じゃなくて恐縮ですが「Haskellで飯を食うには」とかの話題って出ました？]

ψ さかい [お疲れ様でしたー。「Haskellで飯を食うには」は「質問への回答の発表資料」に載っている話と、あとは黒田さん的..]

2009-05-05 [長年日記]

λ. Pure Prolog Implementation...なんか (PPIM)

昔読みかけで挫折したwambookを読み返して、ちゃんと理解するのを目標に参加。昔印刷したwambookを本棚から発掘して会場へ向かった。

WAMをきちんと理解しなおすという目的は、m0h1canさんの説明が分かり易かったこともあり、結構果たせたように思う。が、肝心の実装に私はなんだか駄目な感じに迷走してた orz

最初はWAMからLLVMへの変換か何か出来たらいいなぁとか漠然と思ってた。
が、それは置いていて先ずはリファレンスインプリメンテーションが必要だろうということで、wambookを参照しながら、WAM の small step の操作的意味論をHaskellで書く。
しかし、配列操作の山にウンザリする。
面倒になってきて、LLVMのドキュメント読んだり、横道にそれまくる。
気がついたら8時ごろ orz

が、さすがに何も作らなかったというのは悲しすぎるので、最後の一時間と帰りの電車で、超簡単な処理系だけ書いた。Prolog.hs

昨日に続いて今日もustream.tvでストリーミングしてみたんだけど、今日は昨日のような数十分の遅延は発生しなかった。昨日はemobileで今日は無線LANだったからかな。なんにせよ、よかったよかった。

参考

PPIM(0h1cansanKotobazeme)に備えて色々 (Wiki)

Tags: logic-programming haskell

[ツッコミを入れる]

2009-05-06 [長年日記]

λ. Haskell→Isabelle

ranhaさんが書いていた　 Haskabelle*1に少し興味を持つ。 HaskellプログラムをIsabelleに変換するものらしい。マニュアルによると、例えば以下のようなHaskellプログラム

module Classes where

class Monoid a where
  nothing :: a
  plus :: a -> a -> a

instance Monoid Integer where
  nothing = 0
  plus = (+)

-- prevent name clash with Prelude.sum
summ :: (Monoid a) => [a] -> a
summ [] = nothing
summ (x:xs) = plus x (summ xs)

class (Monoid a) => Group a where
  inverse :: a -> a

instance Group Integer where
  inverse = negate

sub :: (Group a) => a -> a -> a
sub a b = plus a (inverse b)

が

theory Classes
imports Nats Prelude
begin
class Monoid = type +
  fixes nothing :: 'a
  fixes plus :: "'a => 'a => 'a"

instantiation int :: Monoid
begin
  definition nothing int :: "int"
  where
    "nothing int = 0"
  definition plus int :: "int => int => int"
  where
    "plus int = (op +)"
instance ..
end

fun summ :: "('a :: Monoid) list => ('a :: Monoid)"
where
"summ Nil = nothing"
| "summ (x # xs) = plus x (summ xs)"

class Group = Monoid +
  fixes inverse :: "'a => 'a"

instantiation int :: Group
begin
  definition inverse int :: "int => int"
  where
    "inverse int = uminus"
instance ..
end

fun sub :: "('a :: Group) => ('a :: Group) => ('a :: Group)"
where
  "sub a b = plus a (inverse b)"
end

というIsabelleの記述に変換されるとか。 Isabelleの構文をきちんと知らないので、良くは分からないけど。

ただ、Haskellのデータ型や関数をIsabelleの普通のデータ型や関数に変換しているため、変換結果はIsabelleに停止しない関数として拒絶されることがあるそうだ。 (その辺りはどうしているのかなぁ、と思ったら案の定)

調べてみると、HaskellからIsabelleへの変換の試みは他にもいくつかあるみたいだな。 Implementation of a Pragmatic Translation from Haskell into Isabelle/HOL はHaskabelleと同じくそのまま単純に変換している。一方、Paolo Torrini, Christoph Lueth, Christian Maeder, Till Mossakowski. Translating Haskell to Isabelle は、Isabelle用の領域理論のライブラリであるIsabelle/HOLCFを使った領域理論的な記述へと変換しているので、扱いは面倒だけど、停止しない関数が拒絶されるといった問題は無い。

Tags: haskell theorem-proving

*1 綴りが難しいよ (＞＜)

[ツッコミを入れる]