This is possibly related to reflection and quoting but I don't want to assume anything beforehand. Here is my requirement.
My typed lambda calculus (Curry style) is a simpler variant of Calculus of Constructions (CoC). Is it possible to write an analyzer (e.g., type checker) that inspects the runtime representation of the term within the calculus? For example, what I want is roughly along the lines of the following:
$\Gamma \vdash Analyzer : \forall \tau. AST~\tau \rightarrow Bool$
where $AST~\tau$ is the type constructor representing the abstract syntax tree of a term with type $\tau$. The expected body of Analyzer is something like below.
Analyzer e = case e of
| Var -> True
| Abs t e' -> Analyzer e'
...
There are two roadblocks for me.
- How to represent AST of $e$ within the same language?
- How can the Analyzer access the intensional structure of the term $e$?
I am reading few papers on reflection and quotation. The details are a bit dense and I am looking for a simpler explanation. I believe I don't require the full complexity of type self-representation here.
If there is an alternate way of accomplishing this, I'll be more than happy to accept it as an answer. For example, it might be possible to stringify the input term $e$. However, the Analyzer still has to iterate through the intensional structure of $e$. Is that possible within the calculus?
