Guarded Impredicativity

[Alejandro Serrano Mena]

Hi,

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

> I just tried it and it doesn't currently work.
>
> [1 of 1] Compiling Id               ( Id.hs, interpreted )
>
> Id.hs:14:7: error:
>     • Couldn't match type ‘a0 -> a0’ with ‘forall a. a -> a’
>       Expected type: TExpQ (forall a. a -> a)
>         Actual type: Q (TExp (a0 -> a0))
>     • In the Template Haskell quotation [|| id ||]
>       In the expression: [|| id ||]
>       In an equation for ‘foo’: foo = [|| id ||]
>    |
> 14 | foo = [|| id ||]
>    |
>
> Do you think you could perhaps take a look into fixing it?
>

I will give it a try.

>
> PS: If you disable the testsuite on CI (so that the build passes) then
> people can download and use the artefacts from your branch rather than
> have to build the compiler from source.
>

Is there an easy way to do this (or a tutorial), better in a way which
doesn't break the actual CI pipeline if this is finally merged?

Regards,
Alejandro

>
>
> On Fri, Jun 28, 2019 at 1:20 PM Alejandro Serrano Mena
> <trupill at gmail.com> wrote:
> >
> > 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/821996d5/attachment.html>