如何解决在Idris中,为什么已经在别处定义了参数,我们为什么需要将类型归为类型呢?
为什么我们在下面写f : Type -> Type
而不是仅仅写f
-不是从Functor f
推断出来的?:
interface Functor f => Applicative (f : Type -> Type) where
pure : a -> f a
(<*>) : f (a -> b) -> f a -> f b
f
已经在以下类型中定义了其种类(或者我应该说Idris中的Type):
interface Functor (f : Type -> Type) where
map : (m : a -> b) -> f a -> f b
我听说在很多情况下,由于Idris的依存类型系统,Idris无法推断Haskell会使用的类型。这是这种情况吗?
一个相关的问题Failed to declare MonadPlus interface constrained on Monad描述了相同的行为,但并没有真正解决为什么无法推断类型的问题。
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。