[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 josef):

 I've thought about this problem for some time, but never written down
 my ideas before. Now seemed like a good time to speak up though :-) Below
 are some hopefully coherenet notes.

 I'd introduce a new quantifier (let's call it "V") which provides
 '''template polymorphism'''.  This quantifier can quantify over all kinds,
 even levity polymorphic things.  The idea is that whenever a function
 of template polymorphic type is called, a new copy of the function
 will be created, specialized with the instantiated type for its
 template polymorphic type variables.

 Example:

 {{{
 id :: V r (a :: TYPE r). a -> a
 id a = a
 }}}

 When we use it like in an expression like this `id #5` or `id "foo"`
 the typechecker creates new bindings `id_#_Int#` and `id_*_String`. These
 new bindings are then used as part of elaborating the expressions:
 `id_#_Int# #5` and `id_*_String "foo"`.

 {{{
 id_#_Int# :: Int# -> Int#
 id_#_Int# a = a

 id_*_String :: String -> String
 id_*_String a = a
 }}}

 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.

 A trivial point, that I still want to point out: given two (or more)
 calls to the same template polymorphic function with the same type
 instantiation only generates one new specialization.

 Most likely a more sophisticated naming scheme than the one I've used
 here will be needed to ensure that the names of the new bindings are
 unique.

 The quantifier is only allowed to be used on the top-level and must
 appear before any usual quantifiers. I.e. template polymorphism is rank-1.

 Quantified template polymorphism, i.e. having class constraints on
 template polymorphic type variables is not a problem.

 == Recursion ==

 It is perfectly possible to support monomorphic recursion for template
 polymorphism. In fact, the elaboration outlined above supports
 monomorphic recursion out of the box. The recursive call inside of
 template polymorphic function would generate the same specialization
 as a call from outside the function, and since we don't generate
 multiple specializations, the call will simply be specialized to a
 recursive call in the new specialized function.


 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.

 == Modules ==

 When exporting a template polymorphic function, it's specializations
 should also be exported, to avoid re-generating them. However, the
 importing module will have to creating its own new specializations if
 needed.

 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.

 == Extensions ==

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

 Example:

 {{{
 data List (V r) (a :: TYPE r) = Cons a (List r a) | Nil
 }}}

 This way we get a list data type which can be used at any kind. After
 type checking and elaboration we will have one list data type for
 each runtime representation.

 However, supporting specialization in different modules might require a
 bit of thought.

 == Final thoughts ==

 The gist of this proposal is that it gives control over optimization
 to the library writer, similarly to the RULES pragma. Though it will not
 help any existing programs go faster.

 I'd really like to see something like this in GHC. Unfortunately, I don't
 have the cycles to flesh out this proposal and implement it. But I'd be
 happy to advice if someone wants to have a go at it.

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