Фактически, есть ошибки компиляции. Исполняемый agda находит ошибку и передает эту информацию в agda-mode в Emacs, которая, в свою очередь, выделяет синтаксис, чтобы вы знали, что произошла ошибка. Мы можем посмотреть, что произойдет, если мы напрямую используем agda. Вот файл, я использую:
module C1 where
open import Data.Nat
loop : ℕ → ℕ
loop 0 = 0
loop x = loop x
Теперь мы называем agda -i../lib-0.7/src -i. C1.agda (не против -i параметров, они просто дайте исполняемый знать, где искать для стандартной библиотеки), и мы получаем ошибку:
Termination checking failed for the following functions:
loop
Problematic calls:
loop x
(at D:\Agda\tc\C1.agda:7,10-14)
Это действительно ошибка компиляции. Такие ошибки мешают нам от import от этого модуля от других модулей или их компиляции. Например, если мы добавим эти строки в указанном файле:
open import IO
main = run (putStrLn "")
И компилировать модуль с помощью C-c C-x C-c, agda-mode жалуется:
You can only compile modules without unsolved metavariables
or termination checking problems.
Другие виды ошибок компиляции включают в себя проблемы проверочные типа:
module C2 where
open import Data.Bool
open import Data.Nat
type-error : ℕ → Bool
type-error n = n
__________________________
D:\Agda\tc\C2.agda:7,16-17
ℕ !=< Bool of type Set
when checking that the expression n has type Bool
Неисправность проверки положительности:
module C3 where
data Positivity : Set where
bad : (Positivity → Positivity) → Positivity
__________________________
D:\Agda\tc\C3.agda:3,6-16
Positivity is not strictly positive, because it occurs to the left
of an arrow in the type of the constructor bad in the definition of
Positivity.
Или нераскрытый метапеременный:
module C4 where
open import Data.Nat
meta : ∀ {a} → ℕ
meta = 0
__________________________
Unsolved metas at the following locations:
D:\Agda\tc\C4.agda:5,11-12
Теперь вы справедливо заметили, что некоторые ошибки «тупики», в то время как другие позволяют продолжать писать свою программу. Это потому, что некоторые ошибки хуже других. Например, если вы получаете нераскрытую метапеременная, есть вероятность, что вы сможете просто заполнить недостающую информацию, и все будет хорошо.
Что касается подвешивания компилятора: проверка или компиляция модуля не должна приводить к замыканию agda. Давайте попробуем принудительно выполнить проверку типа. Мы добавим больше материала в модуль C1:
data _≡_ {a} {A : Set a} (x : A) : A → Set a where
refl : x ≡ x
test : loop 1 ≡ 1
test = refl
Теперь, чтобы проверить, что refl является правильным выражением этого типа, agda должен оценить loop 1. Однако, поскольку проверка завершения не удалась, agda не разворачивается loop (и заканчивается бесконечным циклом).
Однако C-c C-n действительно заставляет agda попытаться оценить выражение (вы в основном говорите «Я знаю, что я делаю»), поэтому, естественно, вы попадаете в бесконечный цикл.
Кстати, вы можете сделать agda петлю, если отключить проверку завершения:
{-# NO_TERMINATION_CHECK #-}
loop : ℕ → ℕ
loop 0 = 0
loop x = loop x
data _≡_ {a} {A : Set a} (x : A) : A → Set a where
refl : x ≡ x
test : loop 1 ≡ 1
test = refl
который заканчивается:
stack overflow
Как правило: если вы можете сделать цикл agda путем проверки (или компиляции) модуля без использования каких-либо компиляторов pragmas, th Это действительно ошибка, и ее следует сообщать на bug tracker. Тем не менее, существует несколько способов сделать программу без завершения, если вы хотите использовать прагмы компилятора. Мы уже видели {-# NO_TERMINATION_CHECK #-}, вот некоторые другие способы:
{-# OPTIONS --no-positivity-check #-}
module Boom where
data Bad (A : Set) : Set where
bad : (Bad A → A) → Bad A
unBad : {A : Set} → Bad A → Bad A → A
unBad (bad f) = f
fix : {A : Set} → (A → A) → A
fix f = (λ x → f (unBad x x)) (bad λ x → f (unBad x x))
loop : {A : Set} → A
loop = fix λ x → x
Это один опирается на тип данных, который не является строго положительным. Или мы могли бы заставить agda принять Set : Set (то есть, тип Set является Set сам) и реконструировать Russell's paradox:
{-# OPTIONS --type-in-type #-}
module Boom where
open import Data.Empty
open import Data.Product
open import Relation.Binary.PropositionalEquality
data M : Set where
m : (I : Set) → (I → M) → M
_∈_ : M → M → Set
a ∈ m I f = Σ I λ i → a ≡ f i
_∉_ : M → M → Set
a ∉ b = (a ∈ b) → ⊥
-- Set of all sets that are not members of themselves.
R : M
R = m (Σ M λ a → a ∉ a) proj₁
-- If a set belongs to R, it does not contain itself.
lem₁ : ∀ {X} → X ∈ R → X ∉ X
lem₁ ((Y , Y∉Y) , refl) = Y∉Y
-- If a set does not contain itself, then it is in R.
lem₂ : ∀ {X} → X ∉ X → X ∈ R
lem₂ X∉X = (_ , X∉X) , refl
-- R does not contain itself.
lem₃ : R ∉ R
lem₃ R∈R = lem₁ R∈R R∈R
-- But R also contains itself - a paradox.
lem₄ : R ∈ R
lem₄ = lem₂ lem₃
loop : {A : Set} → A
loop = ⊥-elim (lem₃ lem₄)
(source). Мы могли бы также написать вариант парадокса Жирара, simplified by A.J.C. Hurkens:
{-# OPTIONS --type-in-type #-}
module Boom where
⊥ = ∀ p → p
¬_ = λ A → A → ⊥
℘_ = λ A → A → Set
℘℘_ = λ A → ℘ ℘ A
U = (X : Set) → (℘℘ X → X) → ℘℘ X
τ : ℘℘ U → U
τ t = λ (X : Set) (f : ℘℘ X → X) (p : ℘ X) → t λ (x : U) → p (f (x X f))
σ : U → ℘℘ U
σ s = s U λ (t : ℘℘ U) → τ t
τσ : U → U
τσ x = τ (σ x)
Δ = λ (y : U) → ¬ (∀ (p : ℘ U) → σ y p → p (τσ y))
Ω = τ λ (p : ℘ U) → ∀ (x : U) → σ x p → p x
loop : (A : Set) → A
loop = (λ (₀ : ∀ (p : ℘ U) → (∀ (x : U) → σ x p → p x) → p Ω) →
(₀ Δ λ (x : U) (₂ : σ x Δ) (₃ : ∀ (p : ℘ U) → σ x p → p (τσ x)) →
(₃ Δ ₂ λ (p : ℘ U) → (₃ λ (y : U) → p (τσ y)))) λ (p : ℘ U) →
₀ λ (y : U) → p (τσ y)) λ (p : ℘ U) (₁ : ∀ (x : U) → σ x p → p x) →
₁ Ω λ (x : U) → ₁ (τσ x)
Это один является реальной беспорядок, хотя. Но он обладает хорошим свойством, что он использует только зависимые функции. Как ни странно, он даже не прошел проверку типа и не вызвал цикл agda. Разделение всего loop срок на две части.