Reflection in Agda

今回のAgdaミーティングが何かプログラミングするのは知ってたんですが、何かは特に決めずに。なので、いきなり聞かれて少し困りました。

今まで、Agda詰まったところ、System F とか Yoneda functor のembededness とかも聞いたんだけど、まぁ、解決せず。

System F でうまく動かないのは、

　　Int : {l : Level } ( X : Set l ) → Set l
　　Int X = X → ( X → X ) → X

　　Zero : {l : Level } → { X : Set l } → Int X
　　Zero {l} {X} = λ(x : X ) → λ(y : X → X ) → x

　　S : {l : Level } → { X : Set l } → Int X → Int X
　　S {l} {X} t = λ(x : X) → λ(y : X → X ) → y ( t x y )

で、Int をコピーするところ。

　　copy_int : {l l' : Level } { X X' : Set l } → Int (X → (X → X) → X) → Int X
　　copy_int {_} {_} {X} {X'} x = It Zero S x

これがだめ。

　　copy_int : {l l' : Level } { X X' : Set l } → Int X → Int X'

であるべきなんですけどね。なので、

　　Prolog の copy_term 作れば良いんじゃね?

と思っていて、Haskell の関数でも書けば良いだろと思っていたんですが、

　　Agda の FFI (Foreign Function Interface)は compile 時にしか動かない

おいおい。なので、それは使い物ならない。その替わり、Reflection がいけそう。

取りあえず、変数の数を数えるmacroを作ってみました。macroで Agda の項の構文木が取れる。

　　macro
　　　　varlist : Term → Term → TC ⊤
　　　　varlist term hole =
　　　　　 unify hole ( to-term ( varlist1 term [] ) )

必ず TC Monad (Type Checer ) を返さないといけないらしい。

　　to-term : List ℕ → Term
　　to-term [] = con (quote List.[]) []
　　to-term (h ∷ t) = con (quote List._∷_)
　　　　　　　　　　 ( arg (arg-info visible relevant ) (lit (nat h ))
　　　　　　　　　∷　( arg (arg-info visible relevant ) (to-term t) )
　　　　　　　　　∷ []　)
　　　　　
　　varlistArgs : List (Arg Term ) → List ℕ → List ℕ

　　varlist1 : Term → List ℕ → List ℕ
　　varlist1 (var n args ) vars =　( n　∷ vars )
　　varlist1 (con c args) vars =　 varlistArgs args vars
　　varlist1 (def f args) vars =　varlistArgs args ( 11 ∷　vars )
　　varlist1 (lam v (abs s x)) vars = varlist1 x vars
　　varlist1 (pat-lam cs args) vars = varlistArgs args vars
　　varlist1 (pi a b) vars =　vars　
　　varlist1 (agda-sort s) vars =　vars　
　　varlist1 (lit l) vars = vars
　　varlist1 (meta x args) vars =　varlistArgs args vars
　　varlist1 unknown vars =　vars

　　varlistArgs [] vars = vars
　　varlistArgs (arg i x ∷ rest) vars =
　　　　varlistArgs rest ( varlist1 x vars )

こんな感じ。何故か ( 11 ∷　vars ) ってのを入れないと黄色くなるんですが、理由は不明。

vvar n args が変数なので、それを数えれば良いだけですね。copy_term までは、まだ、距離があるが、今回の成果はこんなものです。