由于类型在 Idris 中是一等的,因此我似乎应该能够编写一个 typeOf
函数来返回其参数的类型:
typeOf : a => a -> Type
typeOf x = a
但是,当我尝试调用此函数时,我收到了看起来像错误的信息:
*example> typeOf 42
Can't find implementation for Integer
我怎样才能正确实现这个typeOf
函数?或者对于我所缺少的“获取值的类型”的想法是否有一些更微妙的东西,这会阻止这样一个函数的存在?
最佳答案
这样写:
typeOf : {a : Type} -> a -> Type
typeOf {a} _ = a
a => b
是一个函数,它具有由接口(interface)解析填充的隐式参数。 {a : b} -> c
是一个带有通过统一填充的隐式参数的函数。
这里不需要引用接口(interface)。每个术语都有一个类型。如果您编写 typeOf 42
,隐式 a
将通过统一推断为 Integer
。
关于function - 如何实现 typeOf 函数?,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/45260598/