Lazy tuple workaround

[treeowl]

Due to a serious shortcoming in the GHC linearity system, which seems likely to require some research to fix, it's currently impossible to use laziness in any nontrivial way in linear code. I suggest we add some functions to work around the problem until someone with the requisite skills has time to address the underlying problem.

lazyUncurry :: (a %p -> b %p -> c) %q-> (a, b) %p-> c
lazyUncurry = \f -> Unsafe.toLinear (\ ~(a, b) -> f a b)

This can be extended to tuples of various sizes. Another approach that can be used in parallel is

ensure2 :: (a, b) %p -> (a, b)
ensure2 = Unsafe.toLinear $ \ ~(a, b) -> (a, b)

we can easily offer a Generic version of the latter that works with all sorts of Generic records.

[treeowl]

Hmmm.... That particular Generic approach doesn't work when there are strict fields. We can, however, make Generic lazy uncurry functions, and also lazily unpack generic records into tuples.

[treeowl]

OK, here's the best I've come up with:

-- | Uncurry lazily. This can be used for any non-nullary record type with
-- a 'Generic' instance.
--
-- @
-- lazyUncurry :: (a %1-> b %1-> c) %1-> (a, b) %1-> c
-- lazyUncurry :: (a %1 -> b %1-> c %1-> d) %1-> (a, b, c) %1-> d
-- lazyUncurry :: (a %1 -> b %1-> c %1-> d %1-> e) %1-> (a, b, c, d) %1-> e
-- @
lazyUncurry :: (Generic a, Uncurry fun (Rep a) r) => fun %p-> a %q-> r
lazyUncurry f a = uncurry' f (from a)

type family Unc f r where
  Unc (M1 _ _ f) r = Unc f r
  Unc (K1 _ c) r = c %1-> r
  Unc (MP1 p (K1 _ c)) r = c %p-> r
  Unc (f :*: g) r = Unc f (Unc g r)

class fun ~ Unc f r => Uncurry fun f r where
  uncurry' :: fun %1-> f a %1-> r

instance Uncurry fun f r => Uncurry fun (M1 i c f) r where
  uncurry' f (M1 x) = uncurry' f x
  {-# INLINE uncurry' #-}

instance fun ~ (c %1-> r) => Uncurry fun (K1 i c) r where
  uncurry' f (K1 x) = f x
  {-# INLINE uncurry' #-}

instance forall fun c p r i. fun ~ (c %p-> r) => Uncurry fun (MP1 p (K1 i c)) r where
  uncurry' f = Unsafe.toLinear ((\ ~(MP1 (K1 x)) -> f x) :: MP1 p (K1 i c) a -> r)
  {-# INLINE uncurry' #-}

instance (Uncurry fun f fun', Uncurry fun' g r) => Uncurry fun (f :*: g) r where
  uncurry' f = Unsafe.toLinear (\ ~(x :*: y) -> uncurry' (uncurry' f x) y)
  {-# INLINE uncurry' #-}

[treeowl]

This can be used, for example, to define splitAt:

splitAt :: Int -> [a] %1-> ([a], [a])
splitAt n ls
  | n <= 0 = ([], ls)
  | otherwise          = splitAt' n ls
    where
        splitAt' :: Int -> [a] %1-> ([a], [a])
        splitAt' _  []     = ([], [])
        splitAt' 1  (x:xs) = ([x], xs)
        splitAt' m  (x:xs) = lazyUncurry (\xs' xs'' -> (x:xs', xs'')) (splitAt' (m - 1) xs) 

[aspiwack]

As I've commented in the GHC issue, I think we should be quite careful before considering such things as linear. I suppose that we can argue that with current knowledge, the implementation of splitAt with Unsafe.toLinear is incorrect.

[treeowl]

I think we either need to take a principled stand (and refrain from using toLinear to improve performance) or accept something a bit less principled but more general. Scattering the trusted base all over the place is a bad practice.

[aspiwack]

I agree. I don't think it was on purpose that we wrongly used toLinear in splitAt, we were just sloppy.