Dlaczego Coq zawiera wyrażenia let w swoim podstawowym języku?

Coq zawiera wyrażenia let w swoim podstawowym języku. Możemy tłumaczyć wyrażenia let na takie aplikacje: let x : t = v in b ~> (\(x:t). b) v Rozumiem, że to nie zawsze działa, ponieważ wartość vnie byłaby dostępna podczas sprawdzania typu b. Można to jednak łatwo naprawić poprzez specjalną obudowę do sprawdzania poprawności aplikacji formularza (\(x:t). b) v. Pozwala nam to usunąć wyrażenia let kosztem specjalnego przypadku podczas sprawdzania typu. Dlaczego Coq zawiera nadal wyrażenia let? Czy mają inne zalety (poza tym, że nie wymagają specjalnego przypadku)?

Jest powszechnym błędnym przekonaniem, że możemy tłumaczyć let-wyrażenia na aplikacje. Różnica między let x : t := b in vi (fun x : t => v) bpolega na tym, że w let-wyrażeniu, podczas sprawdzania typu vwiemy, że xjest on równy b, ale w aplikacji tak nie jest (podwyrażenie fun x : t => vmusi mieć sens samo w sobie).

Oto przykład:

(* Dependent type of vectors. *)
Inductive Vector {A : Type} : nat -> Type :=
  | nil : Vector 0
  | cons : forall n, A -> Vector n -> Vector (S n).

(* This works. *)
Check (let n := 0 in cons n 42 nil).

(* This fails. *)
Check ((fun (n : nat) => cons n 42 nil) 0).

Twoja sugestia, aby uczynić aplikację (fun x : t => v) bspecjalnym przypadkiem, tak naprawdę nie działa. Zastanówmy się nad tym ostrożniej.

Na przykład, jak sobie z tym poradzisz, kontynuując powyższy przykład?

Definition a := (fun (n : nat) => cons n 42 nil).
Check a 0.

Prawdopodobnie to nie zadziała, ponieważ anie można go wpisać, ale jeśli rozwiniemy jego definicję, otrzymamy dobrze napisane wyrażenie. Czy uważasz, że użytkownicy będą nas kochać, czy nienawidzą nas za naszą decyzję dotyczącą projektu?

Musisz dokładnie przemyśleć, co to znaczy mieć „specjalny przypadek”. Jeśli mam aplikację e₁ e₂, czy powinienem ją znormalizować, e₁zanim zdecyduję, czy jest to abstrakcja ? Jeśli tak, oznacza to, że będę normalizować wyrażenia źle wpisane, a te mogą się cyklicznie zmieniać. Jeśli nie, użyteczność twojej propozycji wydaje się wątpliwa.$\lambda$

Zerwalibyście także podstawowe twierdzenie, które mówi, że każde podwyrażenie dobrze napisanego wyrażenia jest dobrze napisane. To tak rozsądne, jak wprowadzenie nulldo Javy.