构造空的' 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的一个实例，那么问题是什么?我尝试用Bool(不是Ord的实例)替换v''中的Nat s，但错误没有变化。

另一个角度…

使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

当你调用emptyListOfOrds时，你可以使用特殊的语法%instance来搜索默认实例:

v'' = emptyListOfOrds Nat %instance

当然，您并不想在每个调用站点都这样做，因此您可以使用默认的隐式实参来为您调用搜索过程:

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

如果没有显式给出其他值，default val x : T语法将用默认值val填充隐式参数x。将%instance作为默认值，那么与类约束发生的情况几乎相同，实际上我们可能会改变Foo x =>语法的实现来做到这一点……我认为我没有这样做的唯一原因是default参数还不存在，当我实现类型类的第一。

Answer 2

你可以写

emptyListOfOrds : Ord t => List t
emptyListOfOrds = []
v'' : List Nat
v'' = emptyListOfOrds

或者如果你喜欢

 v'' = emptyListOfOrds {t = Nat}

如果您按照您所写的方式请求emptylistfords的类型，您将得到

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

在repl中的:set showimplicits上图灵，然后再次询问给出

{t : Type} -> Prelude.Classes.Ord t => (t2 : Type) -> Prelude.List.List t2

似乎指定Ord t约束引入了一个隐式参数t，然后您的显式参数t被分配了一个新名称。您总是可以显式地为隐式参数提供一个值，例如emptyListOfOrds {t = Nat} Nat。如果这是"正确"的行为或限制出于某种原因，也许你可以打开一个问题关于这个github?也许与显式类型参数和类型类约束有一些冲突?通常，类型类用于隐式解决问题时…

Answer 3

不是答案，只是一些想法。

这里的问题是(t : Type)引入了向右扩展的新作用域，但Ord t在这个作用域之外:

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

您可以在引入类型变量后添加类约束:

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

但是现在你需要显式地指定类实例:

instance [natord] Ord Nat where
  compare x y = compare x y
v'' : List Nat
v'' = emptyListOfOrds Nat @{natord}

也许可以使Ord t参数隐式