function - 如何实现 typeOf 函数？

Question

由于类型在 Idris 中是一等的，因此我似乎应该能够编写一个 typeOf 函数来返回其参数的类型:

typeOf : a => a -> Type
typeOf x = a

但是，当我尝试调用此函数时，我收到了看起来像错误的信息:

*example> typeOf 42
Can't find implementation for Integer

我怎样才能正确实现这个typeOf函数？或者对于我所缺少的“获取值的类型”的想法是否有一些更微妙的东西，这会阻止这样一个函数的存在？

Answer 1

这样写:

typeOf : {a : Type} -> a -> Type
typeOf {a} _ = a

a => b 是一个函数，它具有由接口(interface)解析填充的隐式参数。 {a : b} -> c 是一个带有通过统一填充的隐式参数的函数。

这里不需要引用接口(interface)。每个术语都有一个类型。如果您编写 typeOf 42，隐式 a 将通过统一推断为 Integer。