<div dir="ltr">Hi Peter,<br><div><br>In my understanding, the difference between &#39;let&#39; and &#39;where&#39; is that the first defines expressions while the second one contains function definitions. This means that allowing &quot;(x , y)&quot; in the left-hand side of something in a where block would be ambiguous: it could mean that you&#39;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&#39;re defining a new function called x with two arguments called &quot;,&quot; and &quot;y&quot; 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 &quot;missing type signature for the left-hand side&quot;: Agda expects you to give a type signature for this function &quot;x&quot; 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">&lt;<a href="mailto:selinger@mathstat.dal.ca" target="_blank">selinger@mathstat.dal.ca</a>&gt;</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&#39;s syntax. One thing that regularly<br>
confounds me is that there are certain places where I am forced to use<br>
&quot;let&quot; and other places where I am forced to use &quot;where&quot;. Sometimes<br>
they are the same places, so that I can&#39;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&#39;s syntax to be<br>
rationalized so that every declaration that can be used with &quot;let&quot;<br>
can also be used with &quot;where&quot;, and vice versa?<br>
<br>
Agda version 2.4.2.4<br>
<br>
First, an example of something that works with &quot;let&quot; but not &quot;where&quot;:<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 &quot;let&quot; 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 &quot;let (x , y) = blah&quot; only work with<br>
record types, i.e., types that have a unique constructor (there is no<br>
pattern-matching &quot;let&quot; as far as I am aware); however, it is not clear<br>
to me why the same restriction could not be applied to a &quot;where&quot;.<br>
<br>
Next, an example of something that works with &quot;where&quot; but not with<br>
&quot;let&quot;:<br>
<br>
This works:<br>
<br>
  example = bla-bla-bla<br>
    where<br>
      g : A -&gt; B<br>
      g a = some-term h a<br>
        where<br>
          h : C -&gt; D<br>
          h c = some-other-term<br>
<br>
In other words, you can attach a &quot;where&quot; 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 -&gt; B<br>
      g a = some-term h a<br>
        where<br>
          h : C -&gt; 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 &quot;let&quot; nor &quot;where&quot; 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 -&gt; A<br>
<br>
-- Some postulates to keep the example small.<br>
postulate<br>
  Property1 : A -&gt; Set<br>
  base-case1 : Property1 c1<br>
  induction-step1 : ∀ x -&gt; Property1 x -&gt; Property1 (c2 x)<br>
<br>
  B C : Set<br>
  some-function : C -&gt; B<br>
  Property2 : A -&gt; B -&gt; Set<br>
  base-case2 : ∀ y -&gt; Property2 c1 y<br>
  induction-step2 : ∀ x y -&gt; (∀ c → Property2 x (some-function c)) -&gt; 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 -&gt; Property1 x ∧ (∀ y -&gt; 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 -&gt; Property2 (c2 x) y<br>
      claim2 y = induction-step2 x y f<br>
        where<br>
          f : ∀ c -&gt; 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&#39;ll change the &quot;where&quot; to a &quot;let&quot;, although it is less<br>
  -- readable. However, this still does not parse; this time because<br>
  -- the local &quot;where&quot; clause in claim2 is rejected.<br>
<br>
  lemma : ∀ x -&gt; Property1 x ∧ (∀ y -&gt; 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 -&gt; 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 &quot;let&quot; 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 &quot;let&quot; bindings cannot be used for recursive functions).<br>
<br>
  lemma : ∀ x -&gt; Property1 x ∧ (∀ y -&gt; 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 -&gt; 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 &quot;let&quot; in situations like this,<br>
because if either claim1 or claim2 of f happens to need a recursive<br>
definition, the &quot;let&quot; 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&#39;t seem possible to combine &quot;let&quot; and &quot;where&quot; 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>