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除非您申请?,否则不会进一步评估.

这也是为什么?被称为延迟和?作为力.

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