Lowering of higher order function with linear types-CodePudding

I've been experimenting with linear types recently, and have been wondering if the following transformation is possible. It's definitely not valid without linear types.

The aim is to lower the higher order function argument. This should be ok, because linear types ensure the HOF is called exactly once, so exactly 1 value of a exists. The issue is how to escape the lambda and observe a

   lower :: ((a %1-> b) %1-> r) %1-> b %1-> (r,a)

CodePudding user response：

Edit: You cannot safely implement lower. As dfeuer and danidiaz say in comments: what if the first argument to lower is the identity function? With the implementation I showed in my old answer below you can write:

main :: IO ()
main = putStrLn (snd (lower (\x -> x) False))

Which will produce an error at run time:

Lin: Prelude.undefined
CallStack (from HasCallStack):
  error, called at libraries/base/GHC/Err.hs:74:14 in base:GHC.Err
  undefined, called at Lin.hs:25:19 in main:Main

So linear types do not give enough guarantees to make it safe to implement this function.

Edit2: You can save the situation by slightly changing the signature to: lower :: ((a %1 -> b) %1 -> Ur r) %1 -> b %1 -> (Ur r, a). This way it is impossible to store the linear argument a %1 -> b in r.

import Control.Exception (evaluate)

-- from Data.Unrestricted.Linear from linear-base
data Ur a where
  Ur :: a -> Ur a

lower :: ((a %1 -> b) %1 -> Ur r) %1 -> b %1 -> (Ur r, a)
lower = toLinear2 lower'

lower' :: ((a %1 -> b) %1 -> Ur r) -> b -> (Ur r, a)
lower' f b = unsafePerformIO $ do
  ref <- newIORef undefined
  r <- evaluate $ f (toLinear (\a -> unsafePerformIO $ b <$ writeIORef ref a))
  a <- readIORef ref
  pure (r, a)

Old answer

This may not be the answer you are looking for, but if you know for sure that it is safe, then you can bend the rules a bit:

{-# LANGUAGE LinearTypes, GADTs #-}
import System.IO.Unsafe
import Data.IORef
import Unsafe.Coerce
import Control.Exception (evaluate)

-- 'coerce', 'toLinear' and 'toLinear2' are also found in Unsafe.Linear from linear-base

coerce :: forall a b. a %1-> b
coerce a =
  case unsafeEqualityProof @a @b of
    UnsafeRefl -> a
{-# INLINE coerce #-}

toLinear :: (a %p-> b) %1-> (a %1-> b)
toLinear = coerce

toLinear2 :: (a %p-> b %q-> c) %1-> (a %1-> b %1-> c)
toLinear2 = coerce

lower :: ((a %1 -> b) %1 -> r) %1 -> b %1 -> (r, a)
lower = toLinear2 lower'

lower' :: ((a %1 -> b) %1 -> r) -> b -> (r, a)
lower' f b = unsafePerformIO $ do
  ref <- newIORef undefined
  r <- evaluate $ f (toLinear (\a -> unsafePerformIO $ b <$ writeIORef ref a))
  a <- readIORef ref
  pure (r, a)

I think the main purpose of linear types is only to get the extra type-level information, so I don't think there are any safe primitives that let you do this more cleanly (although I don't know all the ins and outs). Linear types do allow you to implement a safe interface with unsafe operations underneath. See for example how many times toLinear is used in this file from linear-base.

Perhaps the unsafe bits above can be outsourced to a lower-level library. Maybe something like promises, but then with linear types.