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
