[Agda] moving common from `with'

[Andreas Abel]

Agda's 'where' and 'let' are a bit different to Haskell's.  'where' is 
for joining declarations, like in

   decl
     where
       decls

'let' is for local declarations in an expression, like in

   let
     letdecls
   in expression

The main difference is that letdecls are only a subset of decls, like 
you can only have

    var : A
    var = expression
    pattern = expression
    open module-expression

Also, 'let's are immediately expanded (not a good design choice, we are 
aware of that, but easy to implement), whereas 'where' (and also 'with') 
generate proper function definitions.

The syntax for pattern matching lambda is

   \lambda { (pattern -> expression)* }

thus, there is no place to put a 'where' there.  Haskell's 'where' can 
also be used in expressions.  But it allows funny stuff like

   a = let x = 5
       in  x where x = 4

Well, I could not tell whether the value of a should be 4 or 5 here...

Adding 'where' to expressions has beend requested before...

Cheers,
Andreas

On 13.10.12 7:06 PM, Serge D. Mechveliani wrote:
> On Fri, Oct 12, 2012 at 08:10:52PM +0200, Andreas Abel wrote:
>> I'd ditch the with in favor of a case with a pattern-matching lambda for
>> your example.
>>
>> open import Data.Nat
>> open import Function
>> open import Relation.Nullary
>>
>> f' : Nat -> Nat -> Nat
>> f' m n = case m <=? n of
>>           \lambda { (yes _) -> g (suc m)
>>                   ; (no  _) -> g (suc n)
>>                   }
>>                   where
>>                   g : Nat -> Nat
>>                   g m = m + m + 1
>
> (I replaced the math symbols in this citation -- SM).
>
> As to `case', consinder the variant
>
>    f : Nat -> Nat -> Nat
>    f m n = case  m :: (m + n) :: []  of \lambda
>            {
>              (0 :: _)      -> g (suc m)
>            ; (1 :: v :: _) -> g (n + 2 * a)  where
>                                              a = v + v * v
>            ; _             -> g (suc n)
>            }
>            where
>            g : Nat -> Nat
>            g m = m + m + 1
>
> It is not type-checked in  Agda-2.3.0.1 + MAlonzo + lib-0.6 :
> the `where' inside `case' is rejected.
> It can be replaced with `let'.
> But I recall, it is said somewhere that, generally, `let' is not so
> well supported in Agda as `where' (do I recall right?).
>
> Regards,
> Sergei
>
>
>
>

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/