[GHC] #14917: Allow levity polymorphism in binding position

[GHC]

#14917: Allow levity polymorphism in binding position
-------------------------------------+-------------------------------------
        Reporter:  andrewthad        |                Owner:  (none)
            Type:  feature request   |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.2.2
      Resolution:                    |             Keywords:
                                     |  LevityPolymorphism
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by goldfire):

 I, too, have pondered template polymorphism for some time, but never
 fleshed it out even to this level. There are a few problems with this
 design, however:

 >  More formally: A call to a template polymorphic function must
 instantiate all template polymorphic type parameters. These parameters
 must be instantiated with either fully ground types without any variables,
 or variables bound by "V", the template polymorphic quantifier.

 This means that, with your `id` definition, you couldn't have

 {{{#!hs
 idList :: [a] -> [a]
 idList = id
 }}}

 even though you could have

 {{{#!hs
 idListInt :: [Int] -> [Int]
 idListInt = id
 }}}

 So it seems template polymorphism would be infectious, generally requiring
 callers of template-polymorphic functions also to be template-polymorphic.
 I don't think that's a good thing.

 On the flip side, I don't see concretely why we need the "no variables"
 restriction.

 > It is likely possible to support special cases of polymorphic recursion,
 but it is not clear to me that it is worth the extra work.

 Generally, these schemes fail on polymorphic recursion, and I think we
 should do so here, too.

 > This can lead to a situation where a module has two imports which
 exports the same specialization of a function they in turn imported. But
 there is no real problem here, because it doesn't matter which one we pick
 since both specializations will be the same.

 I think there ''is'' a real problem here. First off, it means that the
 `.o` files that GHC produces won't be able to be linked by, e.g., `ld`:
 multiple `.o` files might have the same definitions. In the end, I think
 we'd have to implement some deduplication algorithm during linking, or end
 up with horrid code bloat.

 > One of the interesting things about this proposal is that generalizes
 nicely to data types.

 Under your "no variables" rule, this `List` type would have to be
 specialized at every possible data parameter. I'm worried about bloat.

 > However, supporting [data] specialization in different modules might
 require a bit of thought.

 This is also a thorny question. Here, we absolutely have to get
 deduplication correct, as it's a matter of correctness, not just
 efficiency (in size of the executable).

 One unaddressed question here is: what restrictions would there be on
 template-polymorphic levity-polymorphic variables? Presumably, none, but
 I'm not sure.

 Also, how is this different from the "compulsory unfoldings" idea earlier
 in this thread (started in comment:3)? The user declares template
 polymorphism directly (the compulsory unfoldings idea didn't have any user
 direction -- but perhaps it should have), and the specializations here
 happen by creating new bindings instead of inlining, but I'm not sure a
 user would really see the difference here.

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14917#comment:16>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler