Relaxing Levity-Polymorphic Binder Check for Lifted vs Unlifted pointers
I'm going to define two terms that I will use with these meanings for the remainder of this post.
- Runtime-Rep Polymorphism: full polymorphism in the runtime representation
- 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/dlyug4e/ 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.
Trac metadata
Trac field | Value |
---|---|
Version | 8.4.3 |
Type | FeatureRequest |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | dfeuer, goldfirere, simonpj, treeowl |
Operating system | |
Architecture |