[Agda] Location of implicit argument(s)

[Jean-Philippe Bernardy]

On Fri, Nov 20, 2009 at 1:03 PM, Dan Licata <drl at cs.cmu.edu> wrote:

> I often find myself wishing for this in Agda; e.g. when I have
>
> Lam : forall {G A B} -> Term (A :: G) B -> Term G (A imp B)
>
> I want to write
>
> f (Lam (e : Term (A :: G) B)) = ...
>
> for
>
> f (Lam{G}{A}{B} e) = ...
>
> The reason is that the former saves me from having to remember what
> order the implicit arguments come in (when there's a lot of them, I have
> to keep flipping back to the definition of the datatype).
>
> Could such a syntax be made to work for Agda?

How about this encoding?

_typed_ : (A : Set) (a : A) -> A
A typed a = a

data X : Set where
  x : X

test = (X -> X) typed (\a -> a)


The order might be somewhat confusing though. I came up with
this (somewhat disappointing) hack to restore traditional order:


type_ : (A : Set) -> (a : A) -> A
type_ A  = λ a → a

_:::_ : {A B : Set} -> (a : A) (f : A -> B) -> B
a ::: f = f a


test1 = (\a -> a) ::: type (X -> X)


Cheers,
JP.