[Agda] tuple patterns

[Nils Anders Danielsson]

On 2012-09-21 21:18, Serge D. Mechveliani wrote:
> I. Is it reliable to write  ->  instead of  \arrow ?

If you've encountered a problem, please report a bug.

> II. Tuple patterns.
>
> Writing nested `with' often reduces readability.
> So I try tuple patterns, similar as in Haskell. For example,
>
>    f : Nat -> Nat
>    f m   with  (3 <=? m , m <=? 6)    -- : Dec (3 <= m) x Dec (m <= 6)
>    ... | (no _ , _    ) = 1
>    ... | (_ ,    yes _) = 2
>    ... | _              = 3
>
> (For this letter I replace  \bn -> Nat,  \<=  ->  <=,  \lambda -> \lam).
>
> And it is not parsed in  Agda-2.3.0.1.

Not parsed? I suspect that your problem is that Agda cannot infer the
type of (3 <=? m , m <=? 6). If you use _,′_ instead of _,_, then you
make the life a bit easier for the unification engine.

In this case I suggest that you use the following notation instead,
though:

   f : Nat -> Nat
   f m with 3 <=? m | m <=? 6
   ... | no _ | _     = 1
   ... | _    | yes _ = 2
   ... | _    |       = 3

> I expect that `with' is a language construct, and `case' is a library
> function (are they?).

Yes.

> 2. How to avoid introducing an extra variable (`pair') ?

See above.

> III. In-place type denotations.
>
> For example, the expression
>                            f ((1 , 2) : Nat x Nat) ((3 , 4) : Nat x Nat)
> is easier to write/read than
>
>    let p1 : Nat x Nat
>        p1 = (1 , 2)
>        p2 : Nat x Nat
>        p2 = (1 , 2)
>    in  f p1 p2
>
> (two variables introduced, and 4 extra lines).
> It is desirable for the language and compiler to allow the former.

You can define your own type ascription operator:

   type-signature : ∀ {a} (A : Set a) → A → A
   type-signature A x = x

   syntax type-signature A x = x of-type A

However, this operator cannot be called ':', and it doesn't work in
patterns, so perhaps this functionality should be built-in.

-- 
/NAD