[Agda] trouble with let and where

[Sergei Meshveliani]

On Wed, 2015-11-25 at 22:57 -0400, Peter Selinger 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)
> [..]


1) Personally, I have converged to the following style.
If I am going to use a pattern matching of kind  
<construct x y z ...> = (foo ..)   
in the function body (in order to extract the result parts from
(foo ...)),
then I use  let -- in  for the whole function. And inside this block,
`where' does not work. 

This approach works on practice, after one gets used to this.

2) map (\ (cons x y (c z)) -> f x y z) ts
can be replaced with
   map (\t -> let (cons x y (c z)) = t in f x y z) ts.

3) Question to the language developers:

how does this occur that in Haskell it is much simpler to replace `let'
with `where' ? 

Regards,

------
Sergei