[Agda] I want implicit coercions in Agda

[Guillaume Allais]

I agree with Martin that it was important to make the point that
because a feature can be abused, that does not mean it shouldn't
be implemented. I can mimic some of Coq's canonical structures
mechanisms using REWRITE in a perverse way. That doesn't invalidate
all the practical use-cases for it.

Anyway, here is my use-case:

In agdarsec, I have a □ type constructor which corresponds to guarded
recursive calls. Users are given a fixpoint combinator but to be able
to guarantee that all parsers are total, they are only allowed to use
the recursive call in a guarded manner.

Various combinators' types make explicit the fact that some of their
arguments will be guarded. E.g. conjunction:
_<&>_ : ∀[ Parser P A ⇒ □ Parser P B ⇒ Parser P (A × B) ]

Now, that is both crucial and boring. Crucial for totality but boring
from the point of view of the computational behaviour of the function.
It is pretty annoying to have to explicitly wrap non-guarded values
in the guarded modality by using `box : ∀[ Parser P A ⇒ □ Parser P A ]`.

In Idris and Coq I declare `box` as an implicit coercion and whenever
the checker expects a `□ Parser P A` but got a `Parser P A` then it
inserts a call to `box` and keeps checking the rest of the term. This
allows me to write Haskell-looking parsers while getting Agda-strong
guarantees on totality.

IIRC it works well in Coq but I have gotten weird error messages in
Idris where the system was a bit too eager to introduce these and end
up with a type error in a state hard to understand. I wouldn't mind if,
as described informally earlier, they were only introduced if we *know*
they are going to make the term match (as a first approximation: there
are no open metas in the checked & inferred type).

As is the case in Coq & Idris, I would not expect coercions to be chained.
If there is more than one candidate, the coercion should fail (with maybe
a pragma to allow overlap).


On 18/11/2018 21:35, Ulf Norell wrote:
> On Sun, Nov 18, 2018 at 9:12 PM Martin Escardo <m.escardo at cs.bham.ac.uk>
> wrote:
> 
>>
>> You will not solve the shortcomings of my mathematical style by refusing
>> to implement implicit coercion in Agda.
>>
> 
> I feel that the discussion has derailed a little at this point. The issue
> isn't that some people
> are stubbornly refusing to implement this one simple thing that would make
> life easier for
> the practising mathematician. The problem is that implicit coercions are
> very difficult to get
> right. To move this discussion forward I suggest that you give some of the
> following:
> 
> - concrete examples of implicit coercions that you'd like to see
> - a rough sketch of how they are to be solved
> - references to the proof assistants that (in your opinion) have gotten
> implicit coercions right
> - some notes on why instance arguments are not a good replacement for
> implicit coercions
> 
> / Ulf
> 
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
> 

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: OpenPGP digital signature
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20181119/85f6ccb3/attachment.sig>