[Agda] trouble with let and where
Peter Selinger
selinger at mathstat.dal.ca
Thu Nov 26 14:44:13 CET 2015
Hi Jesper,
thanks for your explanation, but I don't think your point is
valid. Agda does permit and understand all of the following:
record And (x y : Set) : Set where
constructor pair
field
fst : x
snd : y
open And
postulate
A B C : Set
lemma1 : And A B
lemma2 : A -> B -> C
something : C
something =
let
pair x y = lemma1
func z w = lemma2 z w
in
func x y
This shows that Agda has no trouble distinguishing between the
left-hand side "pair x y", which is a constructor applied to two
arguments x and y (and therefore defines x y), and the left-hand side
"func z w", which is a non-constructor applied to z and w (and
therefore defines func). In fact, even the syntax highlighter gets
this distinction, and contrary to what you wrote, there is no
ambiguity.
The problem is not with infix notation either. The following, why
strange looking, is understood perfectly well by Agda:
record And (x y : Set) : Set where
constructor _,_
field
fst' : x
snd' : y
open And
postulate
A B C : Set
lemma1 : And A B
lemma2 : A -> B -> C
something : C
something =
let
(x , y) = lemma1
(z ,' w) = lemma2 ,' w
in
z x y
Here, the left-hand side "(x , y)" is correctly understood as the
constructor _,_ applied to two arguments x and y, and the left-hand
side "(z ,' w)" is correctly understood as the non-constructor z
applied to two arguments ,' and w.
So I think what you wrote is not correct: the problem is not one of
syntactic ambiguity. If Agda has no difficult parsing "pair x y" and
"func x y" on the left-hand side of a let-definition, then there is no
*syntactic* difficulty with parsing them on the left-hand side of a
where-definition either. It then seems rather arbitrary that it is not
allowed.
I therefore renew my request that
where
(x , y) = lemma1
should be permitted! -- Peter
Jesper Cockx wrote:
>
> Hi Peter,
>
> 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.
>
> 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.
>
> cheers,
> Jesper
>
> On Thu, Nov 26, 2015 at 3:57 AM, Peter Selinger <selinger at mathstat.dal.ca>
> wrote:
>
> > Dear Agda list,
> >
> > my question/comment is about Agda's syntax. One thing that regularly
> > confounds me is that there are certain places where I am forced to use
> > "let" and other places where I am forced to use "where". Sometimes
> > they are the same places, so that I can't use anything and have to
> > work around it in some ugly way, like with explicit lambda
> > abstractions or awkward parenthesized nested let expressions.
> > Some examples follow.
> >
> > My questions are: (1) is there some syntactic trick that I am not
> > aware of, which would actually let me write the code as I want to
> > write it? (2) If not, could I please request for Agda's syntax to be
> > rationalized so that every declaration that can be used with "let"
> > can also be used with "where", and vice versa?
> >
> > Agda version 2.4.2.4
> >
> > First, an example of something that works with "let" but not "where":
> >
> > This works:
> >
> > example =3D
> > let
> > (ih1 , ih2) =3D lemma
> > in
> > bla-bla-bla
> >
> > This does not work:
> >
> > example =3D bla-bla-bla
> > where
> > (ih1 , ih2) =3D lemma
> >
> > -- ERROR: Missing type signature for left hand side (ih1 , ih2)
> >
> > The error message indicates that the type signature is
> > missing. However, if we try to add it:
> >
> > example =3D bla-bla-bla
> > where
> > (ih1 , ih2) : some-type =E2=88=A7 some-other-type
> > (ih1 , ih2) =3D lemma
> >
> > -- ERROR: Illegal name in type signature: (ih1 , ih2)
> >
> > example =3D bla-bla-bla
> > where
> > ih1 : some-type
> > ih2 : some-other-type
> > (ih1 , ih2) =3D lemma
> >
> > -- ERROR: More than one matching type signature for left hand side
> >
> > As a matter of fact, adding a type signature in this situation is not
> > possible with "let" either; the error message are the same if I try:
> >
> > example =3D
> > let
> > (ih1 , ih2) : some-type =E2=88=A7 some-other-type
> > (ih1 , ih2) =3D lemma
> > in
> > bla-bla-bla
> >
> > -- ERROR: Illegal name in type signature: (ih1 , ih2)
> >
> > example =3D
> > let
> > ih1 : some-type
> > ih2 : some-other-type
> > (ih1 , ih2) =3D lemma
> > in
> > bla-bla-bla
> >
> > -- ERROR: More than one matching type signature for left hand side
> >
> > Is there some trick that I am not aware of for how one can supply a
> > type signature when the left-hand side of a declaration uses a
> > constructor? Please note that I am aware of the solution
> >
> > example =3D bla-bla-bla
> > where
> > ih1 : some-type
> > ih1 =3D fst lemma
> >
> > ih2 : some-other-type
> > ih2 =3D snd lemma
> >
> > but it is what I would consider an ugly workaround. I am also aware
> > that let-bindings of the form "let (x , y) =3D blah" only work with
> > record types, i.e., types that have a unique constructor (there is no
> > pattern-matching "let" as far as I am aware); however, it is not clear
> > to me why the same restriction could not be applied to a "where".
> >
> > Next, an example of something that works with "where" but not with
> > "let":
> >
> > This works:
> >
> > example =3D bla-bla-bla
> > where
> > g : A -> B
> > g a =3D some-term h a
> > where
> > h : C -> D
> > h c =3D some-other-term
> >
> > In other words, you can attach a "where" to a local function
> > definition that appears in another where-clause.
> >
> > However, this does not work:
> >
> > example x =3D
> > let
> > g : A -> B
> > g a =3D some-term h a
> > where
> > h : C -> D
> > h c =3D some-other-term
> > in
> > bla-bla-bla
> >
> > -- ERROR: Not a valid let-declaration
> >
> > So it is apparently not possible to add a local where-clause to a
> > function definition, if the definition happens to be part of a
> > let-construct rather than a where-construct. I cannot think of any
> > reason why this should be so.
> >
> > Finally, here is a concrete example of a proof one might reasonably
> > want to write, where neither "let" nor "where" nor any combination
> > thereof seems to do exactly the right thing.
> >
> > -- ----------------------------------------------------------------------
> > -- Start of code
> >
> > -- Pairs.
> > record _=E2=88=A7_ (x y : Set) : Set where
> > constructor _,_
> > field
> > fst : x
> > snd : y
> >
> > open _=E2=88=A7_
> >
> > -- Some inductive type.
> > data A : Set where
> > c1 : A
> > c2 : A -> A
> >
> > -- Some postulates to keep the example small.
> > postulate
> > Property1 : A -> Set
> > base-case1 : Property1 c1
> > induction-step1 : =E2=88=80 x -> Property1 x -> Property1 (c2 x)
> >
> > B C : Set
> > some-function : C -> B
> > Property2 : A -> B -> Set
> > base-case2 : =E2=88=80 y -> Property2 c1 y
> > induction-step2 : =E2=88=80 x y -> (=E2=88=80 c =E2=86=92 Property2 x (=
> some-function c)) ->
> > Property2 (c2 x) y
> >
> > module Attempt1 where
> >
> > -- I believe that this code is very reasonable. We prove multiple
> > -- properties by induction. It makes sense to first state the
> > -- multiple induction hypotheses, then derive various consequences,
> > -- including the induction claims. However, this code does not
> > -- type-check or even parse.
> >
> > lemma : =E2=88=80 x -> Property1 x =E2=88=A7 (=E2=88=80 y -> Property2 =
> x y)
> > lemma c1 =3D (base-case1 , base-case2)
> > lemma (c2 x) =3D (claim1 , claim2)
> > where
> > (ih1 , ih2) =3D lemma x
> >
> > claim1 : Property1 (c2 x)
> > claim1 =3D induction-step1 x ih1
> >
> > claim2 : =E2=88=80 y -> Property2 (c2 x) y
> > claim2 y =3D induction-step2 x y f
> > where
> > f : =E2=88=80 c -> Property2 x (some-function c)
> > f c =3D ih2 (some-function c)
> >
> > -- ERROR: Missing type signature for left hand side (ih1 , ih2)
> >
> > module Attempt2 where
> >
> > -- Fine. I'll change the "where" to a "let", although it is less
> > -- readable. However, this still does not parse; this time because
> > -- the local "where" clause in claim2 is rejected.
> >
> > lemma : =E2=88=80 x -> Property1 x =E2=88=A7 (=E2=88=80 y -> Property2 =
> x y)
> > lemma c1 =3D (base-case1 , base-case2)
> > lemma (c2 x) =3D
> > let
> > (ih1 , ih2) =3D lemma x
> >
> > claim1 : Property1 (c2 x)
> > claim1 =3D induction-step1 x ih1
> >
> > claim2 : =E2=88=80 y -> Property2 (c2 x) y
> > claim2 y =3D induction-step2 x y f
> > where
> > f c =3D ih2 (some-function c)
> >
> > in
> > (claim1 , claim2)
> >
> > -- ERROR: Not a valid let-declaration
> >
> > module Attempt3 where
> >
> > -- Finally, I am stuck with having to convert the inferior clause of
> > claim2 to a "let" as well. This makes the whole thing even less
> > elegant. Moreover, this would not work at all if the function f
> > were recursive, or if either of claim1 or claim2 where recursive
> > (because "let" bindings cannot be used for recursive functions).
> >
> > lemma : =E2=88=80 x -> Property1 x =E2=88=A7 (=E2=88=80 y -> Property2 =
> x y)
> > lemma c1 =3D (base-case1 , base-case2)
> > lemma (c2 x) =3D
> > let
> > (ih1 , ih2) =3D lemma x
> >
> > claim1 : Property1 (c2 x)
> > claim1 =3D induction-step1 x ih1
> >
> > claim2 : =E2=88=80 y -> Property2 (c2 x) y
> > claim2 y =3D
> > let
> > f c =3D ih2 (some-function c)
> > in
> > induction-step2 x y f
> > in
> > (claim1 , claim2)
> >
> > -- End of code
> > -- ----------------------------------------------------------------------
> >
> >
> > In general, I do not like the use of "let" in situations like this,
> > because if either claim1 or claim2 of f happens to need a recursive
> > definition, the "let" will not allow it. So if you need both
> >
> > (ih1 , ih2) =3D lemma x
> >
> > and a recursive function
> >
> > claim x =3D something-recursive
> >
> > in the same proof, there is basically no syntax that will work, or is
> > there? It doesn't seem possible to combine "let" and "where" either,
> > as in
> >
> > example =3D
> > let
> > something =3D lemma
> > in
> > something-else
> > where
> > claim =3D some-proof
> >
> > Why is this so messy? In my opinion, the simplest solution would be to
> > allow things like
> >
> > ...
> > where
> > (ih1 , ih2) =3D lemma
> >
> > Is there some compelling reason why it is not allowed?
> >
> > Thanks, -- Peter
> >
> > _______________________________________________
> > Agda mailing list
> > Agda at lists.chalmers.se
> > https://lists.chalmers.se/mailman/listinfo/agda
> >
>
> --001a1134f0d64763bf05256efd31
> Content-Type: text/html; charset="UTF-8"
> Content-Transfer-Encoding: quoted-printable
>
> <meta http-equiv=3D"Content-Type" content=3D"text/html; charset=3Dutf-8"><d=
> iv dir=3D"ltr">Hi Peter,<br><div><br>In my understanding, the difference be=
> tween 'let' and 'where' is that the first defines expressions while the sec=
> ond one contains function definitions. This means that allowing "(x , =
> y)" in the left-hand side of something in a where block would be ambig=
> uous: it could mean that you're defining two values x and y as the first an=
> d 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 "," a=
> nd "y" respectively. I know this second interpretation seems comp=
> letely absurd, but Agda has no way to know that. This is also why you get t=
> he 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 (w=
> here blocks are not allowed in a let expression) seems like something that =
> we could allow, but no-one implemented yet. There could be some implementat=
> ion 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=3D"gma=
> il_extra"><br><div class=3D"gmail_quote">On Thu, Nov 26, 2015 at 3:57 AM, P=
> eter Selinger <span dir=3D"ltr"><<a href=3D"mailto:selinger at mathstat.dal=
> .ca" target=3D"_blank">selinger at mathstat.dal.ca</a>></span> wrote:<br><b=
> lockquote class=3D"gmail_quote" style=3D"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 &quo=
> t;where":<br>
> <br>
> This works:<br>
> <br>
> example =3D<br>
> let<br>
> (ih1 , ih2) =3D lemma<br>
> in<br>
> bla-bla-bla<br>
> <br>
> This does not work:<br>
> <br>
> example =3D bla-bla-bla<br>
> where<br>
> (ih1 , ih2) =3D 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 =3D bla-bla-bla<br>
> where<br>
> (ih1 , ih2) : some-type =E2=88=A7 some-other-type<br>
> (ih1 , ih2) =3D lemma<br>
> <br>
> -- ERROR: Illegal name in type signature: (ih1 , ih2)<br>
> <br>
> example =3D bla-bla-bla<br>
> where<br>
> ih1 : some-type<br>
> ih2 : some-other-type<br>
> (ih1 , ih2) =3D lemma<br>
> <br>
> -- ERROR: More than one matching type signature for left hand side<b=
> r>
> <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 t=
> ry:<br>
> <br>
> example =3D<br>
> let<br>
> (ih1 , ih2) : some-type =E2=88=A7 some-other-type<br>
> (ih1 , ih2) =3D lemma<br>
> in<br>
> bla-bla-bla<br>
> <br>
> -- ERROR: Illegal name in type signature: (ih1 , ih2)<br>
> <br>
> example =3D<br>
> let<br>
> ih1 : some-type<br>
> ih2 : some-other-type<br>
> (ih1 , ih2) =3D lemma<br>
> in<br>
> bla-bla-bla<br>
> <br>
> -- ERROR: More than one matching type signature for left hand side<b=
> r>
> <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 =3D bla-bla-bla<br>
> where<br>
> ih1 : some-type<br>
> ih1 =3D fst lemma<br>
> <br>
> ih2 : some-other-type<br>
> ih2 =3D 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) =3D blah" only work wi=
> th<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 wit=
> h<br>
> "let":<br>
> <br>
> This works:<br>
> <br>
> example =3D bla-bla-bla<br>
> where<br>
> g : A -> B<br>
> g a =3D some-term h a<br>
> where<br>
> h : C -> D<br>
> h c =3D 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 =3D<br>
> let<br>
> g : A -> B<br>
> g a =3D some-term h a<br>
> where<br>
> h : C -> D<br>
> h c =3D 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>
> -- ----------------------------------------------------------------------<b=
> r>
> -- Start of code<br>
> <br>
> -- Pairs.<br>
> record _=E2=88=A7_ (x y : Set) : Set where<br>
> constructor _,_<br>
> field<br>
> fst : x<br>
> snd : y<br>
> <br>
> open _=E2=88=A7_<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 : =E2=88=80 x -> Property1 x -> Property1 (c2 =
> x)<br>
> <br>
> B C : Set<br>
> some-function : C -> B<br>
> Property2 : A -> B -> Set<br>
> base-case2 : =E2=88=80 y -> Property2 c1 y<br>
> induction-step2 : =E2=88=80 x y -> (=E2=88=80 c =E2=86=92 Propert=
> y2 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 : =E2=88=80 x -> Property1 x =E2=88=A7 (=E2=88=80 y -> P=
> roperty2 x y)<br>
> lemma c1 =3D (base-case1 , base-case2)<br>
> lemma (c2 x) =3D (claim1 , claim2)<br>
> where<br>
> (ih1 , ih2) =3D lemma x<br>
> <br>
> claim1 : Property1 (c2 x)<br>
> claim1 =3D induction-step1 x ih1<br>
> <br>
> claim2 : =E2=88=80 y -> Property2 (c2 x) y<br>
> claim2 y =3D induction-step2 x y f<br>
> where<br>
> f : =E2=88=80 c -> Property2 x (some-=
> function c)<br>
> f c =3D 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", alt=
> hough it is less<br>
> -- readable. However, this still does not parse; this time because<b=
> r>
> -- the local "where" clause in claim2 is rejected.<br>
> <br>
> lemma : =E2=88=80 x -> Property1 x =E2=88=A7 (=E2=88=80 y -> P=
> roperty2 x y)<br>
> lemma c1 =3D (base-case1 , base-case2)<br>
> lemma (c2 x) =3D<br>
> let<br>
> (ih1 , ih2) =3D lemma x<br>
> <br>
> claim1 : Property1 (c2 x)<br>
> claim1 =3D induction-step1 x ih1<br>
> <br>
> claim2 : =E2=88=80 y -> Property2 (c2 x) y<br>
> claim2 y =3D induction-step2 x y f<br>
> where<br>
> f c =3D 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 who=
> le thing even less<br>
> elegant. Moreover, this would not work at all if the fu=
> nction f<br>
> were recursive, or if either of claim1 or claim2 where =
> recursive<br>
> (because "let" bindings cannot be used for re=
> cursive functions).<br>
> <br>
> lemma : =E2=88=80 x -> Property1 x =E2=88=A7 (=E2=88=80 y -> P=
> roperty2 x y)<br>
> lemma c1 =3D (base-case1 , base-case2)<br>
> lemma (c2 x) =3D<br>
> let<br>
> (ih1 , ih2) =3D lemma x<br>
> <br>
> claim1 : Property1 (c2 x)<br>
> claim1 =3D induction-step1 x ih1<br>
> <br>
> claim2 : =E2=88=80 y -> Property2 (c2 x) y<br>
> claim2 y =3D<br>
> let<br>
> f c =3D ih2 (some-function c)<br>
> in<br>
> induction-step2 x y f<br>
> in<br>
> (claim1 , claim2)<br>
> <br>
> -- End of code<br>
> -- ----------------------------------------------------------------------<b=
> r>
> <br>
> <br>
> In general, I do not like the use of "let" in situations like thi=
> s,<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) =3D lemma x<br>
> <br>
> and a recursive function<br>
> <br>
> claim x =3D 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&=
> quot; either,<br>
> as in<br>
> <br>
> example =3D<br>
> let<br>
> something =3D lemma<br>
> in<br>
> something-else<br>
> where<br>
> claim =3D 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) =3D 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=3D"mailto:Agda at lists.chalmers.se">Agda at lists.chalmers.se</a><br>
> <a href=3D"https://lists.chalmers.se/mailman/listinfo/agda" rel=3D"noreferr=
> er" target=3D"_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><b=
> r>
> </blockquote></div><br></div>
>
> --001a1134f0d64763bf05256efd31--
>
More information about the Agda
mailing list