如何实现 typeOf 函数？答案

【问题标题】：How can I implement a typeOf function?如何实现 typeOf 函数？
【发布时间】：2017-12-28 20:37:38
【问题描述】：

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

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

但是，当我尝试调用这个函数时，我得到了一个看起来像错误的东西：

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

我怎样才能正确地实现这个typeOf 函数？ 或者我缺少的“获取值的类型”的想法有什么更微妙的东西，这会阻止存在有这样的功能吗？

【问题讨论】：

【解决方案1】：

这样写：

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

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

此处无需提及接口。每个术语都有一个类型。如果写typeOf 42，则隐含的a统一推断为Integer。

【讨论】：