在 Idris 中进行 rank-n 量化答案

【问题标题】：Doing rank-n quantification in Idris在 Idris 中进行 rank-n 量化
【发布时间】：2014-05-17 19:13:04
【问题描述】：

我只能以相当笨拙的方式在 Idris 0.9.12 中进行 rank-n 类型：

tupleId : ((a : Type) -> a -> a) -> (a, b) -> (a, b)
tupleId f (a, b) = (f _ a, f _ b)

只要有类型应用程序，我就需要下划线，因为当我尝试将（嵌套）类型参数设为隐式时，Idris 会引发解析错误：

tupleId : ({a : Type} -> a -> a) -> (a, b) -> (a, b) -- doesn't compile

一个可能更大的问题是我根本无法在更高级别的类型中进行类约束。我无法将以下 Haskell 函数转换为 Idris：

appShow :: Show a => (forall a. Show a => a -> String) -> a -> String
appShow show x = show x

这也使我无法将 Idris 函数用作类型的同义词，例如 Lens，在 Haskell 中是 Lens s t a b = forall f. Functor f => (a -> f b) -> s -> f t。

有什么办法可以补救或规避上述问题？

【问题讨论】：

它在我的 TODO 列表中 - 通常如果有人问到它们，事情会在 TODO 列表中移动，所以问这是帮助解决它的一种方法:)。令人惊讶的是，对此并没有太多需求，尽管显然它会很好。正确获取隐式参数有一些技巧，所以我们现在采用了一种非常简单的方法。类型类是第一类，因此还有一种笨拙的方式来进行类约束——将它们视为普通函数参数，并使用 '%instance' 显式查找实例。
@EdwinBrady 谢谢，我接受这个作为答案（或者我会这样做）。
感觉还不是一个正确的答案...希望我会尽快回复您！
我的question on the google group 的第 4 部分类似于这个 SO 问题，为未来的读者交叉链接。

标签： dependent-type higher-rank-types idris

【解决方案1】：

我刚刚在 master 中实现了这个，允许在任意范围内隐式，它将在下一个 hackage 版本中。虽然它还没有经过很好的测试！我至少尝试过以下简单示例，以及其他一些示例：

appShow : Show a => ({b : _} -> Show b => b -> String) -> a -> String
appShow s x = s x

AppendType : Type
AppendType = {a, n, m : _} -> Vect n a -> Vect m a -> Vect (n + m) a

append : AppendType
append [] ys = ys
append (x :: xs) ys = x :: append xs ys

tupleId : ({a : _} -> a -> a) -> (a, b) -> (a, b)
tupleId f (a, b) = (f a, f b)

Proxy  : Type -> Type -> Type -> Type -> (Type -> Type) -> Type -> Type

Producer' : Type -> (Type -> Type) -> Type -> Type
Producer' a m t = {x', x : _} -> Proxy x' x () a m t

yield : Monad m => a -> Producer' a m ()

目前的主要限制是你不能直接给隐式参数赋值，除了顶层。我最终会对此做点什么...

【讨论】：

类型类也会发生吗？