6

我只阅读了标准教程并且摸索了一下，所以我可能会遗漏一些简单的东西。

如果这在 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，那么有什么问题呢？我尝试将Natsv''替换为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

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

4

3 回答 3

8

正如其他答案所解释的，这是关于变量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参数不存在然而，当我最初实现类型类时。

于 2014-07-19T10:24:52.717 回答
2

你可以写

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

v'' : List Nat
v'' = emptyListOfOrds

或者，如果您愿意

 v'' = emptyListOfOrds {t = Nat}

如果您按照您编写的方式询问 emptyListOfOrds 的类型，您会得到

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

打开:set showimplicitsrepl，然后再次询问

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

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

于 2014-07-19T07:52:58.993 回答
0

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

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

于 2014-07-19T07:58:07.230 回答