依赖型 – 在Idris中进行秩n定量

发布时间：2020-12-14 01:04:05 所属栏目：百科来源：网络整理

导读：我只能在Idris 0.9.12中以一种相当笨拙的方式做排名： tupleId : ((a : Type) - a - a) - (a,b) - (a,b)tupleId f (a,b) = (f _ a,f _ b) 我需要下划线，无论有什么类型的应用程序，因为Idris抛出解析错误时，我试图使(嵌套)类型参数隐式： tupleId : ({a :

我只能在Idris 0.9.12中以一种相当笨拙的方式做排名：

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) -- doesn't compile

一个可能更大的问题是，我不能在高级类型中做类约束。我不能将以下Haskell函数转换为Idris：

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

这也防止我使用Idris函数作为类型的类型同义词，如Lens，这是Lens s t a b = forall f。函数f => (a→fb)→ s – > f t in Haskell。

任何补救或规避上述问题的方法？

我只是实现了这个在master，允许隐含在任意范围，它会在下一个黑客版本。它还没有很好的测试，虽然！我至少尝试了以下简单的例子，和其他几个：

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

主要的约束在一分钟，你不能直接给隐式参数的值，除了在顶层。我最终会做一些事情…

（编辑：李大同）

【声明】本站内容均来自网络，其相关言论仅代表作者个人观点，不代表本站立场。若无意侵犯到您的权利，请及时与联系站长删除相关内容!