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

[GHC]

#14917: Allow levity polymorhism in binding position
-------------------------------------+-------------------------------------
           Reporter:  andrewthad     |             Owner:  (none)
               Type:  feature        |            Status:  new
  request                            |
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.2.2
           Keywords:                 |  Operating System:  Unknown/Multiple
  LevityPolymorphism                 |
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 The main problem with levity polymorphism in a binding position is that
 it's impossible to do codegen since the calling convention depending on
 the instantiation of the runtime representation variable. From the paper,
 we have the following rejected example code:

 {{{
 bTwice :: ∀ (r :: RuntimeRep) (a :: TYPE r). Bool → a → (a → a) → a
 }}}

 However, if you are able to inline the function, this problem disappears.
 You would need a guarantee stronger than what the `INLINE` pragma provides
 though since the `INLINE` pragma still allows the function to be fed as an
 argument to a higher-order function. I'll refer to a hypothetical new
 pragma as `INLINE MANDATE`. This pragma causes a compile-time error to be
 admitted if the function is ever used in a way that would cause it to not
 be inlined. Now `bTwice` would be writeable:

 {{{
 {-# INLINE MANDATE #-}
 bTwice :: ∀ (r :: RuntimeRep) (a :: TYPE r). Bool → a → (a → a) → a
 }}}

 The function definition would be provide in the `.hi` file just as it
 would be for a function marked as `INLINE`, but unlike the `INLINE`
 counterpart, there would be no generated code for this function, since
 generating the code would be impossible.

 I have several uses for this in mind. I often want a levity-polymorphic
 variant `ST`. With `INLINE MANDATE`, I still wouldn't get `do` notation,
 but I could write:

 {{{
 -- This newtype is already allowed today
 newtype STL s (a :: TYPE r) = STL (State# s -> (# s, a #) #)

 intA, intB, intC :: STL s Int#
 wordA, wordB :: Int# -> STL s Word#

 {-# INLINE MANDATE #-}
 (>>=.) :: STL s a -> (a -> STL s b) -> STL s b
 STL a >>=. g = STL (\s0 -> case a s0 of
     (# s1, v #) -> case g v of
       STL f -> f s1

 myFunc :: STL s Word#
 myFunc =
   intA >>=. \a ->
   intB >>=. \b ->
   intC >>=. \c ->
   wordA a >>=. \wa ->
   wordB b >>=. \wb ->
   ... -- do something with the data
 }}}

 I would appreciate any feedback on this. If there's something that makes
 this fundamentally impossible, that would be good to know. Or if other
 people feel like this would be useful, that would be good to know as well.

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