[Agda] New: Syntax for let pattern bindings

[Wolfram Kahl]

On Tue, Jun 05, 2012 at 04:22:51PM +0200, Andreas Abel wrote:
>
> I am proud to announce a small addition to Agda syntax.  Record patterns 
> can now be bound to values with a 'let'.
> 
> For instance, Data.List.splitAt can now be written as
> 
>   splitAt : ∀ {a} {A : Set a} → ℕ → List A → (List A × List A)
>   ...
>   splitAt (suc n) (x ∷ xs) =
>     let (ys , zs) = splitAt n xs
>     in  (x ∷ ys , zs)
> 
> instead of using a 'with'.

YES!! THANK YOU!!!


> Internally, this is treated as
> 
>   let ys = proj₁ (splitAt n xs)
>       zs = proj₂ (splitAt n xs)
>   in  ...
> 
> so be careful if you want to actually run your Agda programs.  You might 
> involuntarily slip from linear into exponential time.
> 
> A better internal handling of let-bindings that would allow the treatment
> 
>   let t  = splitAt n xs
>       ys = proj₁ t
>       zs = proj₂ t
>   in  ...
> 
> is an open issue.

Open in which sense?

 * Unknown whether possible (in general)?
 * Considered possible, but not planned?
 * Easy, but just not done yet?


Thank you very much again for getting started with this ---
I have beeen considering not having pattern bindings as a major shortcoming
(and recently measured that ``with'' as an alternative is just
 forbiddingly slow (for type-checking)).


Wolfram