Idris中的实例解析

Question

有没有人能告诉我为什么

works : WriterT w (ReaderT r Identity) _ -> ReaderT r Identity w
works = execWriterT

但这是

doesnt : WriterT w (Reader r) _ -> Reader r w
doesnt = execWriterT

我得到了错误

Can't find implementation for Functor (Reader r)

但是由于Reader r a的定义是ReaderT r Identity a，我们可以看到works和doesnt在定义上是相同的。我认为这只是实例解析算法的一个bug。怎么回事？

我对Idris完全陌生，我不确定我是否能以某种方式显式地提供实例参数。

对于完成，execWriterT的定义是：

execWriterT : Functor m => WriterT w m a -> m w
execWriterT = (map snd) . runWriterT

环境信息：

> uname -rov                       
4.15.0-29-generic #31-Ubuntu SMP Tue Jul 17 15:39:52 UTC 2018 GNU/Linux
> idris --version
1.3.0-git:61cf812e

编辑:也适用于Idris版本1.3.0-git:713e485f (撰写本文时的master)

Answer 1

这是一个图书馆的bug，真的。Reader由以下定义

Reader r a = ReaderT r Identity a

请注意，a是Reader的参数。此eta-合同至

Reader r = ReaderT r Identity

但这些定义并不等价。(或者更确切地说:它们在外延上是等价的(相同的行为)，但在内涵上是不同的(相同的定义)。

doesnt不工作的原因是因为Reader r不会减少。Reader使用两个参数定义，而Reader r只应用一个参数。它不是完全饱和的，因此它不会简化。除非您再应用一个参数，否则Idris根本不知道Reader r与ReaderT r Identity相关。这会导致实例解析失败，因为实例是用于ReaderT r f的，而不是用于Reader r的(并且您不能为Reader r编写(有用的)实例，因为Reader不是数据类型)。

这是可行的：

Reader' : Type -> Type -> Type
Reader' r = ReaderT r Identity

doesnt : WriterT w (Reader' r) _ -> Reader' r w
doesnt = execWriterT

尽管对submit a PR来说更正确的事情应该是。