[Agda] message of parameterized

[Andreas Abel]

Hello Serge,

On 06.09.12 3:35 PM, Serge D. Mechveliani wrote:
> I have two suggestions for the compiler and one note.
>
> 1. If a function  foo  is imported from a  parameterized module  Foo,
>     and the compiler reports something about the _arguments_ for  foo,
>     then it has sense to add to the report:
>     "For any occasion: mind that the module  Foo  has parameters".
>
> Motivation
> ----------
> Consider the code
>   plus : Op2 Nat
>   plus = Data.Nat._+_
>   CommPlus : Set _
>   CommPlus = Algebra.FunctionProperties.Commutative plus
>
> (under Agda-2.3.0.1, lib-0.6,
>   and for this letter I replace
>                Op\_2 with Op2,  \bn  with  Nat,  \equiv  with  _==_
> ).
> The report is
>   "Nat !=< (Set _5) of type Set
>    when checking that the expression plus has type Rel Nat _5
>   "
> I have a bit more complex code, which I have reduced to this one,
> trying to debug the program.
> why it needs  Rel Nat _5  instead of  Op2 Nat  ?
> At this point I have been puzzling for 1 hour, intil dicovered
> (only by occasion!) that the module  Algebra.FunctionProperties  is
> parameterized.
> So, one probably needs to write  Commutative _==_ _+_
> in this situation rather than    Commutative _+_
>
> A programmer sees in the library sources
>               `Commutative : Op2 A -> Set _',   `Commutative _+_', ...,

At this point, the programmer should wonder about a seemingly unbound 
identifier `A' in the type signature of Commutative and a go looking for 
its origin.  Then he would finally arive at the module header.

> and it is difficult to guess that there might be needed an additional
> argument to insert.
>
> Probably, parameterized modules are good. But they present a certain bug
> farm, so it has sense for the compiler to provide a help.
>
> 2. A minor suggestion:
>     a code piece in a message will be easier to read if it is surrounded
>     either with a pair quotes or extra blanks:
>
>    checking that the expression plus has type Rel Nat _5 foo foo ...
>    -->
>    checking that the expression `plus' has type `Rel Nat _5' foo foo ...

We cannot used quotation marks since they are allowed in identifiers.

Maybe a different color would be best.

> 3. A note on `view'.
>     I nice TRW logical language  Maude  has a very different notion of
> `view'
> (it also has parameterized modules, and the fixity denotations like
> `_f__ :',  `if_then_else : ...').
> As I recall, a view there is a module map produced by instantiating
> sorts for module parameters.

Cheers,
Andreas

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

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/