Agda的評估策略是在哪裏指定的？

Question

鑑於所有阿格達程序終止，評估策略不要緊，指稱語義，但它的性能確實事（如果你曾經運行阿格達程序）。

那麼，這是否阿格達用什麼評價策略？是否使用codata（♯，♭）而不是數據更改評估策略？有沒有辦法強制按需呼叫又稱懶惰評估？

Answer 1

類型檢查可能需要評估正常形態，所以這非常重要，即使你沒有運行您的程序（但是請注意，類型檢查過程中評價可以看作是運行程序）。 Agda以正常順序評估表達式，這意味着函數在其參數被評估之前應用。數據類型也僅在需求時進行評估。

例如，假設我有個自然數和一些操作的這個定義他們：

data ℕ : Set where 
    zero : ℕ 
    suc : ℕ → ℕ 

{-# BUILTIN NATURAL ℕ #-} 
-- Older Agda versions might require you to specify 
-- what is zero and what is suc. 

infixl 4 _+_ 
infixl 5 _*_ 
infixr 6 _^_ 

_+_ : (m n : ℕ) → ℕ 
zero + n = n 
suc m + n = suc (m + n) 

_*_ : (m n : ℕ) → ℕ 
zero * n = zero 
suc m * n = n + m * n 

_^_ : (m n : ℕ) → ℕ 
m^zero = suc zero 
m^suc n = m * m^n 

因爲我們正在與一元的數值，可評估2^16需要的時間會比較大。然而，如果我們試圖評估const 1 (2^16)，它將結束在幾乎沒有時間。

const : ∀ {a b} {A : Set a} {B : Set b} → 
    A → B → A 
const x _ = x 

同樣的事情也適用於數據類型：

infixr 3 _∷_ 

data List {a} (A : Set a) : Set a where 
    [] : List A 
    _∷_ : A → List A → List A 

record ⊤ {ℓ} : Set ℓ where 

Head : ∀ {a} {A : Set a} → List A → Set _ 
Head   []  = ⊤ 
Head {A = A} (_ ∷ _) = A 

head : ∀ {a} {A : Set a} (xs : List A) → Head xs 
head []  = _ 
head (x ∷ _) = x 

replicate : ∀ {a} {A : Set a} → ℕ → A → List A 
replicate 0  _ = [] 
replicate (suc n) x = x ∷ replicate n x 

同樣，head (replicate 1000000 1)將幾乎立即評估。

然而，在正常順序不調用 - 需求，即計算不被共享。

open import Data.Product 
open import Relation.Binary.PropositionalEquality 

slow : 2^16 ≡ 65536 
slow = refl 

slower₁ : (λ x → x , x) (2^16) ≡ (65536 , 65536) 
slower₁ = refl 

slower₂ : 
    let x : ℕ 
     x = 2^16 
    in _≡_ {A = ℕ × ℕ} (x , x) (65536 , 65536) 
slower₂ = refl 

在這種情況下，類型檢查slower₁和slower₂將採取大致兩倍的時間slow需求。相比之下，調用 - 需要將分享的x計算和計算2^16只有一次。

---

注意，類型檢查過程中，你要計算表達式正常形態。如果周圍有任何粘合劑（λ或Π），則必須在粘合劑下面並評估內部表情。

λ n → 1 + n ==> λ n → suc n 

---

如何CODATA改變了嗎？與縮減的互動實際上相當簡單：除非您將♭應用於它，否則♯ x不會進一步評估。

這也是爲什麼♯被稱爲延遲和♭爲力。

---

您也可以將Agda編譯爲Haskell。還有JavaScript，但我不知道如何編譯，所以我會堅持編譯Haskell。

評估策略大多數是Haskell編譯器使用的。作爲一個例子，這裏就是發生瞭如下定義：

data ℕ : Set where 
    zero : ℕ 
    suc : ℕ → ℕ 

_+_ : (m n : ℕ) → ℕ 
zero + n = n 
suc m + n = suc (m + n) 

data Vec {a} (A : Set a) : ℕ → Set a where 
    [] : Vec A zero 
    _∷_ : ∀ {n} → A → Vec A n → Vec A (suc n) 

和編譯後：

-- ℕ 
data T1 a0 = C2 
      | C3 a0 

-- Vec 
data T12 a0 a1 a2 = C15 
        | C17 a0 a1 a2 

-- _+_ 
d6 (C2) v0 = MAlonzo.RTE.mazCoerce v0 
d6 v0 v1 
    = MAlonzo.RTE.mazCoerce 
     (d_1_6 (MAlonzo.RTE.mazCoerce v0) (MAlonzo.RTE.mazCoerce v1)) 
    where d_1_6 (C3 v0) v1 
     = MAlonzo.RTE.mazCoerce 
      (C3 
      (MAlonzo.RTE.mazCoerce 
       (d6 (MAlonzo.RTE.mazCoerce v0) (MAlonzo.RTE.mazCoerce v1)))) 

是的，最後一個是有點瘋狂。但是如果你稍微squ一下，你可以看到：

d6 C2 v0 = v0 
d6 (C3 v0) v1 = C3 (d6 v0 v1)