[Agda] I want implicit coercions in Agda

[Jesper Cockx]

I think this is related to the problem of subtyping / cumulativity. The
reasons why we don't have it are also similar: a combination of

1. Lack of manpower
2. A rather large codebase which makes many implicit assumptions about the
internal state, so any major change usually requires a lot of refactoring
3. Existing literature on these subjects often omits details crucial to the
implementation, such as how it interacts with metavariables and constraint
solving
4. Concerns about adding too much feature bloat to Agda, making it harder
to maintain and making the move towards an eventual core language more
difficult

That being said, having implicit coercions would certainly be very nice in
many situations, so it would be great if someone would do the experiment to
add them to Agda.

An interesting comment in the Agda source code (TypeChecking.Conversion):

-- | @coerce v a b@ coerces @v : a@ to type @b@, returning a @v' : b@
> --   with maybe extra hidden applications or hidden abstractions.
> --
> --   In principle, this function can host coercive subtyping, but
> --   currently it only tries to fix problems with hidden function types.
>

If someone is interested in giving it a try then that'd maybe be a good
place to start.

-- Jesper

On Thu, Nov 8, 2018 at 9:16 PM Martin Escardo <m.escardo at cs.bham.ac.uk>
wrote:

> ... and I am sure many other people do too.
>
> Many other proof assistants have them.
>
> Is there a philosophical reason for that, or is this something that just
> hasn't been done yet?
>
> Real-life mathematics has them in abundance, and it would be nice to
> reflect this in Agda.
>
> I would like to press for a design and implementation of this in Agda. :-)
>
> Best,
> Martin
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20181109/5e8bef5d/attachment.html>