Call for Talks: Haskell Implementors' Workshop 2022

[Alejandro Serrano Mena]

(apologies for multiple copies of this message)

ACM SIGPLAN Haskell Implementors' Workshop
https://icfp22.sigplan.org/home/hiw-2022
Ljubljana, Slovenia, 11 September 2022

Co-located with ICFP 2022
https://icfp22.sigplan.org/

Important dates
---

Deadline: 11 July, 2022 (AoE)
Notification: 11 August, 2022
Workshop: 11 September, 2022

The 14th Haskell Implementors' Workshop is to be held alongside ICFP
2022 this year in Ljubljana. It is a forum for people involved in the
design and development of Haskell implementations, tools, libraries,
and supporting infrastructure, to share their work and discuss future
directions and collaborations with others.

Talks and/or demos are proposed by submitting an abstract, and
selected by a small program committee. There will be no published
proceedings. The workshop will be informal and interactive, with
open spaces in the timetable and room for ad-hoc discussion, demos,
and lightning short talks.

Scope and target audience
-

It is important to distinguish the Haskell Implementors' Workshop from
the Haskell Symposium which is also co-located with ICFP 2022. The
Haskell Symposium is for the publication of Haskell-related research. In
contrast, the Haskell Implementors' Workshop will have no proceedings --
although we will aim to make talk videos, slides and presented data
available with the consent of the speakers.

The Implementors' Workshop is an ideal place to describe a Haskell
extension, describe works-in-progress, demo a new Haskell-related tool,
or even propose future lines of Haskell development. Members of the
wider Haskell community encouraged to attend the workshop -- we need
your feedback to keep the Haskell ecosystem thriving. Students working
with Haskell are specially encouraged to share their work.

The scope covers any of the following topics. There may be some topics
that people feel we've missed, so by all means submit a proposal even if
it doesn't fit exactly into one of these buckets:

* Compilation techniques
* Language features and extensions
* Type system implementation
* Concurrency and parallelism: language design and implementation
* Performance, optimisation and benchmarking
* Virtual machines and run-time systems
* Libraries and tools for development or deployment

Talks
-

We invite proposals from potential speakers for talks and
demonstrations. We are aiming for 20-minute talks with 5 minutes for
questions and changeovers. We want to hear from people writing
compilers, tools, or libraries, people with cool ideas for directions in
which we should take the platform, proposals for new features to be
implemented, and half-baked crazy ideas. Please submit a talk title and
abstract of no more than 300 words.

Submissions can be made via HotCRP at https://icfphiw22.hotcrp.com
until July 11th (anywhere on earth).

We will also have lightning talks session. These have been very well
received in recent years, and we aim to increase the time available to
them. Lightning talks be ~7mins and are scheduled on the day of the
workshop. Suggested topics for lightning talks are to present a single
idea, a work-in-progress project, a problem to intrigue and perplex
Haskell implementors, or simply to ask for feedback and collaborators.

Program Committee
-

* Pepe Iborra (Meta)
* Gabrielle Keller (Utrecht University)
* Emily Pilmore (Kadena)
* Vladislav Zavialov (Serokell)
* Alejandro Serrano (Tweag)

Contact
---

* Alejandro Serrano 
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Re: Re[4]: Strictness/demand info for a Name

[Alejandro Serrano Mena]

Nice, so only I get the corresponding IdInfo, my work is “done”. But I’m
still missing how to thread everything together. Right now, what I have to
work with are:

   - The HieAst node I am searching information about, from which I can get
   the name,
   - The result of the parsing, renaming, and type checking phases.

Is there a way, with that information only, to obtain the corresponding
IdInfo? (This might be a very simple question, or just have a negative
answer, but I’m not versed at all in how all this information flows within
GHC).

Thanks in advance,
Alejandro

El 13 ene 2022 16:50:01, Sebastian Graf  escribió:

> Yes, every imported identifier from a module that was compiled with
> optimisations should have the proper analysis information in its IdInfo.
> So if you have `base` somewhere in one of your compiled libraries and load
> it, then the identifier of `GHC.OldList.map` will have an `idDmdSig` that
> says it's strict in the list parameter.
>
> At least that's how it works in GHC, where these IdInfos are populated
> with the information from the loaded interface files. The situation with
> HLS might be different, although I wouldn't expect that.
>
> -- Originalnachricht --
> Von: "Alejandro Serrano Mena" 
> An: "Sebastian Graf" 
> Cc: "GHC developers" ; "Matthew Pickering" <
> matthewtpicker...@gmail.com>
> Gesendet: 13.01.2022 16:43:50
> Betreff: Re: Re[2]: Strictness/demand info for a Name
>
> Thanks for the pointers! :)
>
> Knowing this, let me maybe rephrase my question: is it possible to get
> demand information of identifiers *without* running the analysis itself?
>
> Alejandro
>
> El 13 ene 2022 15:45:29, Sebastian Graf  escribió:
>
>> Yes, Matt is right.
>>
>> `dmdSigInfo` describes the how a function Id uses its arguments and free
>> variables, whereas
>> `demandInfo` describes how a (local, mostly) Id is used.
>>
>> Note that if you wanted to go beyond type-checking, you could probably
>> run the analysis on the desugaring of the current module quite easily.
>> But the results would be misleading, as prior optimisations (that you
>> probably don't want to run) may arrange the program in a way that demand
>> analysis has an easier time.
>>
>> -- Originalnachricht --
>> Von: "Matthew Pickering" 
>> An: "Alejandro Serrano Mena" 
>> Cc: "GHC developers" 
>> Gesendet: 13.01.2022 15:38:29
>> Betreff: Re: Strictness/demand info for a Name
>>
>> You look at `dmdSigInfo` in `IdInfo`.
>>
>>
>> Matt
>>
>>
>> On Thu, Jan 13, 2022 at 2:20 PM Alejandro Serrano Mena
>>
>>  wrote:
>>
>> >
>>
>> >  Dear all,
>>
>> >
>>
>> >  I’m trying to bring the information about demand and strictness to the
>> Haskell Language Server, but I cannot find a way to do so. I was wondering
>> whether you could help me :)
>>
>> >
>>
>> >  Here’s my understanding; please correct me if I’m wrong:
>>
>> >
>>
>> >  The analysis runs on Core, so getting this information for the current
>> file would require to run the compiler further than type checking, which is
>> quite expensive,
>>
>> >  However, this analysis should somehow use known information about
>> imported functions, which should be readily available somewhere,
>>
>> >  If the above is true, what is the simplest way to get the information
>> for imported things? As I mentioned above, I would prefer not to run the
>> compiler further than the type checking phase, since otherwise it gets too
>> expensive for IDE usage. Right now HLS uses the information from the .hie
>> files.
>>
>> >
>>
>> >
>>
>> >  In fact, this goes into the more general question of how to show
>> information from different analyses within the IDE; I guess solving the
>> case for strictness/analysis may open the door to more (maybe everything
>> recorded inside a `Id`?)
>>
>> >
>>
>> >  Regards,
>>
>> >  Alejandro
>>
>> >  ___
>>
>> >  ghc-devs mailing list
>>
>> >ghc-devs@haskell.org
>>
>> >http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>>
>> ___
>>
>> ghc-devs mailing list
>>
>> ghc-devs@haskell.org
>>
>> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>>
>>
>>
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Re: Re[2]: Strictness/demand info for a Name

