Last active

Embed URL

HTTPS clone URL

SSH clone URL

You can clone with HTTPS or SSH.

Download Gist

Can you break my shitty linear resource monad transformer? Looking for people to find ways that it's unsafe.

View Resource.hs
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89
{-# 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.