dependent-type - 在 Idris 中测试类型是否为函数类型

Question

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

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

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

score 8 · Accepted Answer

Type 上的匹配称为type-casing。能够做到这一点将打破一个非常有价值的称为参数化的概念。

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

虽然您不再收到错误，但您无法提供与orType -> Bool不同的实现。const Trueconst False

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

score 1 · Accepted Answer

这里的问题是：你为什么需要这样的东西？

您是否需要确定任意 Idris 类型是否为函数？还是您只需要从 Idris 类型的特定子集中找出它？我不知道第一个可能的应用程序，但如果它是您需要的第二个，那么您可以定义自己的嵌入式语言来处理这些类型的值，如下所示：

data Ty = TyNat | TyString | TyFun Ty Ty | ...

isFunction : Ty -> Bool
isFunction (TyFun _ _) = True
isFunction _ = False

查看此演讲以获取有关如何实现这些嵌入式语言的更多信息： https ://vimeo.com/61663317

2 回答 2