dependent-type - 在Idris中进行秩N量化

Question

我只能以一种相当笨拙的方式在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。

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

Answer 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 ()

目前的主要限制是您不能直接为隐式参数提供值，除非在顶层。我最终会为此做些...