Typüberprüfung könnte Auswertung Normalform erfordern, so dass es nicht egal, auch wenn Sie nicht über Ihre Programme laufen (aber ja, Auswertung bei der Typprüfung als die Ausführung des Programms angesehen werden könnte). Agda wertet Ausdrücke in normaler Reihenfolge aus, was bedeutet, dass Funktionen angewendet werden, bevor ihre Argumente ausgewertet werden. Datentypen werden auch nur bei Bedarf ausgewertet.
Angenommen, ich habe diese Definition der natürlichen Zahlen und einige Operationen auf sie:
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
Da wir mit einstelligen Zahlen arbeiten, 2^16 Auswertung wird eine ganze Menge Zeit in Anspruch nehmen. Wenn wir jedoch versuchen, const 1 (2^16) auszuwerten, wird es in fast keiner Zeit fertig sein.
const : ∀ {a b} {A : Set a} {B : Set b} →
A → B → A
const x _ = x
Das gleiche gilt für die Datentypen:
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
Wieder head (replicate 1000000 1) fast sofort auswerten wird.
jedoch normale Ordnung nicht ist Call-by-Bedarf, sind nämlich Berechnungen nicht mit anderen geteilt.
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
In diesem Fall geben Sie slower₁ und slower₂ Überprüfung wird in etwa der doppelten Zeit slow Bedürfnisse nehmen. Im Vergleich dazu Call-by-Bedarf würde die Berechnung von x teilen und 2^16 nur einmal berechnen.
Beachten Sie, dass Sie bei der Typprüfung Ausdrücke in Normalform auswerten müssen. Wenn es irgendwelche Bindemittel sind um (λ oder Π), müssen Sie unter dem Bindemittel gehen und den inneren Ausdruck als auch zu bewerten.
λ n → 1 + n ==> λ n → suc n
Wie funktioniert CODATA das Bild ändern? Die Interaktion mit der Reduktion ist eigentlich recht einfach: ♯ x wertet nicht weiter, wenn Sie ♭ für sie gelten.
Dies ist auch, warum ♯ als Verzögerung und ♭ als Kraft bekannt ist.
Sie können Agda auch zu Haskell kompilieren. Es gibt auch JavaScript, aber ich weiß nicht, wie das kompiliert wird, also bleibe ich bei der Kompilation zu Haskell.
Die Strategie Auswertung ist vor allem, was das Haskell Compiler verwendet.Als Beispiel ist hier, was zu den folgenden Definitionen passiert:
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)
Und nach der Kompilierung:
-- ℕ
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))))
Yup, ist die letzte ein bisschen verrückt. Aber wenn Sie ein bisschen squit, können Sie sehen:
d6 C2 v0 = v0
d6 (C3 v0) v1 = C3 (d6 v0 v1)