[GHC] #15532: Relaxing Levity-Polymorphic Binder Check for Lifted vs Unlifted pointers

17 Aug 2018

      #15532: Relaxing Levity-Polymorphic Binder Check for Lifted vs Unlifted pointers
-------------------------------------+-------------------------------------
           Reporter:  andrewthad     |             Owner:  (none)
               Type:  feature        |            Status:  new
  request                            |
           Priority:  normal         |         Milestone:  8.6.1
          Component:  Compiler       |           Version:  8.4.3
           Keywords:                 |  Operating System:  Unknown/Multiple
  LevityPolymorphism                 |
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:  14917
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 I'm going to define two terms that I will use with these meanings for the
 remainder of this post.

 1. Runtime-Rep Polymorphism: full polymorphism in the runtime
 representation
 2. Levity Polymorphism: polymorphism dealing with lifted vs unlifted types
 that are definitely represented by pointers.

 GHC's levity polymorphism has the restriction that runtime-rep-polymorphic
 binders are not allowed. A comment David made recently on
 https://github.com/haskell/primitive/issues/198 got me thinking about the
 possibility of relaxing this restriction when it comes to dealing with a
 function with levity-polymorphic (not runtime-rep-polymorphic) binders.
 GHC's runtime already appears to allow doing this. AndrasKovacs writes on
 https://www.reddit.com/r/haskell/comments/6v9rmg/an_unified_array_interface/...
 that he is able to store both lifted and unlifted values inside of the
 same `Array#` (pointing out as well that their primop implementations are
 identical) without crashing the GC. As further evidence that we can,
 roughly speaking, use lifted and unlifted values in the same places, I
 threw together a little experiment:

 {{{
 {-# LANGUAGE MagicHash #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE TypeInType #-}

 import Data.Primitive
 import Data.Primitive.UnliftedArray
 import GHC.Types
 import GHC.Exts

 main :: IO ()
 main = do
   a@(Array myArr) <- newArray 1 ("foo" :: String) >>= unsafeFreezeArray
   UnliftedArray myArrArr <- newUnliftedArray 1 a >>=
 unsafeFreezeUnliftedArray
   putStrLn (myFunc show (2 :: Integer))
   putStrLn (myFunc2 (\x -> show (Array x)) myArr)
   putStrLn (myBigFunc (+1) show show (2 :: Integer))
   putStrLn (myBigFunc2 (\x -> array# (indexUnliftedArray (UnliftedArray x)
 0 :: Array String)) (\x -> show (Array x)) (\x -> show (UnliftedArray x ::
 UnliftedArray (Array String))) myArrArr)

 {-# NOINLINE myFunc #-}
 myFunc :: (a -> String) -> a -> String
 myFunc f a =
   let x = f a
    in x ++ x

 myFunc2 :: forall (a :: TYPE 'UnliftedRep). (a -> String) -> a -> String
 myFunc2 = unsafeCoerce# myFunc

 {-# NOINLINE myBigFunc #-}
 myBigFunc :: (a -> b) -> (b -> String) -> (a -> String) -> a -> String
 myBigFunc f g h a =
   let y = f a
       x = g y
    in x ++ x ++ h a

 myBigFunc2 :: forall (a :: TYPE 'UnliftedRep) (b :: TYPE 'UnliftedRep). (a
 -> b) -> (b -> String) -> (a -> String) -> a -> String
 myBigFunc2 = unsafeCoerce# myBigFunc
 }}}

 The compiles (surprisingly without a core lint error) and runs fine. So,
 here's the idea. We start with David's suggested change to `RuntimeRep`:

 {{{
 data RuntimeRep
   = PtrRep Levity
   | ...
 data Levity = Lifted | Unlifted
 }}}

 And then we change the check that disallows runtime-rep polymorphism in
 binding positions to accept levity polymorphism in binding positions (but
 continuing to reject runtime-rep polymorphism). For example, the two
 examples in the above code snippet would be rewritten as:

 {{{

 myFunc :: forall (v :: Levity) (a :: TYPE ('PtrRep v)). (a -> String) -> a
 -> String
 myFunc = ... -- same implementation

 myBigFunc :: forall (v :: Levity) (w :: Levity) (a :: TYPE ('PtrRep v)) (b
 :: TYPE ('PtrRep w)). (a -> b) -> (b -> String) -> (a -> String) -> a ->
 String
 myBigFunc = ... -- same implementation

 }}}

 Again, GHC's runtime seems to already allow this. It's just the type
 system that's missing support for it. The only weird thing I can think of
 that comes up is that you cannot use bang patterns on a levity-polymorphic
 argument since unlifted values cannot be entered.

 I think it is possible to go a little further still. Fields of data types
 could be levity polymorphic:

 {{{
 data List (a :: TYPE ('PtrRep v)) = Cons a (List a) | Nil

 map :: forall (v :: Levity) (w :: Levity) (a :: TYPE ('PtrRep v)) (b ::
 TYPE ('PtrRep w)). (a -> b) -> List a -> List b
 }}}

 Again, bang patterns would need to be forbidden on such fields. This
 doesn't get us everything sought out in
 https://ghc.haskell.org/trac/ghc/wiki/UnliftedDataTypes, but it's kind of
 a half-way point that requires no changes to GHC's runtime and no changes
 to code generation. I think the whole thing can be handled in the type
 checker. Other potential application: `Array#` and `ArrayArray#` (and
 nearly all functions that operate on them) could be consolidated into a
 single type, reducing the number of duplicated primop implementations in
 GHC.

 Of course this would all need to be a GHC proposal, but I wanted to first
 solicit some feedback here on initial draft of the idea.

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

GHC

GHC

GHC

GHC

GHC

GHC

GHC

GHC

GHC

GHC

GHC

GHC

GHC

tags

participants (1)