New implementation for `ImpredicativeTypes`

Fri Sep 6 20:48:42 UTC 2019

Why would you infer this type as opposed to `[exists a. a]`?

On Fri, Sep 6, 2019 at 12:08 PM Vladislav Zavialov
<vladislav at serokell.io> wrote:
>
> Iavor,
>
> Alex’s example can be well-typed if we allow first-class existentials:
>
>   [1, ‘a’, “b”] :: [exists a. Show a => a]
>
> This has nothing to do with the definition of lists. I believe the confusion was between existential types and impredicative types, as Simon has pointed out.
>
> - Vlad
>
> > On 6 Sep 2019, at 20:56, Iavor Diatchki <iavor.diatchki at gmail.com> wrote:
> >
> > Hello Alex,
> >
> > the issue with your example is not the mapping of `show` but the list
> > `[1, 'a', "b"]`.  It is not well typed simply because of how lists are
> > defined.   Remember that `[1, 'a', "b"]` is not really special---it is
> > just syntactic sugar for `1 : 'a' : "b" : []` and the type of `(:)`
> > requires the elements to have the same type.
> >
> > Of course, in principle, one could define a different list type that
> > allowed values of arbitrary types to be stored in it (e.g., the
> > example list would be just of type `List`).
> > The issue is that you can't really use the elements of such a list as
> > you wouldn't know what type they have.
> >
> > Yet another option is to define a list type where the "cons" operation
> > remembers the types of the elements in the type of the constructed
> > list---at this point the lists become more like tuples (e.g., the
> > example would be of type `List [Int,Char,String]`).   This is
> > possible, but then them `map` function would have an interesting
> > type...
> >
> > I'd be happy to answer more questions but I don't want to side-track
> > the thread as all this is quite orthogonal to impredicative types.
> >
> > -Iavor
> >
> >
> >
> >
> >
> >
> >
> >
> >
> > On Fri, Sep 6, 2019 at 7:21 AM Alex Rozenshteyn <rpglover64 at gmail.com> wrote:
> >>
> >> 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 <simonpj at microsoft.com> 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 <ghc-devs-bounces at haskell.org> On Behalf Of Alex Rozenshteyn
> >>> Sent: 06 September 2019 03:31
> >>> To: Alejandro Serrano Mena <trupill at gmail.com>
> >>> Cc: GHC developers <ghc-devs at haskell.org>
> >>> 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&depth=9
> >>>
> >>>
> >>>
> >>> 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 <trupill at gmail.com> 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! :)
> >>>
> >>>
> >>>
> >>> 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 at haskell.org
> >>> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
> >>
> >> _______________________________________________
> >> ghc-devs mailing list
> >> ghc-devs at haskell.org
> >> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
> > _______________________________________________
> > ghc-devs mailing list
> > ghc-devs at haskell.org
> > http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>