[Agda] trouble with let and where

[Jesper Cockx]

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 =
>     let
>       (ih1 , ih2) = lemma
>     in
>       bla-bla-bla
>
> This does not work:
>
>   example = bla-bla-bla
>     where
>       (ih1 , ih2) = 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 = bla-bla-bla
>     where
>       (ih1 , ih2) : some-type ∧ some-other-type
>       (ih1 , ih2) = lemma
>
>   -- ERROR: Illegal name in type signature: (ih1 , ih2)
>
>   example = bla-bla-bla
>     where
>       ih1 : some-type
>       ih2 : some-other-type
>       (ih1 , ih2) = 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 =
>     let
>       (ih1 , ih2) : some-type ∧ some-other-type
>       (ih1 , ih2) = lemma
>     in
>       bla-bla-bla
>
>   -- ERROR: Illegal name in type signature: (ih1 , ih2)
>
>   example =
>     let
>       ih1 : some-type
>       ih2 : some-other-type
>       (ih1 , ih2) = 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 = bla-bla-bla
>     where
>       ih1 : some-type
>       ih1 = fst lemma
>
>       ih2 : some-other-type
>       ih2 = 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) = 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 = bla-bla-bla
>     where
>       g : A -> B
>       g a = some-term h a
>         where
>           h : C -> D
>           h c = 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 =
>     let
>       g : A -> B
>       g a = some-term h a
>         where
>           h : C -> D
>           h c = 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 _∧_ (x y : Set) : Set where
>   constructor _,_
>   field
>     fst : x
>     snd : y
>
> open _∧_
>
> -- 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 : ∀ x -> Property1 x -> Property1 (c2 x)
>
>   B C : Set
>   some-function : C -> B
>   Property2 : A -> B -> Set
>   base-case2 : ∀ y -> Property2 c1 y
>   induction-step2 : ∀ x y -> (∀ c → 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 : ∀ x -> Property1 x ∧ (∀ y -> Property2 x y)
>   lemma c1 = (base-case1 , base-case2)
>   lemma (c2 x) = (claim1 , claim2)
>     where
>       (ih1 , ih2) = lemma x
>
>       claim1 : Property1 (c2 x)
>       claim1 = induction-step1 x ih1
>
>       claim2 : ∀ y -> Property2 (c2 x) y
>       claim2 y = induction-step2 x y f
>         where
>           f : ∀ c -> Property2 x (some-function c)
>           f c = 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 : ∀ x -> Property1 x ∧ (∀ y -> Property2 x y)
>   lemma c1 = (base-case1 , base-case2)
>   lemma (c2 x) =
>     let
>       (ih1 , ih2) = lemma x
>
>       claim1 : Property1 (c2 x)
>       claim1 = induction-step1 x ih1
>
>       claim2 : ∀ y -> Property2 (c2 x) y
>       claim2 y = induction-step2 x y f
>         where
>           f c = 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 : ∀ x -> Property1 x ∧ (∀ y -> Property2 x y)
>   lemma c1 = (base-case1 , base-case2)
>   lemma (c2 x) =
>     let
>       (ih1 , ih2) = lemma x
>
>       claim1 : Property1 (c2 x)
>       claim1 = induction-step1 x ih1
>
>       claim2 : ∀ y -> Property2 (c2 x) y
>       claim2 y =
>         let
>           f c = 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) = lemma x
>
> and a recursive function
>
>       claim x = 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 =
>     let
>       something = lemma
>     in
>       something-else
>         where
>           claim = some-proof
>
> Why is this so messy? In my opinion, the simplest solution would be to
> allow things like
>
>   ...
>     where
>       (ih1 , ih2) = 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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20151126/47e3b4c5/attachment-0001.html