Linear resources.hs

{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE EmptyDataDecls #-}
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE ScopedTypeVariables #-}


module Main where

import GHC.TypeLits
import GHC.Prim
import Data.Type.List

import Data.Proxy

import Control.Monad.Indexed

data L (n :: Nat) (is :: [Nat])


newtype Linear p i o a
  = Linear (p a)

newtype Resource (n :: Nat) a = Res a

allocate :: (m ~ (n + 1), os ~ (Insert n is), Functor p)
         => p a
         -> Linear p (L n is) (L m os) (Resource n a)
allocate x = Linear $ fmap Res x


consume :: (Find q is ~ 'True, os ~ Remove q is)
        => Resource q a
        -> (a -> p b)
        -> Linear p (L n is) (L n os) b
consume (Res x) f = Linear (f x)

runLinear :: KnownNat m => Linear p (L 0 '[]) (L m '[]) a -> p a
runLinear (Linear x) = x

starting :: (KnownNat m) => Linear p (L 0 '[]) (L m os) a -> Linear p (L 0 '[]) (L m os) a
starting x = x

-- test1 :: Linear IO (L n '[]) (L (n+3) '[]) ()
-- test1 :: Linear IO (L n '[]) (L (((n+1)+1)+1) '[]) ()
-- test1 :: Linear IO (L 0 '[]) (L (3) '[]) ()
test1 =
    allocate getLine >>>= \l0 ->
    allocate getLine >>>= \l1 ->
    consume l0 print >>>= \_ ->
    allocate getLine >>>= \l2 ->
    consume l2 print >>>= \_ ->
    consume l1 print
--
-- runLinear' :: (KnownNat m, Functor p) => Linear p (L 0 '[]) (L m '[]) a -> p (a,Integer)
-- runLinear' (Linear x) = fmap (,natVal' (proxy# :: Proxy# m)) x


instance Functor p => IxFunctor (Linear p) where
  imap f (Linear x) = Linear (fmap f x)

instance Applicative p => IxPointed (Linear p) where
  ireturn x = Linear (pure x)

instance Applicative p => IxApplicative (Linear p) where
  iap (Linear pf) (Linear px) = Linear (pf <*> px)

instance Monad p => IxMonad (Linear p) where
  ibind f (Linear a) = Linear (a >>= \x -> let (Linear y) = f x in y)


main :: IO ()
main = do
  runLinear $
    allocate getLine >>>= \l0 ->
    allocate getLine >>>= \l1 ->
    consume l0 print >>>= \_ ->
    allocate getLine >>>= \l2 ->
    consume l2 print >>>= \_ ->
    consume l1 print