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.diatc...@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 <rpglove...@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 <simo...@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-boun...@haskell.org> On Behalf Of Alex Rozenshteyn >>> Sent: 06 September 2019 03:31 >>> To: Alejandro Serrano Mena <trup...@gmail.com> >>> Cc: GHC developers <ghc-devs@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 <trup...@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@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 _______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
