在Idris中进行n阶量化

Question

在Idris 0.9.12中，我只能以相当笨拙的方式实现排名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函数用作类型的同义词，例如在Haskell中的Lens s t a b = forall f. Functor f => (a -> f b) -> s -> f t。有什么解决或规避上述问题的方法吗？

- András Kovács

---

这在我的待办事项清单上——通常情况下，如果有人询问，这件事就会被提升到待办事项清单的更靠前位置，因此提问是帮助解决问题的一种方式：）。令人惊讶的是，实际上并没有太多这方面的需求，尽管显然这将是不错的。正确地获取隐含参数有一些技巧性，所以我们现在采取了比较简单的方法。类型类是第一类对象，因此也有一种笨拙的方法来处理类约束——将它们视为普通函数参数，并使用“％instance”显式查找实例。 - Edwin Brady

@EdwinBrady 谢谢，我接受这个作为答案（如果它是一个答案的话，我会这么做）。 - András Kovács

还不像是一个合适的答案...希望很快能给你回复！ - Edwin Brady

我的谷歌小组问题第四部分与这个SO问题类似，为未来读者进行交叉链接。 - Davorak

Answer 1

我刚刚在主分支中实现了这个功能，允许在任意作用域中使用隐式参数，并且它将在下一个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 ()

目前的主要限制是您无法直接为隐式参数赋值，除非在顶层。我最终会对此采取措施...

- Edwin Brady

---

类型类也会发生吗？ - dfeuer