Guarded Impredicativity

[Alejandro Serrano Mena]

No, up to now the only changes are in the type checking of applications and
variables.
However, I guess that it would be possible to give [| id |] the type Code
(forall a. a -> a) with a explicit type signature (the system always allows
impredicative instantiation is explicitly marked), but without the
annotation it would the usual type forall a. Code (a -> a).

El vie., 28 jun. 2019 a las 14:17, Matthew Pickering (<
matthewtpickering at gmail.com>) escribió:

> Have you modified how typed quotations are type checked? For example,
> with your patch I would hope that
>
> [| id |] :: Code (forall a . a -> a)
>
> would be accepted?
>
> I'll try it out. This patch will have big ramifications for the typed
> template haskell community.
>
> Matt
>
> On Fri, Jun 28, 2019 at 1:12 PM Alejandro Serrano Mena
> <trupill at gmail.com> wrote:
> >
> > Dear all,
> >
> > We are trying to bring back `ImpredicativeTypes` into GHC by using the
> ideas in the "Guarded Impredicative Polymorphism" paper [
> https://www.microsoft.com/en-us/research/publication/guarded-impredicative-polymorphism/
> ].
> >
> > For now I have produced a first attempt, which lives in
> https://gitlab.haskell.org/trupill/ghc. It would be great if those
> interested in impredicative polymorphism could give it a try and see
> whether it works as expected or not.
> >
> > The main idea behing "guarded impredicativity" is that you can infer an
> impredicative instantiation for a type variable in a function call if you
> have at least one given argument where that type variable appears under a
> type constructor different from (->).
> > For example, consider the call `(\x -> x) : ids`, where `ids :: [forall
> a. a -> a]`. Since in the type of `(:)`, namely `forall a. a -> [a] ->
> [a]`, the variable `a` appears under the `[]` constructor and that second
> argument is given, we are allowed to instantiate `a := forall a. a -> a`.
> On the other hand, if we try to do `ids <> ids`, where `(<>)` is monoid
> concatenation with type `forall m. Monoid m => m -> m -> m`, we are forced
> to instantiate `m` with a not-polymorphic type because at no point the
> variable appears under a type constructor.
> >
> > Just for reference, the best to get a working clone is to follow these
> steps:
> > > git clone --recursive https://gitlab.haskell.org/ghc/ghc
> impredicative-ghc
> > > cd impredicative-ghc
> > > git remote add trupill git at gitlab.haskell.org:trupill/ghc.git
> > > git fetch trupill
> > > git checkout trupill master
> >
> > Thanks very much in advance,
> > Alejandro
> >
> > _______________________________________________
> > 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/d775ba78/attachment.html>