[Agda] I want implicit coercions in Agda

[Miëtek Bak]

Martin Odersky is proposing to get rid of implicits in Scala 3.  I would like to draw your attention to the following quote:

“… most applications of implicit conversions have turned out to be of dubious value. The problem is that many newcomers to the language start with defining implicit conversions since they are easy to understand and seem powerful and convenient. … But the problem remains that syntactically, conversions and values just look too similar for comfort.”

https://github.com/lampepfl/dotty/pull/5458

Personally, I found implicit conversions greatly increase the difficulty of understanding other people’s code, and I would be happier if they did not make their way into Agda.

-- 
(mb)


On Fri, Nov 9, 2018, at 08:37, Jesper Cockx wrote:
> 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
> >
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda