{-# LANGUAGE LinearTypes #-}
{-# LANGUAGE GADTs #-}

module Data.Unrestricted.Internal.Ur
  (
    Ur(..)
  , unur
  , lift
  , lift2
  ) where

-- | @Ur a@ represents unrestricted values of type @a@ in a linear
-- context. The key idea is that because the contructor holds @a@ with a
-- regular arrow, a function that uses @Ur a@ linearly can use @a@
-- however it likes.
-- > someLinear :: Ur a %1-> (a,a)
-- > someLinear (Ur a) = (a,a)
data Ur a where
  Ur :: a -> Ur a

-- | Get an @a@ out of an @Ur a@. If you call this function on a
-- linearly bound @Ur a@, then the @a@ you get out has to be used
-- linearly, for example:
--
-- > restricted :: Ur a %1-> b
-- > restricted x = f (unur x)
-- >   where
-- >     -- f __must__ be linear
-- >     f :: a %1-> b
-- >     f x = ...
unur :: Ur a %1-> a
unur :: forall a. Ur a %1 -> a
unur (Ur a
a) = a
a

-- | Lifts a function on a linear @Ur a@.
lift :: (a -> b) -> Ur a %1-> Ur b
lift :: forall a b. (a -> b) -> Ur a %1 -> Ur b
lift a -> b
f (Ur a
a) = b -> Ur b
forall a. a -> Ur a
Ur (a -> b
f a
a)

-- | Lifts a function to work on two linear @Ur a@.
lift2 :: (a -> b -> c) -> Ur a %1-> Ur b %1-> Ur c
lift2 :: forall a b c. (a -> b -> c) -> Ur a %1 -> Ur b %1 -> Ur c
lift2 a -> b -> c
f (Ur a
a) (Ur b
b) = c -> Ur c
forall a. a -> Ur a
Ur (a -> b -> c
f a
a b
b)