Idris模块名称与'base'冲突

我有一个模块，其名称以Data.List结尾。在里面我想从基础库导入模块Data.List。Idris模块名称与'base'冲突

module Foo.Data.List 
import Data.List

如果我调用从文件夹Foo伊德里斯那么编译器抱怨：

[Foo]$ idris --check Data/List.idr 
Cycle detected in imports: Data/List.idr -> Data/List -> Data/List

我猜是因为它喜欢的模块中的电流源文件夹是，这仅仅是被定义的模块。

我该如何参考基础库中的Data.List？在其全

我的小源文件：

module Foo.Data.List 
import Data.List as S 

last : List e -> Maybe e 
last l = case l of 
    (h::t) => Just (S.last (h::t)) 
    _ => Nothing

更新时间：

如果我从包含Foo的文件夹调用伊德里斯，

idris --check Foo/Data.List.idr

然后我得到的错误信息：

When checking right hand side of Foo.Data.List.case block in last at ./Foo/Data/List.idr:6:15 with expected type 
     Maybe e 

When checking argument x to constructor Prelude.Maybe.Just: 
     Type mismatch between 
       Maybe e (Type of last (h :: t)) 
     and 
       e (Expected type)

这意味着编译器将S.last视为Foo.Data.List.last而不是base.Data.List.last。

来源

2016-02-25 libeako

我使用0.10.0上惊天动地的释放。 – libeako

考虑到以下目录结构：

[idris-stuff]$ tree 
. 
└── myproject 
    └── Foo 
     └── Data 
      └── List.idr

您需要在myproject目录下运行idris，不myproject/Foo：

[idris-stuff]$ cd myproject 
[myproject]$ idris --check Foo/Data/List.idr

如果您尝试从Foo运行它，它就会失败因为您的本地Data/List.idr文件将被挑选超过标准库一个：

[myproject]$ cd Foo/ 
[Foo]$ idris --check Data/List.idr 
Cycle detected in imports: Data/List.idr -> Data/List -> Data/List

来源

2016-02-28 03:19:42 Cactus

什么是解决方案是例如能够引用具有唯一路径前缀的标准库，如“base”。 – libeako

当您在其他模块中导入Data.List时，它不会选择'Foo.Data.list'，除非您错误地尝试从'Foo'内部编译其他模块。 – Cactus

第二个问题仅仅是由于S.last不在范围内，因为没有定义名称Data.List.last而引起的。您收到的错误消息非常混乱，可能值得作为Idris错误报告;一个更好的错误信息将是一个抱怨S.last不在范围之内。

要机智，预期以下版本typechecks和作品：

module Foo.Data.List 
import Prelude.List as S 

last : List e -> Maybe e 
last l = case l of 
    (h :: t) => Just (S.last (h::t)) 
    _ => Nothing

来源

2016-03-01 11:06:52 Cactus

基地/ Data.Last.last是否存在并不重要。编译器确实找到了Flast.Foo.Data.List.last - 这当然会导致类型错误。问题是S = Foo.Data.List而不是base/Data.List。 – libeako

是的，伊德里斯的错误信息是误导性的。 – Cactus

Idris模块名称与'base'冲突

回答

相关问题