Is it possible to create a "quote" function that, given a native λ-term, returns its λ-encoded representation? Suppose we implement the λ-calculus inside the λ-calculus itself with λ-encodings and Bruijn indices:

Lam = λ body .        λ Lam . λ App . λ Var . Lam body
App = λ fun . λ arg . λ Lam . λ App . λ Var . App fun arg
Var = λ idx .         λ Lam . λ App . λ Var . Var idx


Is it possible to implement a quote() function that, given a native term, returns its own λ-encoded representation? For example:

quote(λ f . λ x . f (f x)) 


Would return:

Lam (Lam (App (Var 1) (App (Var 1) (Var 0))))


If not, is it possible if given a type?

quote(Arr(Arr(T,T),Arr(T,T)), λ f . λ x . f (f x)))


Where Arr(Arr(T,T),Arr(T,T)) represents that the term we want to quote has the following STLC type: (o -&gt; o) -&gt; o -&gt; o.
No, this is not possible, assuming you want to go from an arbitrary lambda term to some first-order AST. 

The lambda calculus is extensional, which means that the lambda calculus cannot distinguish between two lambda-terms which are behaviourally equivalent. Eg, if you have terms implementing quick sort and merge sort, then no other lambda-term can distinguish them, since they are both extensionally the same function. As a result, full quotation is impossible, since it should let you get different source code for those two terms.