CODEWITHSUNDEEP
agda
nicolas
nicolas

Reputation: 9815

nicer way to write constructors as function in Agda

I have a list 

data List (X : Set) : Set where
  <>   : List X
  _,_  : X -> List X -> List X

a definition for equality

data _==_ {l}{X : Set l}(x : X) : X -> Set l where
  refl : x == x

and congruence 

cong : forall {k l}{X : Set k}{Y : Set l}(f : X -> Y){x y} -> x == y -> f x == f y
cong f refl = refl

I am trying to prove 

propFlatten2 : {X : Set } ( xs0 : List X ) (x : X)  (xs1 : List X) (xs2 : List X)
              -> ( xs0 ++ x , xs1 ) ++ xs2  ==  xs0 ++ (x , xs1 ++ xs2 )
propFlatten2 <> x xs1 xs2 = refl
propFlatten2 (x , xs0) x₁ xs1 xs2 =   cong (λ l -> x , l) {!!}

Is there a better way to use directly the constructor _,_ other than through a lambda in the last line ?

Upvotes: 4

Views: 248

Answers (1)

Vitus
Vitus

Reputation: 11922

Agda doesn't have any special syntax for partial application of operators. You can, however, use the operators in their usual prefix version:

x + y = _+_ x y

This is convenient when you need to partially apply leftmost argument(s):

_+_ 1 = λ x → 1 + x

When you need to partially apply arguments going from the right, your options are more limited. As mentioned in the comments, you could use one of the convenience functions such as flip (found in Function):

flip f x y = f y x  -- Type omitted for brevity.

And then simply flip the arguments of _+_:

flip _+_ 1 = λ x → x + 1

Sometimes you find operators whose only purpose is to make the code a bit nicer. Best example I can think of is probably Data.Product.,_. When you write a dependent pair (Data.Product.Σ), sometimes the first part of the pair can be filled in automatically. Instead of writing:

_ , x

You can just write:

, x

It's hard to say when writing a specialized operator such as the one above is actually worth it; if your only use case is using it with congruence, I'd just stick with the lambda since it makes it very clear what's going on.

Upvotes: 2

Related Questions