Agda2で遊んでみた

Haskell風構文のDependently Typed Programming LanguageであるAgda2を少し学んでみました。

• The Agda Wiki - Agda

インストールとか

ubuntu intrepidで使う場合、依存ライブラリのうち、zlibとQuickCheckだけは別途makeして入れる必要がありました。あとはdebパッケージですみました。

Adga2のソースをdarcsでとってきて中のREADMEにあるとおりにやれば、ビルドできます。zlibとQuickCheckは/usr/localにinstallで入れました。

ソースコードのファイル名は大文字始まりで、拡張子はagda。

対話環境での実行はIオプションをつけます:

runghc Agda2/src/main/Main.hs -I MySample.agda

対話環境

プロンプトに「:?」でコマンド一覧が出るようです。:typeOfくらいしか使えませんでした。

ビルトインの利用

やり方

• The Agda Wiki - FFI
• The Agda Wiki - Postulates

例:Hello.agda

module Hello where
{-# IMPORT System.IO.Unsafe #-}
data Unit : Set where
  unit : Unit
{-# COMPILED_DATA Unit () () #-}

data List (A : Set) : Set where
  nil : List A
  cons : A -> List A -> List A
{-# COMPILED_DATA List [] [] (:) #-}
{-# BUILTIN LIST List #-}
{-# BUILTIN NIL nil #-}

postulate
  String : Set
  IO : Set -> Set
  putStrLn  : String -> IO Unit
  unsafePerformIO : {A : Set} -> IO A -> A
  _>>=_ : {A B : Set} -> IO A -> (A -> IO B) -> IO B
  return : {A : Set} -> A -> IO A
{-# COMPILED_TYPE String String #-}
{-# BUILTIN STRING String #-}
{-# COMPILED_TYPE IO IO #-}
{-# BUILTIN IO IO #-}
{-# COMPILED putStrLn putStrLn #-}
{-# COMPILED unsafePerformIO (\_ -> unsafePerformIO) #-}
{-# COMPILED _>>=_ (\_ _ -> (>>=) :: IO a -> (a -> IO b) -> IO b) #-}
{-# COMPILED return (\_ -> return :: a -> IO a) #-}

main : IO Unit
main = putStrLn "Hello"

postulateは仮説のこと、この構文によって本体不要の型を定義できます。これらをCOMPILEDプラグマによってバックエンドのHaskellのオブジェクトに結びつけることになります。
読み込むコード中にでも埋めておけば、このプラグマBUILTINによって"abc"のようなリテラルが使えるようになります。

コード全体が正しく記述されていれば、cオプションでHaskellコードにコンパイルでき、mainを実行することができます。

$ runhaskell Agda2/src/main/Main.hs -c Hello.agda
$ ./MAlonzo/Hello
Hello

中途生成されるHello.hsものこるので、プラグマの仕組みはなんとなくわかるかも。

プラグマCOMPILED内のHaskellコード部(最右部分)は、現状そのまま生成コード内に埋め込まれるようで、型判定ミスだけでなく構文ミスでもghcのコンパイルエラーとして表示されます。

とりあえず、ここまで。本題に入るまでが大変だったりするのは、こういうものにはよくあることですが。dependently typed progammingについては明日以降で。