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ść v
nie 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)?
type-theory
dependent-types
type-checking
coq
Labbekak
źródło
źródło
let
wyrażeń, ale nie ma a) powodu, aby unikaćlet
wyrażeń i są one również wygodne, oraz b) dodanie hacków do twojego podstawowego języka nie jest świetnym pomysłem.Odpowiedzi:
Jest powszechnym błędnym przekonaniem, że możemy tłumaczyć
let
-wyrażenia na aplikacje. Różnica międzylet x : t := b in v
i(fun x : t => v) b
polega na tym, że wlet
-wyrażeniu, podczas sprawdzania typuv
wiemy, żex
jest on równyb
, ale w aplikacji tak nie jest (podwyrażeniefun x : t => v
musi mieć sens samo w sobie).Oto przykład:
Twoja sugestia, aby uczynić aplikację
(fun x : t => v) b
specjalnym 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?
Prawdopodobnie to nie zadziała, ponieważ
a
nie 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.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
null
do Javy.źródło