<div dir="ltr">Hi Peter,<br><div><br>In my understanding, the difference between 'let' and 'where' is that the first defines expressions while the second one contains function definitions. This means that allowing "(x , y)" in the left-hand side of something in a where block would be ambiguous: it could mean that you're defining two values x and y as the first and second projections of the RHS (as you want), OR it could mean that you're defining a new function called x with two arguments called "," and "y" respectively. I know this second interpretation seems completely absurd, but Agda has no way to know that. This is also why you get the error message "missing type signature for the left-hand side": Agda expects you to give a type signature for this function "x" it thinks you are defining.<br><br></div><div>The other problem you have (where blocks are not allowed in a let expression) seems like something that we could allow, but no-one implemented yet. There could be some implementation issues with finding the right context for the where-block, though.<br><br></div><div>cheers,<br></div><div>Jesper<br></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Thu, Nov 26, 2015 at 3:57 AM, Peter Selinger <span dir="ltr"><<a href="mailto:selinger@mathstat.dal.ca" target="_blank">selinger@mathstat.dal.ca</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Dear Agda list,<br>
<br>
my question/comment is about Agda's syntax. One thing that regularly<br>
confounds me is that there are certain places where I am forced to use<br>
"let" and other places where I am forced to use "where". Sometimes<br>
they are the same places, so that I can't use anything and have to<br>
work around it in some ugly way, like with explicit lambda<br>
abstractions or awkward parenthesized nested let expressions.<br>
Some examples follow.<br>
<br>
My questions are: (1) is there some syntactic trick that I am not<br>
aware of, which would actually let me write the code as I want to<br>
write it? (2) If not, could I please request for Agda's syntax to be<br>
rationalized so that every declaration that can be used with "let"<br>
can also be used with "where", and vice versa?<br>
<br>
Agda version 2.4.2.4<br>
<br>
First, an example of something that works with "let" but not "where":<br>
<br>
This works:<br>
<br>
example =<br>
let<br>
(ih1 , ih2) = lemma<br>
in<br>
bla-bla-bla<br>
<br>
This does not work:<br>
<br>
example = bla-bla-bla<br>
where<br>
(ih1 , ih2) = lemma<br>
<br>
-- ERROR: Missing type signature for left hand side (ih1 , ih2)<br>
<br>
The error message indicates that the type signature is<br>
missing. However, if we try to add it:<br>
<br>
example = bla-bla-bla<br>
where<br>
(ih1 , ih2) : some-type ∧ some-other-type<br>
(ih1 , ih2) = lemma<br>
<br>
-- ERROR: Illegal name in type signature: (ih1 , ih2)<br>
<br>
example = bla-bla-bla<br>
where<br>
ih1 : some-type<br>
ih2 : some-other-type<br>
(ih1 , ih2) = lemma<br>
<br>
-- ERROR: More than one matching type signature for left hand side<br>
<br>
As a matter of fact, adding a type signature in this situation is not<br>
possible with "let" either; the error message are the same if I try:<br>
<br>
example =<br>
let<br>
(ih1 , ih2) : some-type ∧ some-other-type<br>
(ih1 , ih2) = lemma<br>
in<br>
bla-bla-bla<br>
<br>
-- ERROR: Illegal name in type signature: (ih1 , ih2)<br>
<br>
example =<br>
let<br>
ih1 : some-type<br>
ih2 : some-other-type<br>
(ih1 , ih2) = lemma<br>
in<br>
bla-bla-bla<br>
<br>
-- ERROR: More than one matching type signature for left hand side<br>
<br>
Is there some trick that I am not aware of for how one can supply a<br>
type signature when the left-hand side of a declaration uses a<br>
constructor? Please note that I am aware of the solution<br>
<br>
example = bla-bla-bla<br>
where<br>
ih1 : some-type<br>
ih1 = fst lemma<br>
<br>
ih2 : some-other-type<br>
ih2 = snd lemma<br>
<br>
but it is what I would consider an ugly workaround. I am also aware<br>
that let-bindings of the form "let (x , y) = blah" only work with<br>
record types, i.e., types that have a unique constructor (there is no<br>
pattern-matching "let" as far as I am aware); however, it is not clear<br>
to me why the same restriction could not be applied to a "where".<br>
<br>
Next, an example of something that works with "where" but not with<br>
"let":<br>
<br>
This works:<br>
<br>
example = bla-bla-bla<br>
where<br>
g : A -> B<br>
g a = some-term h a<br>
where<br>
h : C -> D<br>
h c = some-other-term<br>
<br>
In other words, you can attach a "where" to a local function<br>
definition that appears in another where-clause.<br>
<br>
However, this does not work:<br>
<br>
example x =<br>
let<br>
g : A -> B<br>
g a = some-term h a<br>
where<br>
h : C -> D<br>
h c = some-other-term<br>
in<br>
bla-bla-bla<br>
<br>
-- ERROR: Not a valid let-declaration<br>
<br>
So it is apparently not possible to add a local where-clause to a<br>
function definition, if the definition happens to be part of a<br>
let-construct rather than a where-construct. I cannot think of any<br>
reason why this should be so.<br>
<br>
Finally, here is a concrete example of a proof one might reasonably<br>
want to write, where neither "let" nor "where" nor any combination<br>
thereof seems to do exactly the right thing.<br>
<br>
-- ----------------------------------------------------------------------<br>
-- Start of code<br>
<br>
-- Pairs.<br>
record _∧_ (x y : Set) : Set where<br>
constructor _,_<br>
field<br>
fst : x<br>
snd : y<br>
<br>
open _∧_<br>
<br>
-- Some inductive type.<br>
data A : Set where<br>
c1 : A<br>
c2 : A -> A<br>
<br>
-- Some postulates to keep the example small.<br>
postulate<br>
Property1 : A -> Set<br>
base-case1 : Property1 c1<br>
induction-step1 : ∀ x -> Property1 x -> Property1 (c2 x)<br>
<br>
B C : Set<br>
some-function : C -> B<br>
Property2 : A -> B -> Set<br>
base-case2 : ∀ y -> Property2 c1 y<br>
induction-step2 : ∀ x y -> (∀ c → Property2 x (some-function c)) -> Property2 (c2 x) y<br>
<br>
module Attempt1 where<br>
<br>
-- I believe that this code is very reasonable. We prove multiple<br>
-- properties by induction. It makes sense to first state the<br>
-- multiple induction hypotheses, then derive various consequences,<br>
-- including the induction claims. However, this code does not<br>
-- type-check or even parse.<br>
<br>
lemma : ∀ x -> Property1 x ∧ (∀ y -> Property2 x y)<br>
lemma c1 = (base-case1 , base-case2)<br>
lemma (c2 x) = (claim1 , claim2)<br>
where<br>
(ih1 , ih2) = lemma x<br>
<br>
claim1 : Property1 (c2 x)<br>
claim1 = induction-step1 x ih1<br>
<br>
claim2 : ∀ y -> Property2 (c2 x) y<br>
claim2 y = induction-step2 x y f<br>
where<br>
f : ∀ c -> Property2 x (some-function c)<br>
f c = ih2 (some-function c)<br>
<br>
-- ERROR: Missing type signature for left hand side (ih1 , ih2)<br>
<br>
module Attempt2 where<br>
<br>
-- Fine. I'll change the "where" to a "let", although it is less<br>
-- readable. However, this still does not parse; this time because<br>
-- the local "where" clause in claim2 is rejected.<br>
<br>
lemma : ∀ x -> Property1 x ∧ (∀ y -> Property2 x y)<br>
lemma c1 = (base-case1 , base-case2)<br>
lemma (c2 x) =<br>
let<br>
(ih1 , ih2) = lemma x<br>
<br>
claim1 : Property1 (c2 x)<br>
claim1 = induction-step1 x ih1<br>
<br>
claim2 : ∀ y -> Property2 (c2 x) y<br>
claim2 y = induction-step2 x y f<br>
where<br>
f c = ih2 (some-function c)<br>
<br>
in<br>
(claim1 , claim2)<br>
<br>
-- ERROR: Not a valid let-declaration<br>
<br>
module Attempt3 where<br>
<br>
-- Finally, I am stuck with having to convert the inferior clause of<br>
claim2 to a "let" as well. This makes the whole thing even less<br>
elegant. Moreover, this would not work at all if the function f<br>
were recursive, or if either of claim1 or claim2 where recursive<br>
(because "let" bindings cannot be used for recursive functions).<br>
<br>
lemma : ∀ x -> Property1 x ∧ (∀ y -> Property2 x y)<br>
lemma c1 = (base-case1 , base-case2)<br>
lemma (c2 x) =<br>
let<br>
(ih1 , ih2) = lemma x<br>
<br>
claim1 : Property1 (c2 x)<br>
claim1 = induction-step1 x ih1<br>
<br>
claim2 : ∀ y -> Property2 (c2 x) y<br>
claim2 y =<br>
let<br>
f c = ih2 (some-function c)<br>
in<br>
induction-step2 x y f<br>
in<br>
(claim1 , claim2)<br>
<br>
-- End of code<br>
-- ----------------------------------------------------------------------<br>
<br>
<br>
In general, I do not like the use of "let" in situations like this,<br>
because if either claim1 or claim2 of f happens to need a recursive<br>
definition, the "let" will not allow it. So if you need both<br>
<br>
(ih1 , ih2) = lemma x<br>
<br>
and a recursive function<br>
<br>
claim x = something-recursive<br>
<br>
in the same proof, there is basically no syntax that will work, or is<br>
there? It doesn't seem possible to combine "let" and "where" either,<br>
as in<br>
<br>
example =<br>
let<br>
something = lemma<br>
in<br>
something-else<br>
where<br>
claim = some-proof<br>
<br>
Why is this so messy? In my opinion, the simplest solution would be to<br>
allow things like<br>
<br>
...<br>
where<br>
(ih1 , ih2) = lemma<br>
<br>
Is there some compelling reason why it is not allowed?<br>
<br>
Thanks, -- Peter<br>
<br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div><br></div>