[Alejandro Serrano Mena]

Thanks for the pointers! :)

Knowing this, let me maybe rephrase my question: is it possible to get
demand information of identifiers *without* running the analysis itself?

Alejandro

El 13 ene 2022 15:45:29, Sebastian Graf  escribió:

> Yes, Matt is right.
>
> `dmdSigInfo` describes the how a function Id uses its arguments and free
> variables, whereas
> `demandInfo` describes how a (local, mostly) Id is used.
>
> Note that if you wanted to go beyond type-checking, you could probably
> run the analysis on the desugaring of the current module quite easily.
> But the results would be misleading, as prior optimisations (that you
> probably don't want to run) may arrange the program in a way that demand
> analysis has an easier time.
>
> -- Originalnachricht ------
> Von: "Matthew Pickering" 
> An: "Alejandro Serrano Mena" 
> Cc: "GHC developers" 
> Gesendet: 13.01.2022 15:38:29
> Betreff: Re: Strictness/demand info for a Name
>
> You look at `dmdSigInfo` in `IdInfo`.
>
>
> Matt
>
>
> On Thu, Jan 13, 2022 at 2:20 PM Alejandro Serrano Mena
>
>  wrote:
>
> >
>
> >  Dear all,
>
> >
>
> >  I’m trying to bring the information about demand and strictness to the
> Haskell Language Server, but I cannot find a way to do so. I was wondering
> whether you could help me :)
>
> >
>
> >  Here’s my understanding; please correct me if I’m wrong:
>
> >
>
> >  The analysis runs on Core, so getting this information for the current
> file would require to run the compiler further than type checking, which is
> quite expensive,
>
> >  However, this analysis should somehow use known information about
> imported functions, which should be readily available somewhere,
>
> >  If the above is true, what is the simplest way to get the information
> for imported things? As I mentioned above, I would prefer not to run the
> compiler further than the type checking phase, since otherwise it gets too
> expensive for IDE usage. Right now HLS uses the information from the .hie
> files.
>
> >
>
> >
>
> >  In fact, this goes into the more general question of how to show
> information from different analyses within the IDE; I guess solving the
> case for strictness/analysis may open the door to more (maybe everything
> recorded inside a `Id`?)
>
> >
>
> >  Regards,
>
> >  Alejandro
>
> >  ___
>
> >  ghc-devs mailing list
>
> >ghc-devs@haskell.org
>
> >http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>
> ___
>
> ghc-devs mailing list
>
> ghc-devs@haskell.org
>
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>
>
>
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Strictness/demand info for a Name

[Alejandro Serrano Mena]

Dear all,

I’m trying to bring the information about demand and strictness to the
Haskell Language Server, but I cannot find a way to do so. I was wondering
whether you could help me :)

Here’s my understanding; please correct me if I’m wrong:

   - The analysis runs on Core, so getting this information for the current
   file would require to run the compiler further than type checking, which is
   quite expensive,
   - However, this analysis should somehow use known information about
   imported functions, which should be readily available somewhere,
   - If the above is true, what is the simplest way to get the information
   for imported things? As I mentioned above, I would prefer not to run the
   compiler further than the type checking phase, since otherwise it gets too
   expensive for IDE usage. Right now HLS uses the information from the .hie
   files.


In fact, this goes into the more general question of how to show
information from different analyses within the IDE; I guess solving the
case for strictness/analysis may open the door to more (maybe everything
recorded inside a `Id`?)

Regards,
Alejandro
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Re: Quick Look has landed

[Alejandro Serrano Mena]

Awesome news! Thanks so much, Simon, for all the programming effort you've
put into this :)

Alejandro

El jue., 24 sept. 2020 a las 22:04, Dimitrios Vytiniotis (<
dimit...@gmail.com>) escribió:

> Wow this is great news!!! We finally landed something acceptable after 15
> years Thanks so much for all the hard work on the implementation side
> Alejandro and Simon.
>
> On Thu, 24 Sep 2020, 21:21 Simon Peyton Jones, 
> wrote:
>
>> Dimitrios, Jurriaan, Alejandro
>>
>> I’m happy to tell you that Quick Look has landed on GHC’s master branch.
>>
>> It’ll be in GHC 9.2, but is usable already by building HEAD.  Good work!
>>
>> The implementation is very faithful to the paper, which was an invaluable
>> guide.
>>
>> Simon
>>
>
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Uppercase OverloadedLabels

[Alejandro Serrano Mena]

