[Agda] trouble with let and where

[Peter Selinger]

Andreas Abel wrote:
> 
> Hi Peter & folks,
> 
> [...] 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

Yes, please! Such a piece of syntactic sugar would be greatly
appreciated. Image a use case like

  where
    (x , y , z , u , v , w) = complicated-induction-hypothesis

and how it would look if we had to put in the "fst"s and "snd"s
manually!

> [...] 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'.

Some restricted version of this is already permitted. At least, I
don't get any errors from this:

data A : Set where
  a : A

g : A -> A
g x =
  let f : A -> A
      f x = x
  in f a
	  
I assume it is being desugared to

  let f : A -> A
      f = (\x -> x)
  in f a

However, if it not possible for such a "let f x =" to (a) be defined
by pattern matching, (b) to have a subservient "where" clause, or (c)
to be recursive. I think (c) is on purpose, given that such a "let" is
desugared to a lambda abstraction and then a substitution. But there
is no reason in principle why (a) and (b) could not be possible
anyway. I like your point that such a definition could be handled
semantically as if it had been dropped into a local anonymous module. 

> Maybe 'let' was never systematically developed to include as much 
> features as possible...

It already seems to include a fair amount :)

-- Peter