Reflection by parameter type

Reflection in Idris is a purely compile-time syntactic feature. To predict how this will work, you need to know how Idris converts your program to its primary language. It is important to note that at runtime you cannot retrieve the reflected conditions and restore them as you would with Lisp. This is how your program is compiled:

• Internally, Idris creates a hole that expects something like that Type -> TT
  
  .
• In this state, the proof script for foo
  
  . We start with no assumptions and no type goals Type -> TT
  
  . That is, a term is being built that looks like ?rhs : Type => TT . rhs
  
  . The syntax ?foo : ty => body
  
  shows that there is a hole under the name foo
  
  , the possible meaning of which will be available inside body
  
  .
• The step intro t
  
  creates a function with an argument t : Type
  
  , which means we now have a member like ?foo_body : TT . \t : Type => foo_body
  
  .
• The step then reflect t
  
  fills in the current hole by taking it on the right side and converting it to TT
  
  . This term is really just a reference to a function argument, so you end up with a variable t
  
  . reflect
  
  like all other actions a script only has access to information available directly at compile time. Thus, the result of filling foo_body
  
  with member reflection t
  
  is P Bound (UN "t") (TType (UVar (-1)))
  
  .

If you could do what you want to do here, it will have serious implications both for understanding Idris's code and for using it effectively.

The loss of understanding will stem from the inability to use parametricity to reason about the behavior of functions based on their types. All functions could become potentially ad-hoc polymorphic, as they could (say) behave differently in lists of strings than in lists of int.

The loss in performance depends on providing enough type information for reflection. Once Idris code is compiled, there is no type information in it (unlike a JVM or .NET system or a dynamically typed system like Python, where types have a runtime representation that the code can access). In Idris, types can be very large because they can contain arbitrary programs - this means that much more information needs to be stored, and computations that occur at the type level must also be saved and repeated at runtime.

If you want to think about type structure to further automate compile-time checking, take a look at this tactic applyTactic

. Its argument should be a function that takes a reflected context and target and returns a new reflected tactic script. An example in the sourceData.Vect

.

So, I believe the summary is that Idris cannot do what you want, and he probably never can, but you could have made progress the other way.