[Agda] trouble with let and where
Andreas Abel
abela at chalmers.se
Mon Nov 30 14:26:53 CET 2015
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/
More information about the Agda
mailing list