Dear Haskell-Café / GHC devs,
Is there any reason why the `OverloadedHaskell` extension does not work
with labels starting with an uppercase letter?

Kind regards,
Alejandro
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Re: Find constraints over type

[Alejandro Serrano Mena]

My goal is to add type information on hover within `ghcide`. Right now,
when you select a variable, we give back the type as reported in the
corresponding Var. However, when this type involved a type variable, it
misses a lot of important information about the typing context in which we
are working. So the goal is to report back some of this typing context.

Going back to my original example:

f :: Eq a => [a] -> Bool
f xs = xs == []

It would be great if by hovering over the 'xs', one would get '[a] where Eq
a', or some other representation of the known constraints.

Since this is intended to be a help for the programmer, it doesn't really
matter whether we get "too many" constraints (for example, if we had "Ord
a" it's OK to get "Eq a" too, since that's interesting constraint
information).

Right now I am working with TypecheckModules most of the time.

Regards,
Alejandro

El jue., 16 ene. 2020 a las 19:47, Simon Peyton Jones (<
simo...@microsoft.com>) escribió:

> There is definitely no pure way to get from ‘a’ to its constraints.
>
>- It is far from clear what “its constraints” are.   Is (C a b) such a
>constraint?  C [a] b?  What about superclasses?
>- Constraints vary depending on where  you are.  GADT matches can
>bring into scope extra constraints on existing type variables.
>
>
>
> So as Ben says, to give a sensible response you’ll need to explain more
> about your goal
>
>
>
> Simon
>
>
>
> *From:* ghc-devs  *On Behalf Of *Alejandro
> Serrano Mena
> *Sent:* 16 January 2020 16:19
> *To:* GHC developers 
> *Subject:* Find constraints over type
>
>
>
> Dear GHC devs,
>
> I am trying to figure out a way to obtain the constraints that hold over a
> type. Let me give you an example: suppose that I write the following
> function:
>
>
>
> f :: Eq a => [a] -> Bool
>
> f xs = xs == []
>
>
>
> If I ask for the type of the Var ' xs', I get back '[a]'. This is correct,
> but I am missing the crucial information that '[a]' must be Eq.
>
>
>
> Is there an easy way to get it? It seems that 'varType' doesn't give me
> enough information.
>
>
>
> Regards,
>
> Alejandro
>
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Find constraints over type

[Alejandro Serrano Mena]

Dear GHC devs,
I am trying to figure out a way to obtain the constraints that hold over a
type. Let me give you an example: suppose that I write the following
function:

f :: Eq a => [a] -> Bool
f xs = xs == []

If I ask for the type of the Var ' xs', I get back '[a]'. This is correct,
but I am missing the crucial information that '[a]' must be Eq.

Is there an easy way to get it? It seems that 'varType' doesn't give me
enough information.

Regards,
Alejandro
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Working in my own branch with changes in submodules

[Alejandro Serrano Mena]

