lazy-evaluation - Agda 的评估策略在任何地方都有规定吗？

Question

鉴于所有Agda程序都终止了，评估策略对于定义语义并不重要，但对性能却至关重要(以防您曾经运行过Agda程序)。

那么， Agda 使用哪种评估策略？使用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应用于它，否则 ♭不会进行任何进一步的评估。

这也是为什么 ♯被称为delay和 ♭被称为force的原因。

您还可以将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))))

是的，最后一个有点疯狂。但是，如果您稍稍蹲下，您会看到:

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