Bsrgvty

How was the Luftwaffe able to destroy nearly 4000 Soviet aircraft in 3 days of operation Barbarossa?

What was the sound coming from below the feet of the Death Eaters at Malfoy Manor?

Why does the B-2 Spirit have a pattern of thin white lines?

What is the difference between chemical equilibrium and dynamic equilibrium?

This Riley Riddle is a Mess

What instructions should I give to an untrained passenger for Hand propping Cessna 172N as a pilot?

Difference between apply and funcall

What antenna is this in an Apollo 15 LM photo?

Quantum circuits explain algorithms, why didn't classical circuits?

How can I swallow pills more easily?

Are we experiencing lower level of gravity now compared to past?

Conditional proof demonstration

Short story from the 70s(?) about aliens/angels destroying humankind, from the point of view of a priest/pastor

Is this a reasonable magic pet?

Perfect pitch on only one instrument?

How would a medieval village protect themselves against dinosaurs?

How can I make sure a string contains at least one uppercase letter, one lowercase letter, one number and one punctuation character?

Is there a way to determine what kind of data is sitting in the Redo Queue for an AlwaysOn AG Secondary Replica?

How can I convince my child to write?

How to end sending data over I2C by Slave or Master?

How do the different seasons work for Eladrin?

Balancing empathy and deferring to the syllabus in teaching responsibilities

Is military allowed to wear civilian clothes when testifying in Congress?

What are these color strips for?

Why does Coq include let-expressions in its core language

Theorem Proofs in CoqCan coq express its own metatheory?Collection of inference rules viewed itself as a judgmentLocal type argument synthesis when type variable does not appear in argumentsPure type systems and let-expressionsUnderstanding the definition of Positivity Constraints in CoqHow does this use of “apply” in Coq work?Drawbacks of adding type equality to 1MLDoes dependent type checkers need to store lambda parameter type in their core language?For proof automation in Coq, when is it appropriate to use canonical structures or Equations instead of Ltac?

.everyoneloves__top-leaderboard:empty,.everyoneloves__mid-leaderboard:empty,.everyoneloves__bot-mid-leaderboard:empty
margin-bottom:0;

9

3

$begingroup$

Coq includes let-expressions in its core language.
We can translate let-expressions to applications like this:
let x : t = v in b ~> ((x:t). b) v
I understand that this does not always work because the value v would not be available when typechecking b. However this can be easily fixed by special casing the typechecking of applications of the form ((x:t). b) v. This allows us to remove let-expressions at the cost of a special case while typechecking. Why does Coq include still include let-expressions? Do they have other advantages (besides not needing the special case)?

type-theory dependent-types type-checking coq

share|cite|improve this question

asked Sep 11 at 14:19

LabbekakLabbekak

44311 silver badge88 bronze badges

$endgroup$

• 
  
  
  

  
  4
  

  
  
  
  
  
  

  
  $begingroup$
  Your suggestion sounds like adding a hack to avoid needing let expressions, but there's a) no reason to avoid let expressions and they are also convenient, and b) adding hacks to your core language is not a great idea.
  $endgroup$
  – Derek Elkins
  Sep 11 at 19:02
  

  
  
  
  

add a comment
 | 

9

3

$begingroup$

Coq includes let-expressions in its core language.
We can translate let-expressions to applications like this:
let x : t = v in b ~> ((x:t). b) v
I understand that this does not always work because the value v would not be available when typechecking b. However this can be easily fixed by special casing the typechecking of applications of the form ((x:t). b) v. This allows us to remove let-expressions at the cost of a special case while typechecking. Why does Coq include still include let-expressions? Do they have other advantages (besides not needing the special case)?

type-theory dependent-types type-checking coq

share|cite|improve this question

asked Sep 11 at 14:19

LabbekakLabbekak

44311 silver badge88 bronze badges

$endgroup$

• 
  
  
  

  
  4
  

  
  
  
  
  
  

  
  $begingroup$
  Your suggestion sounds like adding a hack to avoid needing let expressions, but there's a) no reason to avoid let expressions and they are also convenient, and b) adding hacks to your core language is not a great idea.
  $endgroup$
  – Derek Elkins
  Sep 11 at 19:02
  

  
  
  
  

