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是一个函数，它有一个由接口解析填充的隐式参数。{a : b} -> c是一个带有由统一填充的隐式参数的函数。

此处无需提及接口。每个术语都有一个类型。如果您写，则通过统一推断出typeOf 42隐式。aInteger