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'衝突

回答

相關問題