How can I implement the typeOf function?
Since the types are first class in Idris, it seems to me that I should write a function typeOf
that returns the type of its argument:
typeOf : a => a -> Type
typeOf x = a
However, when I try to call this function, I get what looks like an error:
*example> typeOf 42 Can't find implementation for Integer
How can I implement this functionality correctly typeOf
? Or is there something more subtle about the "get value type" idea that I am missing that would prevent such a function from existing?
source to share
Write it like this:
typeOf : {a : Type} -> a -> Type
typeOf {a} _ = a
a => b
is a function that has an implicit argument filled with an interface resolution. {a : b} -> c
is a function with an implicit argument filled with unification.
There is no need to refer to interfaces here. Each term is of one type. If you write typeOf 42
, implicit a
is outputted to Integer
by concatenation.
source to share