function - 如何实现 typeOf 函数?

标签 function types idris first-class

由于类型在 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/

相关文章:

c# - 创建一个抽象函数,它根据继承者接受不同的参数

c - 从文件扫描时如何使用结构实现堆栈

c++ - 在 C++ 中循环定义函数的参数

implicit - GADT 数据构造函数参数在 Idris 中如何工作?

dictionary - Idris 中字典/ map 的类型是什么

JavaScript 获取有单词的天数,比当前日期提前 5 天

postgresql - column1 的索引 = x AND column2 <= y ORDER BY column3 DESC

java - 可以通过 Java 泛型类型系统强制执行自然排序吗?

java - 如何设置列表的引用类型?

dependent-type - Idris:有界 double 的算术