[Agda] Notes from Agda meeting

[Catarina Coquand]

Dear all,

at the last meeting we discussed the following:

- the syntax of hidden args
- the syntax of classes
- fixity decls
- Catarina presented the implementation of hidden args.

Andreas presented well the problem with the current syntax

omposition in telescope style currently looks like

comp1a (|A,|B,|C :: Set) (f :: B -> C) (g :: A -> B) :: A -> C
  = \ (x::A) -> f (g x)

which is fine.  Unfortunately, when you turn this into Pi-style you 
cannot write

comp1b :: (|A,|B,|C :: Set) -> (f :: B -> C) -> (g :: A -> B) -> A -> C
  = \ (|A,|B,|C :: Set) -> \ (f :: B -> C) -> \ (g :: A -> B) ->
    \ (x::A) -> f (g x)

since the current parser demands "|->" notation for hidden abstraction, 
so you need to write

comp1c :: (A,B,C :: Set) |-> (f :: B -> C) -> (g :: A -> B) -> A -> C
  = \ (A,B,C :: Set) |-> \ (f :: B -> C) -> \ (g :: A -> B) ->
    \ (x::A) -> f (g x)

instead.  This, however, does not scale to mixed (hidden and non-hidden) 
telescopes, like

comp2a (A,|B,C :: Set) (f :: B -> C) (g :: A -> B) :: A -> C
  = \ (x::A) -> f (g x)

One has to break up the common quantification of A B and C and write

comp2c :: (A :: Set) -> (B :: Set) |-> (C :: Set) ->
   (f :: B -> C) -> (g :: A -> B) -> A -> C
  = \ (A :: Set) -> (B :: Set) |-> (C :: Set) ->
    \ (f :: B -> C) -> \ (g :: A -> B) ->
    \ (x::A) -> f (g x)

The problem is the "|->" arrow.  It cannot be used with multiple 
quantification; what should

  (A,|B,C :: Set) |->

mean?

Andreas suggested to remove the |-> arrow  and  to  instead write 
(|A::Set) -> |A -> A. We
discussed that this coul be hard to read, e.g. |C |A -> A is maybe a bit 
strange to read even
though it parses.

Our suggestion was to allow
(A,|B,C :: Set)  -> C
(A,B,C :: Set)  |-> C

and disallow
(A,|B,C :: Set)  |-> C
and report about amiguous hiding. Since this involves some implemenation 
work it might
take some time before it's implemented.


---

For the syntax of classes we did not decide on much. Questions was if 
classes/instances should
be visibly identified  with signatures and records. If not, one needs to 
find special syntax for
non-default possibly overlapping instances.


-----

We also discussed how to declare fixity, Catarina and Ulf discussed 
continued the
discussion afterwards and suggest to do it as in Haskell knowing that 
it's not an
ideal solution but not having any better solution.



Catarina