add a comment
 | 

$begingroup$

Coq includes let-expressions in its core language.
We can translate let-expressions to applications like this:
let x : t = v in b ~> ((x:t). b) v
I understand that this does not always work because the value v would not be available when typechecking b. However this can be easily fixed by special casing the typechecking of applications of the form ((x:t). b) v. This allows us to remove let-expressions at the cost of a special case while typechecking. Why does Coq include still include let-expressions? Do they have other advantages (besides not needing the special case)?

type-theory dependent-types type-checking coq

share|cite|improve this question

asked Sep 11 at 14:19

LabbekakLabbekak

44311 silver badge88 bronze badges

$endgroup$

share|cite|improve this question

asked Sep 11 at 14:19

LabbekakLabbekak

44311 silver badge88 bronze badges

share|cite|improve this question

asked Sep 11 at 14:19

LabbekakLabbekak

44311 silver badge88 bronze badges

asked Sep 11 at 14:19

LabbekakLabbekak

44311 silver badge88 bronze badges

asked Sep 11 at 14:19

LabbekakLabbekak

44311 silver badge88 bronze badges

1 Answer
1

active

oldest

votes

23

$begingroup$

It is a common misconception that we can translate let-expresions to applications. The difference between let x : t := b in v and (fun x : t => v) b is that in the let-expression, during type-checking of v we know that x is equal to b, but in the application we do not (the subexpression fun x : t => v has to make sense on its own).

Here is an example:

(* 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).

Your suggestion to make application (fun x : t => v) b a special case does not really work. Let us think about it more carefully.

For example, how would you deal with this, continuing the above example?

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

Presumably this will not work because a cannot be typed, but if we unfold its definition, we get a well-typed expression. Do you think the users will love us, or hate us for our design decision?

You need to think carefully what it means to have the "special case". If I have an application e₁ e₂, should I normalize e₁ before I decide whether it is a $lambda$-abstraction? If yes, this means I will be normalizing ill-typed expressions, and those might cycle. If no, the usability of your proposal seems questionable.

You would also break the fundamental theorem which says that every sub-expression of a well-typed expression is well-typed. That's as sensible as introducing null into Java.

share|cite|improve this answer

edited Sep 11 at 19:24

answered Sep 11 at 17:11

Andrej BauerAndrej Bauer

22.6k11 gold badge5151 silver badges9191 bronze badges

$endgroup$

add a comment
 | 

Your Answer

StackExchange.ready(function()
var channelOptions =
tags: "".split(" "),
id: "419"
;
initTagRenderer("".split(" "), "".split(" "), channelOptions);

StackExchange.using("externalEditor", function()
// Have to fire editor after snippets, if snippets enabled
if (StackExchange.settings.snippets.snippetsEnabled)
StackExchange.using("snippets", function()
createEditor();
);

else
createEditor();

);

function createEditor()
StackExchange.prepareEditor(
heartbeatType: 'answer',
autoActivateHeartbeat: false,
convertImagesToLinks: false,
noModals: true,
showLowRepImageUploadWarning: true,
reputationToPostImages: null,
bindNavPrevention: true,
postfix: "",
imageUploader:
brandingHtml: "Powered by u003ca class="icon-imgur-white" href="https://imgur.com/"u003eu003c/au003e",
contentPolicyHtml: "User contributions licensed under u003ca href="https://creativecommons.org/licenses/by-sa/4.0/"u003ecc by-sa 4.0 with attribution requiredu003c/au003e u003ca href="https://stackoverflow.com/legal/content-policy"u003e(content policy)u003c/au003e",
allowUrls: true
,
onDemand: true,
discardSelector: ".discard-answer"
,immediatelyShowMarkdownHelp:true
);



);

draft saved

draft discarded

Sign up or log in

StackExchange.ready(function ()
StackExchange.helpers.onClickDraftSave('#login-link');
);

Sign up using Google

Sign up using Facebook

Sign up using Email and Password

Post as a guest

Name

Email

Required, but never shown

StackExchange.ready(
function ()
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fcs.stackexchange.com%2fquestions%2f114640%2fwhy-does-coq-include-let-expressions-in-its-core-language%23new-answer', 'question_page');

);

Post as a guest

Name

Email

Required, but never shown

