测试类型是否是Idris中的函数类型

Question

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

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

但是,这会返回True所有输入.我怎样才能做到这一点？

Answer 1

匹配类型称为类型套管.能够做到这一点将打破一个称为参数化的概念,这是非常有价值的.

伊德里斯不支持类型套管.我认为它可能在一个阶段尝试过,但人们很快就放弃了.它还用于在尝试使用类型套管时出错,但检查导致了错误,因此现在已禁用.

虽然你没有得到任何的错误越多,你不能提供一个实现Type -> Bool将不同的工作const True或const False.

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