问Idris函数用于构造空的` `List‘，其中`a’被绑定到` of‘的实例中？

EN

正如其他答案所解释的，这是关于变量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语法将使用默认值val填充隐式参数x。将%instance设为缺省值与类约束发生的情况基本相同，实际上，我们可能会更改Foo x =>语法的实现，以做到这一点……我认为我没有这样做的唯一原因是，当我开始实现类型类时，default参数还不存在。

你可以写

emptyListOfOrds : Ord t => List t
emptyListOfOrds = []

v'' : List Nat
v'' = emptyListOfOrds

或者如果你愿意

 v'' = emptyListOfOrds {t = Nat}

如果您以您所写的方式要求类型的emptyListOfOrds，您将得到

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

:set showimplicits中的图灵，然后再问一遍

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

似乎指定一个Ord t约束会引入一个隐式t，然后您的显式param t将得到一个新的名称。您始终可以显式地为该隐式参数提供一个值，例如emptyListOfOrds {t = Nat} Nat。如果这是出于某种原因的“正确”行为或限制，也许您可以在github上就此打开一个问题？可能与显式类型参数和类型类型约束有冲突吗？通常情况下，当你的事情被隐式解决的时候.虽然我记得有语法可以获得类型实例的显式引用。

没有答案，只是一些想法。

这里的问题是，(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参数隐含是可能的。