little 'indexed' library

IxFunctor.hs

{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE Trustworthy #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FunctionalDependencies  #-}
{-# LANGUAGE FlexibleInstances  #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  Indexed.Types
-- Copyright   :  (C) 2012-2015 Edward Kmett
-- License     :  BSD-style (see the file LICENSE)
-- Maintainer  :  Edward Kmett <ekmett@gmail.com>
-- Stability   :  experimental
-- Portability :  non-portable
--
-- Common types that are useful for working with indexed functors
-----------------------------------------------------------------------------
module IxFunctor   where

import Control.Category
import Data.Data as Data
import Data.Monoid
import Data.Type.Equality
import Prelude hiding (id,(.))
import Unsafe.Coerce
-- for the file handle illustration:
import System.FilePath
import System.IO
import Control.Exception 
import System.Environment
-------------------------------------------------------------------------------
-- Natural Transformations
-------------------------------------------------------------------------------

infixr 0 ~>
-- | A natural transformation from @f@ to @g@
type f ~> g = forall x. f x -> g x

infixr 0 :~>, $$
-- | A natural transformation suitable for storing in a container.
newtype f :~> g = Nat { ($$) :: f ~> g }
  deriving Typeable

instance f ~ g => Monoid (f :~> g) where
  mempty = Nat id
  mappend (Nat f) (Nat g) = Nat (f . g)

-------------------------------------------------------------------------------
-- Atkey
-------------------------------------------------------------------------------
data At :: * -> k -> k -> * where 
  At :: a -> At a k k
 deriving Typeable

instance Show a => Show (At a i j) where
  showsPrec d (At a) = showParen (d > 10) $
    showString "At " . showsPrec 11 a

instance (Read a, i ~ j) => Read (At a i j) where
  readsPrec d = readParen (d > 10) $ \r -> do
    ("At", s) <- lex r
    (k, t) <- readsPrec 11 s
    return (At k, t)

instance Eq a => Eq (At a i j) where
  At m == At n = m == n

instance Ord a => Ord (At a i j) where
  At m `compare` At n = compare m n

-- | Project out the value
key :: At a i j -> a
key (At a) = a

instance Monoid m => Category (At m) where
  id          = At mempty
  At m . At n = At (m <> n)

instance (Monoid m, i ~ j) => Monoid (At m i j) where
  mempty              = At mempty
  At m `mappend` At n = At (mappend m n)

-- | Type alias for indexed monads, functors, etc. in Bob Atkey's style.
type Atkey f i j a = f (At a j) i


infixl 4 /$/, /*/, /*, */
infixl 1 ?>=, !>=
infixr 1 >~>, <~< 

-- | A 'Functor' between indexed categories.
class IFunctor f where
  imap :: (a ~> b) -> f a ~> f b


(/$/) :: IFunctor f => (a ~> b) -> f a ~> f b
(/$/) = imap

imapAt :: IFunctor f => (a -> b) -> f (At a k) ~> f (At b k)
imapAt f = imap (\(At a) -> At (f a))
{-# INLINE imapAt #-} 

class IFunctor f => IApplicative f where
  ireturn :: a ~> f a

  (/*/) :: f (At (a -> b) j) i -> f (At a k) j -> f (At b k) i
  default (/*/) :: IMonad f => f (At (a -> b) j) i -> f (At a k) j -> f (At b k) i
  mf /*/ ma = mf !>= \f -> ma !>= \a -> ireturnAt (f a)

  (/*) :: f (At a j) i -> f (At b k) j -> f (At a k) i
  ma /* mb = imapAt const ma /*/ mb

  (*/) :: f (At a j) i -> f (At b k) j -> f (At b k) i
  ma */ mb = imapAt (const id) ma /*/ mb

ireturnAt :: IApplicative m => a -> m (At a i) i
ireturnAt a = ireturn (At a)
 
class IApplicative m => IMonad m where
  ibind   :: (a ~> m b) -> m a ~> m b
  ijoin   :: m (m a) ~> m a

  ijoin   = ibind id
  ibind f = ijoin . imap f

(>~>) :: IMonad m => (a ~> m b) -> (b ~> m c) -> a ~> m c
f >~> g = ibind g . f

(<~<) :: IMonad m => (b ~> m c) -> (a ~> m b) -> a ~> m c
f <~< g = ibind f . g

-- @
-- m '?>=' 'ireturn' ≡ m
-- 'ireturn' a '?>=' f ≡ f a
-- (m '?>=' f) '?>=' g ≡ m '?>=' \x -> f x '?>=' g
-- @
(?>=) :: IMonad m => m a i -> (a ~> m b) -> m b i
m ?>= f = ibind f m

(!>=) :: IMonad (m :: (x -> *) -> x -> *) => m (At a j) i -> (a -> m b j) -> m b i
m !>= f = m ?>= \ (At a) -> f a


-------------------------------------------------------------------------------
-- ($)
-------------------------------------------------------------------------------

infixr 0 $
-- | A type level version of @('$')@, useful to avoid parentheses
type ($) a = a

---------------------------
-- Free
---------------------------


class IMonad m => IMonadFree f m | m -> f where
  ifree :: f (m a) ~> m a


data Free f a i where
  Return :: a i -> Free f a i
  Free   :: f (Free f a) i -> Free f a i

instance IFunctor f => IFunctor (Free f) where
  imap f (Return a) = Return (f a)
  imap f (Free as)  = Free (imap (imap f) as)

instance IFunctor f => IApplicative (Free f) where
  ireturn = Return
  
instance IFunctor f => IMonad (Free f) where
  ibind f (Return a) = f a
  ibind f (Free as) = Free (imap (ibind f) as)

instance IFunctor f => IMonadFree f (Free f) where
  ifree = Free
  --  
-- | A CPS'd Free Monad, Church-encoded.
newtype Church f a i = Church { runChurch :: forall r. (a ~> r) -> (f r ~> r) -> r i }

instance IFunctor (Church f) where
  imap f m = Church $ \kp -> runChurch m (kp . f)

instance IApplicative (Church f) where
  ireturn a = Church $ \k _ -> k a

instance IMonad (Church f) where
  ibind f m = Church $ \k kf -> runChurch m (\a -> runChurch (f a) k kf) kf


instance IFunctor f => IMonadFree f (Church f) where
  ifree as = Church $ \k kf -> kf (imap (\ m -> runChurch m k kf) as)

-- | Go 'Free'.
improve :: Church f a ~> Free f a
improve m = runChurch m Return Free

--------------------------------
-- McBride's file handle example
--------------------------------
-- Nb, this is the inefficient form that retraverses binds
-- so only try 'myReadFile' on small files!
-- One would prefer the church encoded variant of free


data FHState = FOpen | FClosed

data FHSTATE :: FHState -> * where -- typical singletons
  FOPEN    :: FHSTATE FOpen
  FCLOSED  :: FHSTATE FClosed

data FH :: (FHState -> *) -> FHState -> * where
  FHOpen   :: FilePath -> (FHSTATE ~> q) -> FH q FClosed
  FHClose  :: q FClosed -> FH q FOpen
  FHRead   :: (Maybe Char -> q FOpen) -> FH q FOpen

instance IFunctor FH where
  imap f (FHOpen s k) = FHOpen s (f . k)
  imap f (FHClose q) = FHClose (f q)
  imap f (FHRead k) = FHRead (f . k)

fhOpen :: FilePath -> Free FH FHSTATE FClosed
fhOpen f = Free $ FHOpen f Return

fhClose :: Free FH (At () FClosed) FOpen
fhClose = Free . FHClose . Return $ At ()

fhRead :: Free FH (At (Maybe Char) FOpen) FOpen
fhRead = Free . FHRead $ \ c -> Return (At c)

runFH :: Free FH (At a FClosed) FClosed -> IO a
runFH (Return (At a)) = return a
runFH (Free (FHOpen s f)) = catch
   (openFile s ReadMode >>= openFH (f FOPEN))
   (\(SomeException _) -> runFH (f FCLOSED))

openFH :: Free FH (At a 'FClosed) 'FOpen-> Handle -> IO a
openFH (Free (FHClose k)) h = hClose h >> runFH k
openFH (Free (FHRead f)) h = catch
          (hGetChar h >>= \ c -> openFH (f (Just c)) h)
          (\(SomeException _) -> openFH (f Nothing) h)

myReadFile :: FilePath -> IO (Maybe String)
myReadFile s = runFH $ ibind check (fhOpen s)  where
  check :: FHSTATE ~> (Free FH (At (Maybe String) FClosed))
  check FCLOSED = Return (At Nothing)
  check FOPEN = grab !>= \ s -> fhClose !>= \ _ -> Return (At (Just s))
  grab :: (Free FH (At String FOpen)) FOpen
  grab = fhRead !>= \ x -> case x of
    Nothing -> Return (At "")
    Just c -> grab !>= \ cs -> Return (At (c : cs))