Conor applies reflection in a second way in his article, namely to miniaturize a collection of functions.  In most sensible type theories, one cannot write functions by recursion using pattern matching over the structure of functions.  You can’t say things like, if the first input is a doubly nested lambda-abstraction (like $\lambda x.\lambda y. x$) do one thing, and if it is not, do something else.  The language does not give you the power to analyze functions intensionally in that way.  As an aside, I have to mention that the Archon language I designed a few years back and recently picked up again with Jacques Carette does allow you to do this.  See our short paper recently accepted to PEPM ’12, or the longer earlier paper about Archon.  Back to reflection: if we want to take different action based on the structure of a function, we can apply the same idea of reflection we used for types.  We define a datatype Func, say, where each element has an interpretation as a function belonging to the collection of functions we wish to recurse over.  This interpretation is the semantics for the datatype, and it can be defined within the type theory.  We may need to apply the earlier idea of reflection for types to be able to give a type to the semantics for Func, since otherwise it won’t be clear what the type of [F] should be, for F an element of Func.  Sure, if all the elements of Func were intended to represent functions of the same type X, then we could just define [F] in such a way that it has type X in all cases.  But more likely, we want the elements of Func to represent functions of different types.  Then we might want, for example, to refine our definition of Func somewhat, so that whenever we have F an element of Func, we know what element T of our type universe we want to associate with it.  So we would have F : Func T.  Then our semantics can map elements of Func T to [T].  So [F] : [T], where F : Func T.  This is a very simplistic rendition of this idea, and certainly Conor’s treatment is much more sophisticated.  But this hopefully conveys the basic approach.