HOASによるラムダ式

30分プログラム、その691。HOASによるラムダ式。
id:keigoiさんに、HOAS(Higher order abstract syntax)なるものを教えてもらいました。
詳しいことは、http://homepages.inf.ed.ac.uk/ratkey/unembedding.pdfに書いてあるらしいです。

今のところの理解は、

• Haskellのラムダ式で、ターゲット言語のラムダ式を表現する
• アルファ変換とか変数補足とかを考えなくてすむ

といった感じです。

さっぱり分からないので、上記の論文にのっている例を実装してみました。

使い方

*Main> eval (lambda (\x->x) `apply` (int 42))
42

ソースコード

{-# OPTIONS_GHC -fglasgow-exts #-}

import Text.Printf
class Lambda exp where
    int :: Int -> exp
    lambda :: (exp -> exp) -> exp
    apply  :: exp -> exp -> exp

type Hoas = forall exp. Lambda exp => exp

example1 :: Hoas
example1 = int 42

example2 :: Hoas
example2 = lambda (\x->x) `apply` int 42

data Value = VFunc (Value->Value) | VInt Int

instance Show Value where
    show (VInt n) = show n
    show _ = error "can not show"

instance Lambda Value where
    int n = VInt n
    lambda f = VFunc f
    apply (VFunc f) y = f y

eval :: Hoas -> Value
eval term = term

参考

• 過去の30分プログラム
• http://homepages.inf.ed.ac.uk/ratkey/unembedding.pdf