dependent-type - 测试一个类型是否是 Idris 中的函数类型

Question

我想要一个函数来确定一个类型是否是一个函数类型，如下所示:

isFunction : Type -> Bool
isFunction (a -> b) = True
isFunction _ = False

这将返回 True但是，对于所有输入。我怎样才能使这项工作？

Answer 1

匹配类型称为类型套管。能够做到这一点将打破一个非常有值(value)的称为参数化的概念。

https://stackoverflow.com/a/23224110/108359

Idris 不支持类型大小写。我认为它可能在某个阶段尝试过，但人们很快就放弃了。它也曾经在尝试类型转换时出错，但检查导致错误，因此现在已被禁用。

虽然您不再遇到错误，但您无法提供 Type -> Bool 的实现。这与 const True 的工作方式不同或 const False .

很抱歉，此功能不可用。这听起来像是一个限制，但每次我认为我有一个类似于此的功能的动机时，我最终发现我可以用更明确的方式来构建我的程序。