Since types are first-class in Idris, it seems like I should be able to write a typeOf function that returns the type of its argument:
typeOf : a => a -> Type
typeOf x = a
However, when I attempt to call this function, I get what looks like an error:
*example> typeOf 42
Can't find implementation for Integer
How can I properly implement this typeOf function? Or is there something more subtle about the idea of "getting the type of a value" that I'm missing, which would prevent the existence of such a function?
Write it this way:
typeOf : {a : Type} -> a -> Type
typeOf {a} _ = a
a => b is a function which has an implicit argument filled in by interface resolution. {a : b} -> c is a function with an implicit argument filled in by unification.
There is no need to refer to interfaces here. Every term has a single type. If you write typeOf 42, the implicit a is inferred to Integer by unification.