伊德里斯：在記錄隱參數

當我嘗試編譯這個例子伊德里斯：在記錄隱參數

record R where 
    f:() -> {t: Type} -> t

我得到這個錯誤：

Type mismatch between 
     () -> t1 (Type of f) 
and 
     () -> t (Expected type) 

Specifically: 
     Type mismatch between 
       t1 
     and 
       t

在另一方面，這種例子

record R where 
    f: {t: Type} ->() -> t

作品只是精細。你能告訴我第一個問題嗎？

來源

2017-09-16 Gregg54654

我不確定，但我想隱式參數必須出現在非隱式參數之前 – marcosh

是的，也許。這有點奇怪，因爲這對使用數據的等效定義沒有問題： 'data D：Type MkD：（f：（） - > {t：Type} - > t） - > D' – Gregg54654

我也是實例化這樣的記錄有問題。我沒有數據問題。不幸的是，我沒有這個簡單的例子。 – Gregg54654

這是Idris中的一個錯誤：有時->運算符不是正確關聯的：issue #4077。

要看到它，我們可以desugar記錄語法：

data R : Type where 
    MkR : (() -> {t : Type} -> t) -> R

現在，我們需要手動執行f投影。事實證明，

f : R -> (() -> {t : Type} -> t) 
f (MkR g) = g

不不類型檢測，但

f : R ->() -> {t : Type} -> t 
f (MkR g) = g

一樣。

在我看來，伊德里斯使用第一個變體來解除record爲data，因此您觀察到的錯誤。

來源

2017-09-18 13:13:16

伊德里斯：在記​​錄隱參數

回答

相關問題

伊德里斯：在記錄隱參數