23

$begingroup$

It is a common misconception that we can translate let-expresions to applications. The difference between let x : t := b in v and (fun x : t => v) b is that in the let-expression, during type-checking of v we know that x is equal to b, but in the application we do not (the subexpression fun x : t => v has to make sense on its own).

Here is an example:

(* 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).

Your suggestion to make application (fun x : t => v) b a special case does not really work. Let us think about it more carefully.

For example, how would you deal with this, continuing the above example?

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

Presumably this will not work because a cannot be typed, but if we unfold its definition, we get a well-typed expression. Do you think the users will love us, or hate us for our design decision?

You need to think carefully what it means to have the "special case". If I have an application e₁ e₂, should I normalize e₁ before I decide whether it is a $lambda$-abstraction? If yes, this means I will be normalizing ill-typed expressions, and those might cycle. If no, the usability of your proposal seems questionable.

You would also break the fundamental theorem which says that every sub-expression of a well-typed expression is well-typed. That's as sensible as introducing null into Java.

share|cite|improve this answer

edited Sep 11 at 19:24

answered Sep 11 at 17:11

Andrej BauerAndrej Bauer

22.6k11 gold badge5151 silver badges9191 bronze badges

$endgroup$

add a comment
 | 

23

$begingroup$

It is a common misconception that we can translate let-expresions to applications. The difference between let x : t := b in v and (fun x : t => v) b is that in the let-expression, during type-checking of v we know that x is equal to b, but in the application we do not (the subexpression fun x : t => v has to make sense on its own).

Here is an example:

(* 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).

Your suggestion to make application (fun x : t => v) b a special case does not really work. Let us think about it more carefully.

For example, how would you deal with this, continuing the above example?

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

Presumably this will not work because a cannot be typed, but if we unfold its definition, we get a well-typed expression. Do you think the users will love us, or hate us for our design decision?

You need to think carefully what it means to have the "special case". If I have an application e₁ e₂, should I normalize e₁ before I decide whether it is a $lambda$-abstraction? If yes, this means I will be normalizing ill-typed expressions, and those might cycle. If no, the usability of your proposal seems questionable.

You would also break the fundamental theorem which says that every sub-expression of a well-typed expression is well-typed. That's as sensible as introducing null into Java.

share|cite|improve this answer

edited Sep 11 at 19:24

answered Sep 11 at 17:11

Andrej BauerAndrej Bauer

22.6k11 gold badge5151 silver badges9191 bronze badges

$endgroup$

add a comment
 | 

$begingroup$

It is a common misconception that we can translate let-expresions to applications. The difference between let x : t := b in v and (fun x : t => v) b is that in the let-expression, during type-checking of v we know that x is equal to b, but in the application we do not (the subexpression fun x : t => v has to make sense on its own).

Here is an example:

(* 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).

Your suggestion to make application (fun x : t => v) b a special case does not really work. Let us think about it more carefully.

For example, how would you deal with this, continuing the above example?

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

Presumably this will not work because a cannot be typed, but if we unfold its definition, we get a well-typed expression. Do you think the users will love us, or hate us for our design decision?

You need to think carefully what it means to have the "special case". If I have an application e₁ e₂, should I normalize e₁ before I decide whether it is a $lambda$-abstraction? If yes, this means I will be normalizing ill-typed expressions, and those might cycle. If no, the usability of your proposal seems questionable.

You would also break the fundamental theorem which says that every sub-expression of a well-typed expression is well-typed. That's as sensible as introducing null into Java.

share|cite|improve this answer

edited Sep 11 at 19:24

answered Sep 11 at 17:11

Andrej BauerAndrej Bauer

22.6k11 gold badge5151 silver badges9191 bronze badges

$endgroup$

(* 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).

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

share|cite|improve this answer

edited Sep 11 at 19:24

answered Sep 11 at 17:11

Andrej BauerAndrej Bauer

22.6k11 gold badge5151 silver badges9191 bronze badges

answered Sep 11 at 17:11

Andrej BauerAndrej Bauer

22.6k11 gold badge5151 silver badges9191 bronze badges

answered Sep 11 at 17:11

Andrej BauerAndrej Bauer

22.6k11 gold badge5151 silver badges9191 bronze badges