是否有可能使用Agda中的PHOAS来标准化仿射λ演算项？

Question

在Agda中,可以使用PHOAS方便地表示λ项:

data Term (V : Set) : Set where
  var : V ? Term V
  abs : (V ? Term V) ? Term V
  app : Term V ? Term V ? Term V

这种方法比Bruijn指数有几个好处,如"机械化语义的参数高阶抽象语法"中所述.据我所知,不能有一个eval : ? {V} -> Term V -> Term V函数,给定一个λ项,返回其正常形式 - 毕竟,Agda是完全的,而λ演算不是.但我想知道是否有可能eval为仿射λ项编写这样的函数; 即,绑定变量最多出现一次的那些.这种语言显然是完全的.