Opened 13 months ago

Last modified 13 months ago

#15532 new feature request

Relaxing Levity-Polymorphic Binder Check for Lifted vs Unlifted pointers

Reported by: andrewthad Owned by:
Priority: normal Milestone: 8.6.1
Component: Compiler Version: 8.4.3
Keywords: LevityPolymorphism Cc: simonpj, goldfirere, treeowl, dfeuer
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: 14917 Differential Rev(s):
Wiki Page:

Description

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/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.

Change History (12)

comment:1 Changed 13 months ago by simonpj

Lifted types are lazy, unlifted ones are strict. See Type.isUnliftedType. So code that is polymorphic in levity might build a thunk for an unlifted value, which the consumer won't expect.

comment:2 Changed 13 months ago by andrewthad

code that is polymorphic in levity might build a thunk for an unlifted value

I thought that this may happen, but I cannot actually get the GHC runtime to exhibit this problem.

comment:3 Changed 13 months ago by andrewthad

This example also works:

{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE UnboxedTuples #-}
{-# 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 (example even show (show . (+1)) (5 :: Integer)) 
  let r = exampleUnlifted
        (\x -> isTrue# (sizeofArrayArray# x ># 1#))
        (\x -> array# (indexUnliftedArray (UnliftedArray x) 1 :: Array String))
        (\x -> array# (indexUnliftedArray (UnliftedArray x) 0 :: Array String))
        myArrArr
      !(# e #) = indexArray# r 0#
  putStrLn e

{-# NOINLINE example #-}
example :: (a -> Bool) -> (a -> b) -> (a -> b) -> a -> b
example p f g a = if p a then f a else g a

exampleUnlifted :: forall (a :: TYPE 'UnliftedRep) (b :: TYPE 'UnliftedRep).
  (a -> Bool) -> (a -> b) -> (a -> b) -> a -> b
exampleUnlifted = unsafeCoerce# example

comment:4 Changed 13 months ago by goldfire

RR-polymorphism (runtime-rep-polymorphism) actually has two different restrictions: we disallow RR-polymorphic binders and we also disallow RR-polymorphic function arguments. Your argument might hold water to lift the binder restriction, but I think we'll need to keep the function-argument restriction to avoid confusion around laziness.

comment:5 Changed 13 months ago by andrewthad

I think we'll need to keep the function-argument restriction to avoid confusion around laziness

When you say "confusion around laziness", are you referring to difficulty the user would have with reasoning about the behavior of a functions, or are you referring to an inability of GHC to generate correct code in this situation.

comment:6 Changed 13 months ago by goldfire

The latter. GHC needs to know whether a function should be call-by-need or call-by-value.

comment:7 Changed 13 months ago by andrewthad

In that case, I should be able to write a function like exampleUnlifted (but possibly more complicated) that will segfault. I'll see if I can come up with something.

comment:8 Changed 13 months ago by andrewthad

We can get a crash if we instead write example as:

example :: (a -> Bool) -> (a -> a) -> (a -> b) -> (a -> b) -> a -> b
example p k f g a = if p a then f (k (k a)) else g (k a)

This fails at runtime with:

internal error: MUT_ARR_PTRS_FROZEN0 object entered!

Thanks for helping me see what I was missing. So GHC couldn't possibly generate code for the definition I gave for the levity-polymorphic map function given in the original issue.

comment:9 Changed 13 months ago by andrewthad

Dang. That means that levity-polymorphic fields in data constructors won't work either. That takes away most of the utility I hoped this would provide.

comment:10 Changed 13 months ago by goldfire

If the levity were retained at runtime (that is, we use a singleton levity), then it is reasonable to case on the levity when deciding whether to be call-by-name or call-by-value. For functions, this could be arranged today via a type-class construction. Not sure how to do it for data constructors, but it's conceivable to add such a thing.

comment:11 Changed 13 months ago by andrewthad

The singleton levity trick would work, but it seems a little disappointing that users would need to take a (admittedly small) performance hit to get this extra polymorphism.

I retract part of my claim about levity polymorphic data constructors. Here is what would be possible/impossible without any changes to GHC's codegen and runtime:

  • Defining levity-polymorphic fields in data construtors. YES
  • Constructing a value with such a data constructor where the levity is monomorphic. YES
  • Constructing a value with such a data constructor where the levity is polymorphic. NO
  • Casing on such a value in a levity-monomorphic or levity-polymorphic settings. YES

This feels consistent with your earlier claim about the binder rule being relaxable but the function argument rule not being relaxable. Casing on a data constructor introduces a binder but applying a data constructor is applying a function. However, casing on a data constructor to get out a levity polymorphic field still isn't particularly useful, since there is basically nothing interesting you can do with the value at that point.

comment:12 Changed 13 months ago by andrewthad

So, you couldn't write map or foldr or anything like that, but you could get a levity polymorphic index lookup:

(!) :: forall (v :: Levity) (a :: TYPE ('PtrRep v)). Int -> List a -> a
Note: See TracTickets for help on using tickets.