[Agda] trouble with let and where

[Peter Selinger]

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