有沒有一種很好的方式來直接使用` - >`作爲Idris中的一個函數？

Question

人們可以在伊德里斯函數返回一個類型，例如

t : Type -> Type -> Type 
t a b = a -> b 

但是現在的情況上來，我想用->摺疊類型列表（用寫一些解析器實驗時），即

typeFold : List Type -> Type 
typeFold = foldr1 (->) 

這樣typeFold [String, Int]會給String -> Int : Type。這不，雖然編譯：

error: no implicit arguments allowed 
    here, expected: ")", 
    dependent type signature, 
    expression, name 
typeFold = foldr1 (->) 
       ^

但是這工作得很好：

t : Type -> Type -> Type 
t a b = a -> b 

typeFold : List Type -> Type 
typeFold = foldr1 t 

有沒有更好的方式與->工作，如果沒有是值得提高的功能提出要求？

Answer 1

以這種方式使用->的問題在於，它不是一個類型構造函數，而是一個活頁夾，其中域綁定的名稱在範圍內，因此->本身沒有直接類型。例如，您定義的t不會捕獲依賴類型，如(x : Nat) -> P x。

雖然它有點煩瑣，但你正在做的是正確的做法。我不確信我們應該爲(->)作爲一個類型構造函數制定特殊的語法 - 部分原因是它確實不是一個，部分原因是它感覺當它不依賴於類型時會導致更多的混淆。

Answer 2

Data.Morphisms模塊提供了類似的內容，除了你必須圍繞Morphism「newtype」做所有的包裝/解包。