Why would you infer this type as opposed to `[exists a. a]`?
On Fri, Sep 6, 2019 at 12:08 PM Vladislav Zavialov <[email protected]> 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 <[email protected]> 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 <[email protected]> > > 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 <[email protected]> > >> 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 <[email protected]> On Behalf Of Alex > >>> Rozenshteyn > >>> Sent: 06 September 2019 03:31 > >>> To: Alejandro Serrano Mena <[email protected]> > >>> Cc: GHC developers <[email protected]> > >>> 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 <[email protected]> > >>> 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 > >>> [email protected] > >>> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs > >> > >> _______________________________________________ > >> ghc-devs mailing list > >> [email protected] > >> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs > > _______________________________________________ > > ghc-devs mailing list > > [email protected] > > http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs > _______________________________________________ ghc-devs mailing list [email protected] http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
