How can I implement a typeOf function?

Question

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?

score 8 · Accepted Answer · answered Jul 23 '17 at 09:17

8

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.

answered Jul 23 '17 at 09:17

András Kovács

29,931
3
53
99

Thanks! I must have missed that part of the [documentation](http://docs.idris-lang.org/en/latest/tutorial/miscellany.html#implicit-arguments). – Sam Estep Jul 23 '17 at 11:16
Couldn't it just more simply be written as `typeOf : (a : b) -> Type; typeOf _ = b` – Bruno Gavranovic Apr 20 '19 at 00:57

How can I implement a typeOf function?

1 Answers1