如何实现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,隐含a是Integer由统一推断的.