我只能在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 ()
主要的约束在一分钟,你不能直接给隐式参数的值,除了在顶层。我最终会做一些事情…
原文地址:https://www.jb51.cc/javaschema/282388.html
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。