Dear GHC devs,
I am currently working on my own fork of GHC (
https://gitlab.haskell.org/trupill/ghc), and as part of it I need to do
some changes to the Cabal and haskeline libraries. However, since they are
in submodules, I am not sure about how I can commit those changes, share
them with others, and rebase my changes against the current HEAD for these
submodules.

Thanks in advance and kind regards,
Alejandro
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

validate-whitespace

[Alejandro Serrano Mena]

Hi GHC devs,
I have made a rebase to bring my merge request [
https://gitlab.haskell.org/ghc/ghc/merge_requests/1659] up to date with the
current GHC codebase. In the process there were some conflicts (as
expected) which I could solve. However, now that I have pushed the result,
I get these messages from the CI infrastructure:

$ validate-whitespace .git $(git rev-list $base..$CI_COMMIT_SHA)
=
commit 0d92f8c898ccbf2ffb602bc75e50e9ffd44811d8 has whitespace linter
issues:

 *ERROR* compiler/typecheck/TcUnify.hs:810: introduces trailing whitespace
 > "  "

 *ERROR* compiler/typecheck/TcUnify.hs:818: introduces trailing whitespace
 > "  = "

Validation FAILED for 0d92f8c898ccbf2ffb602bc75e50e9ffd44811d8
=
commit 465d27f2119d7bdbe06832dd79c3848e27b4aaef has whitespace linter
issues:

 *ERROR* compiler/typecheck/TcExpr.hs:1315: introduces trailing whitespace
 > "   ; subst <- if xopt LangExt.ImpredicativeTypes dflags "

 *ERROR* compiler/typecheck/TcExpr.hs:1472: introduces trailing whitespace
 > "  _ -> return emptyTCvSubst "

 *ERROR* compiler/typecheck/TcExpr.hs:1513: introduces trailing whitespace
 > ""

Validation FAILED for 465d27f2119d7bdbe06832dd79c3848e27b4aaef
=
Validation FAILED because at least one commit had linter errors!

What is the right approach to fix these problems? I can fix the whitespace
issues in a new commit, but I don't see how to fix them in all the interim
commits :(

Thanks in advance and kind regards,
Alejandro
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Re: Using head.hackage

[Alejandro Serrano Mena]

El mié., 11 sept. 2019 a las 14:55, Ben Gamari ()
escribió:

> Alejandro Serrano Mena  writes:
>
> > The instructions are quite clear. Alas, when I try to reproduce the steps
> > using my home-build compiler (for which I mean set the `with-compiler` in
> > `cabal.project` to the stage2 compiler obtained by Hadrian), I get:
> >
> >> cabal new-install --lib aeson
> > Distribution/Client/CmdInstall.hs:(361,18)-(363,72): Non-exhaustive
> > patterns in lambda
> >
> Interesting, this sounds like a cabal-install bug. What does
> cabal-install --version say?
>

Here is the output:

$ cabal --version
cabal-install version 3.0.0.0
compiled using version 3.0.0.0 of the Cabal library

Regards,
Alejandro
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Re: Using head.hackage

[Alejandro Serrano Mena]

Note that this only happens with `aeson`, which is the package that the
tutorial asks to add to `extra-packages` in 'cabal.project'.

El mar., 10 sept. 2019 a las 19:17, Alejandro Serrano Mena (<
trup...@gmail.com>) escribió:

> The instructions are quite clear. Alas, when I try to reproduce the steps
> using my home-build compiler (for which I mean set the `with-compiler` in
> `cabal.project` to the stage2 compiler obtained by Hadrian), I get:
>
> > cabal new-install --lib aeson
> Distribution/Client/CmdInstall.hs:(361,18)-(363,72): Non-exhaustive
> patterns in lambda
>
> Do you have any idea of what I might be doing wrong?
>
> Thanks in advance,
> Alejandro
>
> El mar., 10 sept. 2019 a las 12:32, Ben Gamari ()
> escribió:
>
>> Alejandro Serrano Mena  writes:
>>
>> > Dear GHC devs,
>> > As part of our work in "quick look impredicativity", we would like to
>> test
>> > whether any package breaks. I've read about "head.hackage" as a way to
>> test
>> > this fact, but I could not find any information.
>> >
>> > Could somebody point me in the right direction? If it does not exist
>> yet,
>> > I'll try to summarize whatever I learn in the wiki for future reference.
>> >
>> Hi Alejandro,
>>
>> Indeed I have a pair of yet-to-be-published blog posts intended to
>> discuss exactly this. See [1] and [2]. Do let me know if you have any
>> questions.
>>
>> Cheers,
>>
>> - Ben
>>
>>
>> [1] https://gitlab.haskell.org/ghc/homepage/merge_requests/16/diffs
>> [2] https://gitlab.haskell.org/ghc/homepage/merge_requests/29/diffs
>>
>
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Re: Using head.hackage

[Alejandro Serrano Mena]

The instructions are quite clear. Alas, when I try to reproduce the steps
using my home-build compiler (for which I mean set the `with-compiler` in
`cabal.project` to the stage2 compiler obtained by Hadrian), I get:

> cabal new-install --lib aeson
Distribution/Client/CmdInstall.hs:(361,18)-(363,72): Non-exhaustive
patterns in lambda

Do you have any idea of what I might be doing wrong?

Thanks in advance,
Alejandro

El mar., 10 sept. 2019 a las 12:32, Ben Gamari ()
escribió:

> Alejandro Serrano Mena  writes:
>
> > Dear GHC devs,
> > As part of our work in "quick look impredicativity", we would like to
> test
> > whether any package breaks. I've read about "head.hackage" as a way to
> test
> > this fact, but I could not find any information.
> >
> > Could somebody point me in the right direction? If it does not exist yet,
> > I'll try to summarize whatever I learn in the wiki for future reference.
> >
> Hi Alejandro,
>
> Indeed I have a pair of yet-to-be-published blog posts intended to
> discuss exactly this. See [1] and [2]. Do let me know if you have any
> questions.
>
> Cheers,
>
> - Ben
>
>
> [1] https://gitlab.haskell.org/ghc/homepage/merge_requests/16/diffs
> [2] https://gitlab.haskell.org/ghc/homepage/merge_requests/29/diffs
>
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Using head.hackage

[Alejandro Serrano Mena]

Dear GHC devs,
As part of our work in "quick look impredicativity", we would like to test
whether any package breaks. I've read about "head.hackage" as a way to test
this fact, but I could not find any information.

Could somebody point me in the right direction? If it does not exist yet,
I'll try to summarize whatever I learn in the wiki for future reference.

Thanks in advance,
Alejandro
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Re: New implementation for `ImpredicativeTypes`

[Alejandro Serrano Mena]

Hi Alex,
Also de-railing the conversation, the Utrecht Haskell Compiler supports
existential types in addition to universally-quantified ones. The work on
Atze Dijkstra (among others) describes some of the problems and possible
solutions to inference:
- His PhD thesis [https://dspace.library.uu.nl/handle/1874/7352] describes
existentials in Section 8.
- Their paper "A Lazy Language Needs a Lazy Type System" [
https://dspace.library.uu.nl/handle/1874/346316] proposes treating
existential types as "polymorphic contexts".

Going back to impredicativity, adding existential types would only
complicate inference more, since there are more types to choose from while
instantiating. But the delta would not be that large, since once a type
constructor guards a type, everything inside of it should be equal, and
checking equality of existential types is as hard as checking for universal
types.

Alejandro

El vie., 6 sept. 2019 a las 16:21, Alex Rozenshteyn ()
escribió:

> Hi Simon,
>
> You're exactly right, of course. My example is confusing, so let me see if
> I can clarify.
>
> What I want in the ideal is map show [1, 'a', "b"]. That is, minimal
> syntactic overhead to mapping a function over multiple values of distinct
> types that results in a homogeneous list. As the reddit thread points out,
> there are workarounds involving TH or wrapping each element in a
> constructor or using bespoke operators, but when it comes down to it, none
> of them actually allows me to say what I *mean*; the TH one is closest,
> but I reach for TH only in times of desperation.
>
> I had thought that one of the things preventing this was lack of
> impredicative instantiation, but now I'm not sure. Suppose Haskell *did*
> have existentials; would map show @(exists a. Show a => a) [1, 'a', "b"]
> work in current Haskell and/or in quick-look?
>
> Tangentially, do you have a reference for what difficulties arise in
> adding existentials to Haskell? I have a feeling that it would make working
> with GADTs more ergonomic.
>
> On Fri, Sep 6, 2019 at 12:33 AM Simon Peyton Jones 
> wrote:
>
>> I’m confused.   Char does not have the type (forall a. Show a =>a), so
>> our example is iill-typed in System F, never mind about type inference.
>> Perhaps there’s a typo?   I think you may have ment
>>
>>exists a. Show a => a
>>
>> which doesn’t exist in Haskell.  You can write existentials with a data
>> type
>>
>>
>>
>> data Showable where
>>
>>S :: forall a. Show a => a -> Showable
>>
>>
>>
>> Then
>>
>>map show [S 1, S ‘a’, S “b”]
>>
>> works fine today (without our new stuff), provided you say
>>
>>
>>
>>instance Show Showable where
>>
>>  show (S x) = show x
>>
>>
>>
>> Our new system can only type programs that can be written in System F.
>> (The tricky bit is inferring the impredicative instantiations.)
>>
>>
>>
>> Simon
>>
>>
>>
>> *From:* ghc-devs  *On Behalf Of *Alex
>> Rozenshteyn
>> *Sent:* 06 September 2019 03:31
>> *To:* Alejandro Serrano Mena 
>> *Cc:* GHC developers 
>> *Subject:* Re: New implementation for `ImpredicativeTypes`
>>
>>
>>
>> I didn't say anything when you were requesting use cases, so I have no
>> right to complain, but I'm still a little disappointed that this doesn't
>> fix my (admittedly very minor) issue:
>> https://www.reddit.com/r/haskell/comments/3am0qa/existentials_and_the_heterogenous_list_fallacy/csdwlp2/?context=8=9
>> <https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fwww.reddit.com%2Fr%2Fhaskell%2Fcomments%2F3am0qa%2Fexistentials_and_the_heterogenous_list_fallacy%2Fcsdwlp2%2F%3Fcontext%3D8%26depth%3D9=02%7C01%7Csimonpj%40microsoft.com%7Cf5bddbe8c13b424fad8a08d732724d04%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C63708810706935=a5c3ujC0kiPlocgHg8AX%2BwIP6ZH2hnqszCpnWOiqpGQ%3D=0>
>>
>>
>>
>> For those who don't want to click on the reddit link: I would like to be
>> able to write something like map show ([1, 'a', "b"] :: [forall a. Show
>> a => a]), and have it work.
>>
>>
>>
>> On Wed, Sep 4, 2019 at 8:13 AM Alejandro Serrano Mena 
>> wrote:
>>
>> Hi all,
>>
>> As I mentioned some time ago, we have been busy working on a new
>> implementation of `ImpredicativeTypes` for GHC. I am very thankful to
>> everybody who back then sent us examples of impredicativity which would be
>> nice to support, as far as we know this branch supports all of them! :)
>

Re: New implementation for `ImpredicativeTypes`

[Alejandro Serrano Mena]

To follow up on this, the current spec. is available in the following PDF:
https://www.dropbox.com/s/hxjp28ym3lptmxw/quick-look-steps.pdf?dl=0

El mié., 4 sept. 2019 a las 17:13, Alejandro Serrano Mena (<
trup...@gmail.com>) escribió:

> Hi all,
> As I mentioned some time ago, we have been busy working on a new
> implementation of `ImpredicativeTypes` for GHC. I am very thankful to
> everybody who back then sent us examples of impredicativity which would be
> nice to support, as far as we know this branch supports all of them! :)
>
> If you want to try it, at
> https://gitlab.haskell.org/trupill/ghc/commit/a3f95a0fe0f647702fd7225fa719a8062a4cc0a5/pipelines?ref=quick-look-build
> you can find the result of the pipeline, which includes builds for several
> platforms (click on the "Artifacts" button, the one which looks like a
> cloud, to get them). The code is being developed at
> https://gitlab.haskell.org/trupill/ghc.
>
> Any code should run *unchanged* except for some eta-expansion required for
> some specific usage patterns of higher-rank types. Please don't hesitate to
> ask any questions or clarifications about it. A merge request for tracking
> this can be found at
> https://gitlab.haskell.org/ghc/ghc/merge_requests/1659
>
> Kind regards,
> Alejandro
>
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

New implementation for `ImpredicativeTypes`

[Alejandro Serrano Mena]

Hi all,
As I mentioned some time ago, we have been busy working on a new
implementation of `ImpredicativeTypes` for GHC. I am very thankful to
everybody who back then sent us examples of impredicativity which would be
nice to support, as far as we know this branch supports all of them! :)

If you want to try it, at
https://gitlab.haskell.org/trupill/ghc/commit/a3f95a0fe0f647702fd7225fa719a8062a4cc0a5/pipelines?ref=quick-look-build
you can find the result of the pipeline, which includes builds for several
platforms (click on the "Artifacts" button, the one which looks like a
cloud, to get them). The code is being developed at
https://gitlab.haskell.org/trupill/ghc.

Any code should run *unchanged* except for some eta-expansion required for
some specific usage patterns of higher-rank types. Please don't hesitate to
ask any questions or clarifications about it. A merge request for tracking
this can be found at https://gitlab.haskell.org/ghc/ghc/merge_requests/1659

Kind regards,
Alejandro
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Re: Missing library in Mac OS X instructions?

[Alejandro Serrano Mena]

Thanks for the reply!
In my case, it was a clean installation of Mac OS X, with only Xcode
command line tools and after executing the corresponding 'brew' command
from the wiki.

El lun., 19 ago. 2019 11:09, Shayne Fletcher 
escribió:

> Hi Alejandro,
>
> On Mon, Aug 19, 2019 at 2:11 AM Alejandro Serrano Mena 
> wrote:
>
>> Hi,
>> I tried to get GHC working from the repo in Mac OS X following the
>> instructions in
>> https://gitlab.haskell.org/ghc/ghc/wikis/building/preparation/mac-osx.
>> At first I got the "error __GNU_MP_VERSION not defined" problem, for
>> which the guide recommends to prepend "CC=clang"  to "./configure" , which
>> I did. But even then, I also had to install "gmp" using "brew install gmp".
>> 1. Is it right that I need to install gmp using brew or did I miss some
>> previous step?
>> 2. If (1) is affirmative, how can I help update the docs for building in
>> Mac OS X?
>>
>>
> I've encountered this problem. In my case it turned out that I had a rogue
> `cc` executable in my path. See
> https://gitlab.haskell.org/ghc/ghc/issues/16904 for details.
>
> --
> *Shayne Fletcher*
> Language Engineer */* +1 917 699 7663
> *Digital Asset* <https://digitalasset.com/>, creators of *DAML
> <https://daml.com/>*
>
> This message, and any attachments, is for the intended recipient(s) only,
> may contain information that is privileged, confidential and/or proprietary
> and subject to important terms and conditions available at
> http://www.digitalasset.com/emaildisclaimer.html. If you are not the
> intended recipient, please delete this message.
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Missing library in Mac OS X instructions?

[Alejandro Serrano Mena]

Hi,
I tried to get GHC working from the repo in Mac OS X following the
instructions in
https://gitlab.haskell.org/ghc/ghc/wikis/building/preparation/mac-osx. At
first I got the "error __GNU_MP_VERSION not defined" problem, for which the
guide recommends to prepend "CC=clang"  to "./configure" , which I did. But
even then, I also had to install "gmp" using "brew install gmp".
1. Is it right that I need to install gmp using brew or did I miss some
previous step?
2. If (1) is affirmative, how can I help update the docs for building in
Mac OS X?

Regards,
Alejandro
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Re: Guarded Impredicativity

[Alejandro Serrano Mena]

Just to keep you posted about the current development, we are working on a
new approach to impredicativity which is inspired by guarded
impredicativity but requires much fewer changes to the codebase. In
particular, our goal is to isolate the inference of impredicativity,
instead of contaminating the whole compiler with it.

The repo where we are developing it lives in
https://gitlab.haskell.org/trupill/ghc (branch "quick-look").

Regards,
Alejandro

El vie., 19 jul. 2019 a las 23:40, Ryan Scott ()
escribió:

> Good to know. Thanks for checking!
>
> Ryan S.
>
> On Fri, Jul 19, 2019 at 11:22 AM Artem Pelenitsyn
>  wrote:
> >
> > Hello Ryan,
> >
> > Your example seems to work out of the box with the GI branch.
> >
> > With the oneliner Matthew posted before:
> > nix run -f
> https://github.com/mpickering/ghc-artefact-nix/archive//master.tar.gz \
> > ghc-head-from -c ghc-head-from \
> >
> https://gitlab.haskell.org/mpickering/ghc/-/jobs/114593/artifacts/raw/ghc-x86_64-fedora27-linux.tar.xz
> > It is really easy to check. Also, I didn't see anywhere mentioned that
> one need to provide -XImpredicativeTypes. The whole example, therefore, is:
> >
> > {-#LANGUAGE ImpredicativeTypes, ConstraintKinds #-}
> > module M where
> > type F f = (Functor f, forall a. Eq (f a))
> >
> > --
> > Best, Artem
> >
> > On Fri, 19 Jul 2019 at 09:18, Ryan Scott 
> wrote:
> >>
> >> I have another interesting application of guarded impredicativity that
> >> I want to bring up. Currently, GHC #16140 [1] makes it rather
> >> inconvenient to use quantified constraints in type synonyms. For
> >> instance, GHC rejects the following example by default:
> >>
> >> type F f = (Functor f, forall a. Eq (f a))
> >>
> >> This is because F is a synonym for a constraint tuple, so mentioning a
> >> quantified constraint in one of its arguments gets flagged as
> >> impredicative. In the discussion for #16140, we have pondered doing a
> >> major rewrite of the code in TcValidity to permit F. But perhaps we
> >> don't need to! After all, the quantified constraint in the example
> >> above appears directly underneath a type constructor (namely, the type
> >> constructor for the constraint 2-tuple), which should be a textbook
> >> case of guarded impredicativity.
> >>
> >> I don't have the guarded impredicativity branch built locally, so I am
> >> unable to test if this hypothesis is true. In any case, I wanted to
> >> mention it as another motivating use case.
> >>
> >> Ryan S.
> >> -
> >> [1] https://gitlab.haskell.org/ghc/ghc/issues/16140
> >> ___
> >> ghc-devs mailing list
> >> ghc-devs@haskell.org
> >> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
> ___
> ghc-devs mailing list
> ghc-devs@haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Re: Guarded Impredicativity

[Alejandro Serrano Mena]

Thank you very much, this kind of real world examples are very useful to us.
Right now we are still researching what are the possibilities, but we'll
try to cover this use case.

Regards,
Alejandro

El lun., 15 jul. 2019 a las 16:21, Oliver Charles ()
escribió:

> Hi Alejandro and other GHC devs,
>
> I've just been pointed to this mailing list, and in particular the
> discussion on guarded impredicativity from the Haskell IRC channel. I
> wasn't following the list before, so sorry if this post comes out of
> threads!
>
> I have a use case for impredicative polymorphism at the moment that
> comes out of some work on effect systems. Essentially, what I'm trying
> to do is to use reflection to thread around the interpretation of an
> effect. One encoding of effects is:
>
> newtype Program signature carrier a =
>   Program { ( forall x. signature x -> carrier x ) -> carrier a }
>
> But for various reasons, this sucks for writing really high performant
> code.
>
> My formulation is instead to change that -> to =>, and to carry around
> the signature interpretation with reflection. Thus we have something
> roughly along the lines of:
>
> newtype Program s signature carrier a =
>  Program ( forall m. Monad m => m a )
>
> with
>
> runProgram
>   :: ( forall s. Reifies s ( signature :~> carrier ) => Program s
> signature carrier a )
>   -> carrier a
>
> All is well and good, but from the user's perspective, it sucks to
> actually compose these things together, due to the `forall s` bit. For
> example, I can write:
>
> foo =
>   runError (runState s myProgram)
>
> but I can't write
>
> foo =
>   runError . runState s $
>   myProgram
>
> or
>
> foo =
>   myProgram
> & runState s
> & runError
>
> I was excited to hear there is a branch with some progress on GI, but
> unfortunately it doesn't seem sufficient for my application. I've
> uploaded everything (it's just two files) here:
>
> https://gist.github.com/ocharles/8008bf31c70d0190ff3440f9a5b0684d
>
> Currently this doesn't compile, but I'd like it to (I'm using the `nix
> run` command mpickering shared earlier). The problem is Example.hs:55
> - if you change the first . to a $, it type checks.
>
> Let me know if this is unclear and I'm happy to refine it. I just
> wanted to show you:
>
> * Roughly what I want to do
> * A concrete program that still fails to type check, even though I
> believe it should (in some ideal type checker...)
>
> Regards,
> Ollie
>
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Re: Guarded Impredicativity

[Alejandro Serrano Mena]

Thanks very much,
If you had some snippets of code or some libraries you could share with us,
that would be extremely helpful.

Regards,
Alejandro

El jue., 4 jul. 2019 a las 9:10, Spiwack, Arnaud ()
escribió:

> Dear Alejandro and Simon,
>
> Taking into account that I'm a bit of an impredicativity nut, so I may be
> over enthusiastic.
>
> - I frequently want more impredicativity in GHC
> - Last time I did, guarded impredicativity, as in the paper, would have, I
> believed, done the trick.
>
> That being said, it is somewhat hard to give an answer on the spot, but
> I'll try to take note of why and whether guarded impredicativity would
> suffice.
>
> Best,
> Arnaud
>
>
> On Fri, Jun 28, 2019 at 2:15 PM Simon Peyton Jones via ghc-devs <
> ghc-devs@haskell.org> wrote:
>
>> Just to amplify: we are very interested to
>>
>>
>>
>>- Get some idea of *whether anyone  cares about impredicativity*.  If
>>we added it to GHC, would you use it?  Have you ever bumped up Haskell’s
>>inability to instantiate a polymorphic function at a polytype.
>>
>>
>>
>>- Get some idea of *whether the particular form of impredicativity
>>described in the paper would be expressive enough* for your
>>application.
>>
>>
>>
>> Simon
>>
>>
>>
>> *From:* ghc-devs  *On Behalf Of *Alejandro
>> Serrano Mena
>> *Sent:* 28 June 2019 13:12
>> *To:* ghc-devs@haskell.org
>> *Subject:* Guarded Impredicativity
>>
>>
>>
>> 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/
>> <https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fwww.microsoft.com%2Fen-us%2Fresearch%2Fpublication%2Fguarded-impredicative-polymorphism%2F=02%7C01%7Csimonpj%40microsoft.com%7Ca2d42d6134644b3d128a08d6fbc1e36d%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636973207496244478=o8H3dd5tLDRCGpwzsq6BMwNwYepPQgmoKsrXtLbJQdk%3D=0>
>> ].
>>
>>
>>
>> For now I have produced a first attempt, which lives in
>> https://gitlab.haskell.org/trupill/ghc
>> <https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgitlab.haskell.org%2Ftrupill%2Fghc=02%7C01%7Csimonpj%40microsoft.com%7Ca2d42d6134644b3d128a08d6fbc1e36d%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636973207496244478=TGegIFjwdjJ7XPdmlVNY3wve385FalfVLaW1YLCiXlM%3D=0>.
>> 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
>> <https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgitlab.haskell.org%2Fghc%2Fghc=02%7C01%7Csimonpj%40microsoft.com%7Ca2d42d6134644b3d128a08d6fbc1e36d%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636973207496254471=hXtR8j0th3U65DW7MvaofVW8tq7pubXUJqlyflGSBPw%3D=0>
>> impredicative-ghc
>>
>> > cd impredicative-ghc
>>
>> > git remote add trupill g...@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@haskell.org
>> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>>
>
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Re: Guarded Impredicativity

[Alejandro Serrano Mena]

After having a quick look, I think it could be done easily in terms of type
checking. Alas, there's some code in TcSplice.hs which insists anyway on
having a quantifier-free type:

tcTExpTy :: TcType -> TcM TcType
tcTExpTy exp_ty
= do { unless (isTauTy exp_ty) $ addErr (err_msg exp_ty)
; ... }
where
err_msg ty
= vcat [ text "Illegal polytype:" <+> ppr ty
, text "The type of a Typed Template Haskell expression must" <+>
text "not have any quantification." ]

Does anybody have any pointers about why this restriction is in place?

Regards,
Alejandro

El vie., 28 jun. 2019 a las 15:19, Matthew Pickering (<
matthewtpicker...@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?
>
> 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.
>
> Cheers,
>
> Matt
>
> On Fri, Jun 28, 2019 at 1:20 PM Alejandro Serrano Mena
>  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 (<
> matthewtpicker...@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
> >>  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 g...@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@haskell.org
> >> > http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Re: Guarded Impredicativity

[Alejandro Serrano Mena]

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 ()
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@haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Re: Guarded Impredicativity

[Alejandro Serrano Mena]

Hi,

El vie., 28 jun. 2019 a las 15:19, Matthew Pickering (<
matthewtpicker...@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
>  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 (<
> matthewtpicker...@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
> >>  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 g...@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@haskell.org
> >> > http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Re: 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 (<
matthewtpicker...@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
>  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 g...@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@haskell.org
> > http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Guarded Impredicativity

[Alejandro Serrano Mena]

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 g...@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@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Re: Guarded Impredicativity implementation

[Alejandro Serrano Mena]

Hi Artem,
It's great to see some interest about our work :)
At this moment there are no plans of making it part of GHC -- some details
about the integration with other features need further thought. If you are
really interested in trying, we built a prototype at
https://git.science.uu.nl/f100183/ghc-invariant, which incorporates some
advances in the "backward compatibility" section of the paper, but not
guarded impredicativity per se.

Regards,
Alejandro

2018-02-26 23:36 GMT+01:00 Simon Peyton Jones via ghc-devs <
ghc-devs@haskell.org>:

> Alejandro may want to comment…
>
>
>
> *From:* ghc-devs [mailto:ghc-devs-boun...@haskell.org] *On Behalf Of *Artem
> Pelenitsyn
> *Sent:* 26 February 2018 17:05
> *To:* ghc-devs@haskell.org
> *Subject:* Guarded Impredicativity implementation
>
>
>
> Dear ghc-devs,
>
> Is there any work has been done on the latest (ttbomk) proposal for
> impredicative types in Haskell:
>
> > Guarded impredicative polymorphism by Alejandro Serrano, Jurriaan Hage,
> Dimitrios Vytiniotis, Simon Peyton Jones
> https://www.microsoft.com/en-us/research/wp-content/
> uploads/2017/07/impredicative-Jul17.pdf
> 
>
> Or are there any plans to do so? I wasn't able to spot any mentions of
> this in either of GHC's forums (this list, Trac, wiki, ghc-proposals repo).
>
> --
>
> Best wishes,
>
> Artem Pelenitsyn
>
> ___
> ghc-devs mailing list
> ghc-devs@haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>
>
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Re: Reading source annotations during type checking

[Alejandro Serrano Mena]

Thanks very much! New things to try during Christmas :)

Alejandro

2016-12-20 8:47 GMT+01:00 Alan & Kim Zimmerman <alan.z...@gmail.com>:

> I did, and thought I saw a reply.
>
> They are captured in the AST.
>
> data AnnDecl name = HsAnnotation
>   SourceText -- Note [Pragma source text] in BasicTypes
>   (AnnProvenance name) (Located (HsExpr name))
>
> Alan
>
> On Tue, Dec 20, 2016 at 2:54 AM, Ben Gamari <b...@smart-cactus.org> wrote:
>
>> Alan, did you see this?
>>
>> Alejandro Serrano Mena <trup...@gmail.com> writes:
>>
>> > Dear GHC devs,
>> > Is there a way to retrieve "source annotations" (as defined by
>> > https://downloads.haskell.org/~ghc/latest/docs/html/users_gu
>> ide/extending_ghc.html#source-annotations)
>> > during type checking. In particular, I am interested in reading them in
>> > TcExpr and TcCanonical.
>> >
>> > Regards,
>> > Alejandro
>> > ___
>> > ghc-devs mailing list
>> > ghc-devs@haskell.org
>> > http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>>
>
>
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Reading source annotations during type checking

[Alejandro Serrano Mena]

Dear GHC devs,
Is there a way to retrieve "source annotations" (as defined by
https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/extending_ghc.html#source-annotations)
during type checking. In particular, I am interested in reading them in
TcExpr and TcCanonical.

Regards,
Alejandro
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Re: Getting rid of -XImpredicativeTypes

[Alejandro Serrano Mena]

What would be the story for the types of the arguments. Would I be allowed
to write the following?

> f (lst :: [forall a. a -> a]) = head @(forall a. a -> a) lst 3

Regards,
Alejandro

2016-09-25 20:05 GMT+02:00 Simon Peyton Jones via ghc-devs <
ghc-devs@haskell.org>:

> Friends
>
>
>
> GHC has a flag -XImpredicativeTypes that makes a half-hearted attempt to
> support impredicative polymorphism.  But it is vestigial…. if it works,
> it’s really a fluke.  We don’t really have a systematic story here at all.
>
>
>
> I propose, therefore, to remove it entirely.  That is, if you use
> -XImpredicativeTypes, you’ll get a warning that it does nothing (ie.
> complete no-op) and you should remove it.
>
>
>
> Before I pull the trigger, does anyone think they are using it in a
> mission-critical way?
>
>
>
> Now that we have Visible Type Application there is a workaround: if you
> want to call a polymorphic function at a polymorphic type, you can
> explicitly apply it to that type.  For example:
>
>
>
> {-# LANGUAGE ImpredicativeTypes, TypeApplications, RankNTypes #-}
>
> module Vta where
>
>   f x = id @(forall a. a->a) id @Int x
>
>
>
> You can also leave out the @Int part of course.
>
>
>
> Currently we have to use -XImpredicativeTypes to allow the @(forall a.
> a->a).Is that sensible?  Or should we allow it regardless?   I rather
> think the latter… if you have Visible Type Application (i.e.
> -XTypeApplications) then applying to a polytype is nothing special.   So I
> propose to lift that restriction.
>
>
>
> I should go through the GHC Proposals Process for this, but I’m on a
> plane, so I’m going to at least start with an email.
>
>
>
> Simon
>
> ___
> ghc-devs mailing list
> ghc-devs@haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>
>
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Re: Getting rid of -XImpredicativeTypes

[Alejandro Serrano Mena]

2016-09-26 9:00 GMT+02:00 Ben Gamari :

> Simon Peyton Jones via ghc-devs  writes:
>
> > Friends
> >
> > GHC has a flag -XImpredicativeTypes that makes a half-hearted attempt
> > to support impredicative polymorphism. But it is vestigial if it
> > works, it's really a fluke. We don't really have a systematic story
> > here at all.
> >
> Out of curiosity, what ever happened to the most recent attempt at
> addressing impredicativity [1]?
>

It turned our that the new system being proposed was not better than the
current one. In particular, it was almost impossible to know upfront
whether a program using impredicative types would need an annotation to
typecheck. Furthermore, I think it would imply a humongous amount of
changes to GHC, for not a very large gain.


>
> As far as the proposal process is concerned, it would likely be a good
> idea to put together a proposal so we have somewhere to collect
> comments. That being said, it needn't be terribly lengthy given that we
> are merely removing a feature.
>
> Incidentally, that reminds me that I have some documentation fixes to
> the ghc-proposals repository that I should proof-read and push.
>
> Cheers,
>
> - Ben
>
>
> [1] https://ghc.haskell.org/trac/ghc/wiki/ImpredicativePolymorphism/
> Impredicative-2015
>
> ___
> ghc-devs mailing list
> ghc-devs@haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>
>
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs