Skip to content
Create a gist now

Instantly share code, notes, and snippets.

Embed URL


Subversion checkout URL

You can clone with
Download ZIP
Can you break my shitty linear resource monad transformer? Looking for people to find ways that it's unsafe.
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE LiberalTypeSynonyms #-}
{-# LANGUAGE ImplicitParams #-}
{-# LANGUAGE NoImplicitPrelude #-}
{-# LANGUAGE RebindableSyntax #-}
module Resource where
import qualified Prelude as P
import Prelude (Eq, Show, undefined, Integral, fromInteger, id, (.), ($), const, Monad, String, Bool(True, False))
import Control.Monad (liftM)
fail :: String -> a
fail = P.error
class IMonad m where
return :: a -> m i i a
(>>=) :: m i j a -> (a -> m j k b) -> m i k b
(>>) :: IMonad m => m i j a -> m j k b -> m i k b
x >> y = x >>= const y
data Nat = Z | S Nat
type State = (Nat, [Nat]) -- why can't I promote this?
-- Other substructural flavors probably work too, but I don't need them now
class Linear (xs :: [Nat])
instance Linear '[]
instance Linear xs => Linear (S Z ': xs)
newtype Ref (n :: Nat) s a = Ref { getRef :: a }
-- Eww, when I said linear types, I didn't mean O(n)
-- This is also annoying because it doesn't reduce immediately and leads to massive types. I welcome improvements!
type family Grow (xs :: [Nat]) :: [Nat]
type instance Grow '[] = '[Z]
type instance Grow (x ': xs) = x ': Grow xs
type family Use (n :: Nat) (xs :: [Nat]) :: [Nat]
type instance Use Z (x ': xs) = S x ': xs
type instance Use (S i) (x ': xs) = x ': Use i xs
newtype Res s m (i :: (Nat, [Nat])) (j :: (Nat, [Nat])) a = Res { _runRes :: m a }
instance Monad m => IMonad (Res s m) where
return = Res . P.return
x >>= f = Res $ _runRes x P.>>= _runRes . f
create :: Monad m => m a -> Res s m '(i, xs) '(S i, Grow xs) (Ref i s a)
create x = Res (liftM Ref x)
consume :: Monad m => Ref i s a -> Res s m '(j, xs) '(j, Use i xs) a
consume (Ref x) = Res $ P.return x
newtype Conjoined s m i a = Conjoined { runConjoined :: forall j ys. Res s m '(j, ys) '(S j, Grow (Use i ys)) (Ref j s a) }
conjoin :: Monad m => m (m a) -> Res s m '(i, xs) '(S i, Grow xs) (Conjoined s m i a)
conjoin before = Res $ before P.>>= \after -> P.return (Conjoined (Res (liftM Ref after)))
runRes :: Linear xs => (forall s. Res s m '(Z, '[]) '(j, xs) a) -> m a
runRes (Res x) = x
-- Pretend constructors etc. aren't exported. Gah I wish Haskell had real modules.
newtype Id a = Id a deriving (Eq, Show)
instance Monad Id where
return = Id
Id x >>= f = Id (case f x of Id x' -> x')
zomg = conjoin (Id (Id "bar"))
test = do
x <- create (Id "foo")
y <- create (Id True)
Conjoined foo <- zomg
consume y
z <- create (Id 5)
consume x
a <- foo
consume a
consume z
run = runRes test
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Something went wrong with that request. Please try again.