Guarded Impredicativity

Alejandro Serrano Mena trupill at gmail.com
Fri Jun 28 13:57:55 UTC 2019


Yes, this is one of the features we would like to have. If you write down
the explicit instantiation of a function, we just take it, no questions
asked (well, the terms should still be type correct).
But writing out *every* single impredicative instantiation is really
tiresome, hence we are looking for "simple" ways to flow this information
around and alleavite a bit the burden.

El vie., 28 jun. 2019 a las 15:43, Ryan Scott (<ryan.gl.scott at gmail.com>)
escribió:

> Would this permit explicit impredicativity as described in [1]? Simon
> mentions in [1] that explicit impredicativity is easier to implement than
> guarded impredicativity, although it's not clear to me if the latter would
> imply the former.
>
> Ryan S.
> -----
> [1] https://gitlab.haskell.org/ghc/ghc/issues/14859
> _______________________________________________
> ghc-devs mailing list
> ghc-devs at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20190628/13bf8d95/attachment.html>


More information about the ghc-devs mailing list