Idris函数构造空`List a`,其中`a`绑定到`Ord`的实例？

Question

我只阅读了标准教程并且稍微摸了一下,所以我可能会遗漏一些简单的东西.

如果在Idris中无法做到这一点,请解释原因.此外,如果可以用另一种语言完成,请提供代码示例并解释有关该语言类型系统的不同之处.

这是我的方法.问题首先出现在第三部分.

创建已知类型的空列表

 v : List Nat
 v = []

这在REPL中编译并表现为[] : List Nat.优秀.

推广到任何提供的类型

 emptyList : (t : Type) -> List t
 emptyList t = []

 v' : List Nat
 v' = emptyList Nat

不出所料,这是有效的v' == v.

将类型约束到Ord类的实例

emptyListOfOrds : Ord t => (t : Type) -> List t
emptyListOfOrds t = []

v'' : List Nat
v'' = emptyListOfOrds Nat     -- !!! typecheck failure

最后一行失败,出现此错误:

When elaborating right hand side of v'':
Can't resolve type class Ord t

Nat是一个例子Ord,那么问题是什么？我试图取代Nat以s v''与Bool(不是实例Ord),但有错误没有变化.

另一个角度......

使Ord t显式参数满足类型检查器吗？显然不是,但即使它确实要求呼叫者传递冗余信息也不理想.

 emptyListOfOrds' : Ord t -> (t : Type) -> List t
 emptyListOfOrds' a b = []

 v''' : List Nat
 v''' = emptyListOfOrds (Ord Nat) Nat     -- !!! typecheck failure

这次错误更详细:

 When elaborating right hand side of v''':
 When elaborating an application of function stackoverflow.emptyListOfOrds':
         Can't unify
                 Type
         with
                 Ord t

         Specifically:
                 Can't unify
                         Type
                 with
                         Ord t

我可能错过了一些关于如何根据类型声明检查值的关键见解.

Answer 1

正如其他答案所解释的那样,这是关于变量t绑定的方式和位置.也就是说,当你写:

emptyListOfOrds : Ord t => (t : Type) -> List t

详细说明者将看到't'在其使用时未Ord t绑定,因此隐式绑定它:

emptyListOfOrds : {t : Type} -> Ord t => (t : Type) -> List t

所以你真正想说的是有点像:

emptyListOfOrds : (t : Type) -> Ord t => List t

哪个会在类型类约束之前绑定t,因此它Ord t出现在范围内.不幸的是,不支持此语法.我认为没有理由不支持这种语法,但目前并非如此.

你仍然可以实现你想要的东西,但它很难看,我担心:

由于类是第一类,您可以将它们作为普通参数给出:

emptyListOfOrds : (t : type) -> Ord t -> List t

然后,您可以使用特殊语法%instance在调用时搜索默认实例emptyListOfOrds:

v'' = emptyListOfOrds Nat %instance

当然,您并不是真的想在每个调用站点执行此操作,因此您可以使用默认隐式参数来为您调用搜索过程:

emptyListOfOrds : (t : Type) -> {default %instance x : Ord t} -> List t
v'' = emptyListOfOrds Nat

如果没有明确给出其他值,default val x : T语法将x使用默认值填充隐式参数val.给予%instance作为缺省则是相当多到什么与阶级局限时会发生相同的,实际上我们很可能改变的执行Foo x =>语法,做的正是这个......我觉得我做得不是唯一的原因是,default论据不存在但是当我首先实现类型类时.