[Agda] Meeting about Agda

[Andreas Abel]

Catarina Coquand wrote:
> The first meeting will be next Wednesday at 13.15. Since it is the first 
> meeting I will be so unpolite that I decide
> what to be discussed.

I think that is not impolite at all.  It is very necessary that someone 
thinks ahead and structures the meeting such that the meeting time can 
be effectively used.  Thanks for doing that, Catarina.

> 1. Syntax of hidden arguments, classes/signatures, newtype. People has 
> started to use this so we
> urgently need to decide on the syntax.

It would be nice if you put out some suggestions before the meeting 
which we can think about and then maybe just accept during the meeting.

Concering hidden arguments I have the following suggestion:  The current 
syntax is quite good, but still a bit inconsistent.

Composition 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, for instance.

==> Suggestion:  Do not use "|->" at all.  Indicate hiding only in the 
"telescope style", by prefixing variables with "|".  In case of 
non-dependent function types, one can prefix the domain and write

id :: (|A :: Set) -> |A -> A
   = \ (|A :: Set) -> \ (|a :: A) -> a

What is the suggestion for a class/instance syntax?

Cheers,
Andreas

-- 
Andreas Abel  <><      --<>--     Du bist der geliebte Mensch.

Dept. of Computer Science,   Chalmers University of Technology
Rännvägen 6, rum 5111A, 41296 Göteborg, SWEDEN, +46-31-7721006