伊德里斯類型導出用於算術運算

在下面的代碼伊德里斯類型導出用於算術運算

Idris> :t \x => x + x 
\x => x + x : Integer -> Integer

伊德里斯導出一個整數類型的X變量，其中我認爲它應該得到像在Haskell接口不限於：

Haskell> :t (\x y -> x + y) 
(\x y -> x + y) :: Num a => a -> a -> a

然後它甚至不像一個Integer，接受Double類型：

Idris> (\x => x + x) 2.0 
4.0 : Double

Can有人向我解釋這一點？

來源

2017-08-13 Ivan Kleshnin

「Idris」的類型推理並沒有Haskell那麼成熟。對於依賴類型，類型推斷不會那麼好。這裏可能會出現類似於單態限制的情況。爲了更好地解釋這種行爲，你應該在'idris-dev'倉庫中打開bug：https://github.com/idris-lang/Idris-dev/issues – Shersh

@Shersh依賴類型不需要對類型推斷進行任何限制爲非依賴程序。另外，這個案例涉及泛化而不是推論，而且伊德里斯沒有通過設計進行概括，也不是因爲任何根本原因。 –

@AndrásKovács您能指引我談談關於這個「Idris沒有設計概括性」主題的內容嗎？ –

我認爲在一般情況下，可以說在idris的REPL中檢查類型推斷是一個壞主意。存在於Idris文件中的REPL代碼和代碼行爲有所不同。

你想要的功能將被寫成：

addy: Num a => a -> a -> a 
addy x y = x + y

和將有一個類型類同您從Haskell的期望之一。 Idris中的類型推斷通常非常弱（因爲它不能用於依賴型類型系統）。

來源

2017-08-14 09:24:46 Markus

伊德里斯類型導出用於算術運算

回答

相關問題