[Agda] trouble with let and where
Thorsten Altenkirch
Thorsten.Altenkirch at nottingham.ac.uk
Mon Nov 30 16:01:50 CET 2015
Maybe the real question is: how can we reduce let and where to the same thing? Since it seems that where is more general that means can we reduce let to where?
I guess the problem is that where is only applicable at top level while we can use let inside a term,
Sent from my iPhone
> On 30 Nov 2015, at 13:26, Andreas Abel <abela at chalmers.se> wrote:
>
> Hi Peter & folks,
>
> the reason that `let` and `where` are so different is that they have an entirely different semantics in Agda.
>
> * `let` is a term constructor which is nothing more than a (possibly type annotated) substitution;
>
> let x = e in e'
>
> behaves like e'[e/x].
>
> Irrefutable pattern matches are translated to projections:
>
> let (x , y) = e in e'
>
> is nothing but
>
> let x = fst e
> y = snd e
> in e'
>
> * `where` takes a bunch of declarations and attaches them to the lhs of a declaration. (Internally, each `where` creates an anonymous module.)
>
> Like for top-level declarations, the definitions can be grouped such that each group defines a single new symbol by (co)pattern matching. This symbol must have a type signature if the definition is anything more complicated than an alias.
>
> x = e
>
> In contrast to `let`, which is just a substitution, `where` actually introduces new names that are associated with a bunch of reductions.
>
> To implement your suggestion,
>
> where
> (x , y) = e
>
> we could do similar as for `let` and interpret this as
>
> where
> x,y = e -- x,y is a private identifier for sharing e's evaluation
> x = fst x,y
> y = snd x,y
>
> This is not the whole story though. There is also
>
> let open M args in e
>
> which creates an anonymous module and brings its contents into scope in e. In the light of this, I do not see a principal problem to also allow definitions by pattern matching like
>
> let f : ...
> f ps = body
> in e'
>
> in lets. They could also create an anonymous module which contains the definition of f to be used in e'.
>
> Maybe 'let' was never systematically developed to include as much features as possible...
>
> Cheers,
> Andreas
>
>> On 26.11.2015 14:44, Peter Selinger wrote:
>> 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
>
> --
> Andreas Abel <>< Du bist der geliebte Mensch.
>
> Department of Computer Science and Engineering
> Chalmers and Gothenburg University, Sweden
>
> andreas.abel at gu.se
> http://www2.tcs.ifi.lmu.de/~abel/
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please send it back to me, and immediately delete it.
Please do not use, copy or disclose the information contained in this
message or in any attachment. Any views or opinions expressed by the
author of this email do not necessarily reflect the views of the
University of Nottingham.
This message has been checked for viruses but the contents of an
attachment may still contain software viruses which could damage your
computer system, you are advised to perform your own checks. Email
communications with the University of Nottingham may be monitored as
permitted by UK legislation.
More information about the Agda
mailing list