File handles with type-level verification that you use them properly

Handles.hs

{-# LANGUAGE GADTs            #-}
{-# LANGUAGE DataKinds        #-}
{-# LANGUAGE PolyKinds        #-}
{-# LANGUAGE KindSignatures   #-}
{-# LANGUAGE TypeFamilies     #-}
{-# LANGUAGE TypeOperators    #-}
{-# LANGUAGE RankNTypes       #-}
{-# LANGUAGE ConstraintKinds  #-}
{-# LANGUAGE RebindableSyntax #-}

module Handles where

import Prelude hiding ( Read , (>>=) , (>>) , return , ifThenElse )
import qualified Prelude as P
import Control.Applicative
import qualified System.IO as IO

-- Indexed things...

class IxFunctor f where
   imap :: (a -> b) -> f j k a -> f j k b

class IxPointed m => IxApplicative m where
   iap :: m i j (a -> b) -> m j k a -> m i k b

class IxFunctor m => IxPointed m where
   ireturn :: a -> m i i a

class IxApplicative m => IxMonad m where
   ibind :: (a -> m j k b) -> m i j a -> m i k b

ijoin :: IxMonad m => m i j (m j k a) -> m i k a 
ijoin = ibind id

infixr 1 =<<<
infixl 1 >>>=

(>>>=) :: IxMonad m => m i j a -> (a -> m j k b) -> m i k b
m >>>= k = ibind k m 

(=<<<) :: IxMonad m => (a -> m j k b) -> m i j a -> m i k b
(=<<<) = ibind

-- Rebinding syntax...

infixl 1 >>=
(>>=) :: IxMonad m => m i j a -> (a -> m j k b) -> m i k b
(>>=) = (>>>=)

(>>) :: IxMonad m => m i j a -> m j k b -> m i k b
a >> b = a >>= \_ -> b

return :: IxMonad m => a -> m i i a
return = ireturn

ifThenElse :: Bool -> x -> x -> x
ifThenElse b x y = if b then x else y 

-- Types and stuff...

data Nat = Z | S Nat

infixr :::
data List a = a ::: List a | Nil

type family Length l where
   Length Nil        = Z
   Length (x ::: xs) = S (Length xs)

type family Get i l where
   Get Z     (x ::: xs) = x
   Get (S n) (x ::: xs) = Get n xs

type family Set i x l where
   Set Z     x' (x ::: xs) = x' ::: xs
   Set (S n) x' (x ::: xs) = x  ::: Set n x' xs

type family Tack x l where
   Tack x Nil        = x ::: Nil
   Tack x (y ::: ys) = y ::: Tack x ys

type family AllEqualTo x l where
   AllEqualTo x Nil        = True
   AllEqualTo x (x ::: xs) = AllEqualTo x xs
   AllEqualTo x y          = False

type All x l = AllEqualTo x l ~ True

-- Handles...

data OpenMode = Read | Write

data HandleMode = Open OpenMode | Closed

data Mode (m :: HandleMode) where
   ReadMode   :: Mode (Open Read)
   WriteMode  :: Mode (Open Write)
   ClosedMode :: Mode Closed

newtype Handles (s :: List HandleMode) (t :: List HandleMode) a = Handles { getHandles :: IO a }

instance IxFunctor Handles where
   imap f = Handles . fmap f . getHandles

instance IxPointed Handles where
   ireturn = Handles . P.return

instance IxApplicative Handles where
   f `iap` x = Handles (getHandles f <*> getHandles x)

instance IxMonad Handles where
   ibind f x = Handles (getHandles x P.>>= getHandles . f)

data Handle i = Handle { close     :: forall s m. (Get i s ~ Open m)     => Handles s (Set i Closed s) ()
                       , readLine  :: forall s.   (Get i s ~ Open Read)  => Handles s s String 
                       , writeLine :: forall s.   (Get i s ~ Open Write) => String -> Handles s s () }

openFile :: IO.FilePath -> Mode (Open m) -> Handles s (Tack (Open m) s) (Handle (Length s))
openFile path mode = do
   h <- Handles $
      IO.openFile path $ case mode of
         ReadMode  -> IO.ReadMode
         WriteMode -> IO.WriteMode
   return $ Handle (Handles $ IO.hClose    h)
                   (Handles $ IO.hGetLine  h)
                   (Handles . IO.hPutStrLn h)

runHandles :: (All Closed t) => Handles Nil t a -> IO a
runHandles = getHandles

-- Prevent handle leakage ala ST monad?
-- Handle (hah) cases where handles can't be opened via Maybe?

test :: IO ()
test = runHandles $ do
   x <- openFile "x.txt" ReadMode
   y <- openFile "y.txt" WriteMode
   readLine x >>= writeLine y
   close x
   close y