Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
little 'indexed' library
{-# 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))
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.