日々の流転

λ. 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を使った領域理論的な記述へと変換しているので、扱いは面倒だけど、停止しない関数が拒絶されるといった問題は無い。