伊德里斯急於評價

Question

在哈斯克爾，我可能會實現if這樣的：

if' True x y = x 
if' False x y = y 
spin 0 =() 
spin n = spin (n - 1) 

這行爲我怎麼想到：

haskell> if' True (spin 1000000)() -- takes a moment 
haskell> if' False (spin 1000000)() -- immediate 

---

在球拍，我可以實施一個有缺陷的if像這樣：

(define (if2 cond x y) (if cond x y)) 
(define (spin n) (if (= n 0) (void) (spin (- n 1)))) 

這行爲我怎麼想到：

racket> (if2 #t (spin 100000000) (void)) -- takes a moment 
racket> (if2 #f (spin 100000000) (void)) -- takes a moment 

---

在伊德里斯，我可能會實現if這樣的：

if' : Bool -> a -> a -> a 
if' True x y = x 
if' False x y = y 
spin : Nat ->() 
spin Z =() 
spin (S n) = spin n 

這行爲surpris上課我：

idris> if' True (spin 1000)() -- takes a moment 
idris> if' False (spin 1000)() -- immediate 

我預計Irdis表現得像個球拍，其中兩個參數是 評估。但事實並非如此！

伊德里斯如何決定何時評估事物？

Answer 1

我們說伊德里斯有嚴格的評估，但這是針對它的運行時語義。

作爲完全依賴類型的語言，Idris有兩個階段，它評估事物，編譯時和運行時。在編譯時，它只會評估它知道的全部內容（即終止並覆蓋所有可能的輸入），以便確保類型檢查是可確定的。編譯時評估器是Idris內核的一部分，並且在Haskell中使用HOAS（高階抽象語法）樣式表示值來實現。由於這裏所有東西都有一個正常的形式，所以評估策略實際上並不重要，因爲無論哪種方式它都會得到相同的答案，並且在實踐中，它將執行Haskell運行時系統選擇執行的任何操作。

爲方便起見，REPL使用編譯時評估的概念。所以，你的'旋轉1000'實際上從來沒有得到評估。如果您使用相同的代碼創建可執行文件，我期望看到非常不同的行爲。

除了更容易實現（因爲我們有評估器可用），這可以非常有用地顯示術語如何在類型檢查器中評估。所以你可以看到的區別：

Idris> \n, m => (S n) + m 
\n => \m => S (plus n m) : Nat -> Nat -> Nat 

Idris> \n, m => n + (S m) 
\n => \m => plus n (S m) : Nat -> Nat -> Nat 

這將是困難（雖然不是不可能的），如果我們使用的REPL，這下不lambda表達式減少運行時的評價。