-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/
-- | A collection of Oleg Kiselyov's Haskell modules (2009-2008)
--
-- A collection of Oleg Kiselyov's Haskell modules (2009-2008) (released
-- with his permission)
@package liboleg
@version 0.2
-- | http://okmij.org/ftp/Haskell/regions.html#light-weight
--
-- Lightweight monadic regions
--
--
-- - The Abstract of the paper We present Haskell libraries that
-- statically ensure the safe use of resources such as file handles. We
-- statically prevent accessing an already closed handle or forgetting to
-- close it. The libraries can be trivially extended to other resources
-- such as database connections and graphic contexts.
--
--
-- Because file handles and similar resources are scarce, we want to not
-- just assure their safe use but further deallocate them soon after they
-- are no longer needed. Relying on Fluet and Morrisett's calculus of
-- nested regions, we contribute a novel, improved, and extended
-- implementation of the calculus in Haskell, with file handles as
-- resources.
--
-- Our library supports region polymorphism and implicit region
-- subtyping, along with higher-order functions, mutable state,
-- recursion, and run-time exceptions. A program may allocate arbitrarily
-- many resources and dispose of them in any order, not necessarily LIFO.
-- Region annotations are part of an expression's inferred type. Our new
-- Haskell encoding of monadic regions as monad transformers needs no
-- witness terms. It assures timely deallocation even when resources have
-- markedly different lifetimes and the identity of the longest-living
-- resource is determined only dynamically.
--
-- For contrast, we also implement a Haskell library for manual resource
-- management, where deallocation is explicit and safety is assured by a
-- form of linear types. We implement the linear typing in Haskell with
-- the help of phantom types and a parameterized monad to statically
-- track the type-state of resources.
--
-- Joint work with Chung-chieh Shan.
--
-- Handle-based IO with the assured open/close protocol, see README This
-- file contains the Security kernel. See SafeHandlesTest.hs for tests.
-- This is the final solution: lightweight monadic regions with only
-- type-level enforcement of region discipline
module System.SafeHandles
-- | The IO monad with safe handles and regions (SIO) is implemented as the
-- monad transformer IORT (recursively) applied to IO.
--
-- Each region maintains the state listing all open handles assigned to
-- the region. Since we already have IO, it is easy to implement the
-- state as a mutable list (IORef of the list) and make this reference a
-- pervasive environment. We could have used implicit parameters or
-- implicit configurations to pass that IORef around. Here, we use
-- ReaderT.
data IORT s m v
type SIO s = IORT s IO
-- | Our (safe) handle is labeled with the monad where it was created
data SHandle m :: (* -> *)
runSIO :: (forall s. SIO s v) -> IO v
-- | There is no explicit close operation. A handle is automatically closed
-- when its region is finished (normally or abnormally).
newRgn :: (RMonadIO m) => (forall s. IORT s m v) -> m v
-- | Lift from one IORT to an IORT in a children region... IORT should be
-- opaque to the user: hence this is not the instance of MonadTrans
liftSIO :: (Monad m) => IORT s m a -> IORT s1 (IORT s m) a
-- | Create a new handle and assign it to the current region One can use
-- liftIORT (newSHandle ...) to assign the handle to any parent region.
newSHandle :: (RMonadIO m) => FilePath -> IOMode -> IORT s m (SHandle (IORT s m))
-- | Duplicate a handle, returning a handle that can be used in the parent
-- region (and can be returned from the current region as the result).
-- This operation prolongs the life of a handle based on a _dynamic_
-- condition. If we know the lifetime of a handle statically, we can
-- execute liftSIO (newSHandle ...) to place the handle in the
-- corresponding region. If we don't know the lifetime of a handle
-- statically, we place it in the inner region, and then extend its
-- lifetime by reassigning to the parent region based on the dynamic
-- conditions.
shDup :: (RMonadIO m) => SHandle (IORT s1 (IORT s m)) -> IORT s1 (IORT s m) (SHandle (IORT s m))
data IOMode :: *
ReadMode :: IOMode
WriteMode :: IOMode
AppendMode :: IOMode
ReadWriteMode :: IOMode
-- | Safe-handle-based IO... The handle is assigned to the current region
-- or its ancestor. So, we have to verify that the label of the handle is
-- the prefix (perhaps improper) of the label of the monad (label of the
-- region).
shGetLine :: (MonadRaise m1 m2, RMonadIO m2) => SHandle m1 -> m2 String
shPutStrLn :: (MonadRaise m1 m2, RMonadIO m2) => SHandle m1 -> String -> m2 ()
shIsEOF :: (MonadRaise m1 m2, RMonadIO m2) => SHandle m1 -> m2 Bool
-- | It seems however that IOErrors don't invalidate the Handles. For
-- example, if EOF is reported, we may try to reposition the
-- file and read again. That's why in Posix, EOF and file errors
-- can be cleared.
shThrow :: (RMonadIO m) => Exception -> m a
shCatch :: (RMonadIO m) => m a -> (Exception -> m a) -> m a
-- | Useful for debugging
shReport :: (RMonadIO m) => String -> m ()
-- | make IORef available with SIO, so we may write tests that attempt to
-- leak handles and computations with handles via assignment
sNewIORef :: (RMonadIO m) => a -> m (IORef a)
sReadIORef :: (RMonadIO m) => IORef a -> m a
sWriteIORef :: (RMonadIO m) => IORef a -> a -> m ()
instance [overlap ok] (Monad m) => Monad (IORT s m)
instance [overlap ok] TypeCast2'' () a a
instance [overlap ok] (TypeCast2'' t a b) => TypeCast2' t a b
instance [overlap ok] (TypeCast2' () a b) => TypeCast2 a b
instance [overlap ok] TypeCast'' () a a
instance [overlap ok] (TypeCast'' t a b) => TypeCast' t a b
instance [overlap ok] (TypeCast' () a b) => TypeCast a b
instance [overlap ok] (RMonadIO m) => RMonadIO (IORT s m)
instance [overlap ok] (RMonadIO m) => RMonadIO (ReaderT r m)
instance [overlap ok] RMonadIO IO
instance [overlap ok] (Monad m2, TypeCast2 m2 (IORT s m2'), MonadRaise m1 m2') => MonadRaise m1 m2
instance [overlap ok] (Monad m) => MonadRaise m m
-- | Low-level IO operations These operations are either missing from the
-- GHC run-time library, or implemented suboptimally or heavy-handedly
module System.LowLevelIO
-- | Alas, GHC provides no function to read from Fd to an allocated buffer.
-- The library function fdRead is not appropriate as it returns a string
-- already. I'd rather get data from a buffer. Furthermore, fdRead (at
-- least in GHC) allocates a new buffer each time it is called. This is a
-- waste. Yet another problem with fdRead is in raising an exception on
-- any IOError or even EOF. I'd rather avoid exceptions altogether.
myfdRead :: Fd -> Ptr CChar -> ByteCount -> IO (Either Errno ByteCount)
-- | The following fseek procedure throws no exceptions.
myfdSeek :: Fd -> SeekMode -> FileOffset -> IO (Either Errno FileOffset)
-- | Haskell representation for errno values. The implementation
-- is deliberately exposed, to allow users to add their own definitions
-- of Errno values.
newtype Errno :: *
Errno :: CInt -> Errno
-- | poll if file descriptors have something to read Return the list of
-- read-pending descriptors
select'read'pending :: [Fd] -> IO (Either Errno [Fd])
-- | http://okmij.org/ftp/Haskell/misc.html#sys_open
--
-- Haskell interface to sys_open.c: providing openFd and closeFd that can
-- deal with extended file names (which can name TCP and
-- bi-directional pipes in addition to the regular disk files)
-- http://okmij.org/ftp/syscall-interpose.html#Application
--
-- Also included a useful utility read_line to read a NL-terminated line
-- from an Fd. It deliberately uses no handles and so never messes with
-- Fd (in particular, it doesn't put the file descriptor in the
-- non-blocking mode)
--
-- Simple and reliable uni- and bi-directional pipes
--
-- MySysOpen module offers a reliable, proven way of interacting with
-- another local or remote process via a unidirectional or bidirectional
-- channel. It supports pipes and Unix and TCP sockets. MySysOpen is a
-- simple and explicit alternative to the multi-threaded IO processing of
-- the GHC run-time system. The module is the Haskell binding to sys_open
-- -- the extended, user-level file opening interface.
--
-- The second half of MySysOpen.hs contains several bi-directional
-- channel interaction tests. One checks repeated sending and receiving
-- of data; the amount of received data is intentionally large, about
-- 510K. Two other tests interact with programs that are not specifically
-- written for interactive use, such as sort. The latter cannot produce
-- any output before it has read all of the input, accepting no input
-- terminator other than the EOF condition. One test uses shutdown to set
-- the EOF condition. The other test programs the handler for a custom
-- EOF indicator, literally in the file name of the communication pipe.
module System.SysOpen
mysysOpenFd :: FilePath -> OpenMode -> Maybe FileMode -> IO Fd
mysysCloseFd :: Fd -> IO ()
-- | Close the output direction of the bi-directional pipe
mysysCloseOut :: Fd -> IO ()
read_line :: [Char] -> Fd -> IO ([Char], [Char])
-- |
-- http://okmij.org/ftp/typed-formatting/FPrintScan.html#print-show
--
-- Generic polyvariadic printf in Haskell98
--
-- This generalization of Text.Printf.printf is inspired by the message
-- of Evan Klitzke, who wrote on Haskell-Cafe about frequent occurrences
-- in his code of the lines like
--
--
-- infoM $ printf "%s saw %s with %s" (show x) (show y) (show z)
--
--
-- Writing show on and on quickly becomes tiresome. It turns out, we can
-- avoid these repeating show, still conforming to Haskell98.
--
-- Our polyvariadic generic printf is like polyvariadic show with the
-- printf-like format string. Our printf handles values of any present
-- and future type for which there is a Show instance. For example:
--
--
-- t1 = unR $ printf "Hi there"
-- -- "Hi there"
--
--
--
-- t2 = unR $ printf "Hi %s!" "there"
-- -- "Hi there!"
--
--
--
-- t3 = unR $ printf "The value of %s is %s" "x" 3
-- -- "The value of x is 3"
--
--
--
-- t4 = unR $ printf "The value of %s is %s" "x" [5]
-- -- "The value of x is [5]"
--
--
-- The unsightly unR appears solely for Haskell98 compatibility: flexible
-- instances remove the need for it. On the other hand, Evan Klitzke's
-- code post-processes the result of formatting with infoM, which can
-- subsume unR.
--
-- A bigger problem with our generic printf, shared with the original
-- Text.Printf.printf, is partiality: The errors like passing too many or
-- too few arguments to printf are caught only at run-time. We can
-- certainly do better.
--
-- Version: The current version is 1.1, June 5, 2009.
--
-- References
--
--
module Text.GenPrintF
-- | Needed only for the sake of Haskell98 If we are OK with flexible
-- instances, this newtype can be disposed of
newtype RString
RString :: String -> RString
unR :: RString -> String
class SPrintF r
pr_aux :: (SPrintF r) => [FDesc] -> [String] -> r
-- | A very simple language of format descriptors
data FDesc
FD_lit :: String -> FDesc
FD_str :: FDesc
convert_to_fdesc :: String -> [FDesc]
instance Eq FDesc
instance Show FDesc
instance (Show a, SPrintF r) => SPrintF (a -> r)
instance SPrintF RString
-- | The final view to the typed sprintf and sscanf
--
-- http://okmij.org/ftp/typed-formatting/FPrintScan.html
--
-- This code defines a simple domain-specific language of string patterns
-- and demonstrates two interpreters of the language: for building
-- strings (sprintf) and parsing strings (sscanf). This code thus solves
-- the problem of typed printf/scanf sharing the same format string posed
-- by Chung-chieh Shan. This code presents scanf/printf interpreters in
-- the final style; it is thus the dual of the code in PrintScan.hs
--
-- Version: The current version is 1.1, Sep 2, 2008.
--
-- References
--
--
module Text.PrintScanF
class FormattingSpec repr
lit :: (FormattingSpec repr) => String -> repr a a
int :: (FormattingSpec repr) => repr a (Int -> a)
char :: (FormattingSpec repr) => repr a (Char -> a)
fpp :: (FormattingSpec repr) => PrinterParser b -> repr a (b -> a)
(^) :: (FormattingSpec repr) => repr b c -> repr a b -> repr a c
data PrinterParser a
PrinterParser :: (a -> String) -> (String -> Maybe (a, String)) -> PrinterParser a
fmt :: (FormattingSpec repr, Show b, Read b) => b -> repr a (b -> a)
newtype FPr a b
FPr :: ((String -> a) -> b) -> FPr a b
newtype FSc a b
FSc :: (String -> b -> Maybe (a, String)) -> FSc a b
sprintf :: FPr String b -> b
sscanf :: String -> FSc a b -> b -> Maybe a
showread :: (Show a, Read a) => PrinterParser a
prefix :: String -> String -> Maybe String
instance FormattingSpec FSc
instance FormattingSpec FPr
-- | http://okmij.org/ftp/typed-formatting/FPrintScan.html#C-like
--
-- Safe and generic printf/scanf with C-like format string
--
-- We implement printf that takes a C-like format string and the variable
-- number of other arguments. Unlike C of Haskell's printf, ours is
-- total: if the types or the number of the other arguments, the values
-- to format, does not match the format string, a type error is reported
-- at compile time. To the familiar format descriptors %s and %d we add
-- %a to format any showable value. The latter is like the format
-- descriptor ~a of Common Lisp. Likewise, we build scanf that takes a
-- C-like format string and the consumer function with the variable
-- number of arguments. The types and the number of the arguments must
-- match the format string; a type error is reported otherwise.
--
-- Our approach is a variation of the safe printf and scanf described
-- elsewhere on this page. We use Template Haskell to translate the
-- format string to a phrase in the DSL of format descriptors. We use the
-- final approach to embed that DSL into Haskell.
--
-- Unlike the safe printf explained in the Template Haskell
-- documentation, in our implementation, format descriptors are first
-- class. They can be built incrementally. The same descriptor can be
-- used both for printing and for parsing. Our printf and scanf are
-- user-extensible: library users can write functions to direct format
-- output to any suitable data sink, or to read parsed data from any
-- suitable data source such as string or a file. Finally, what is
-- formatted can be parsed back using the same format descriptor.
--
-- Here are some of the tests from the test collection referenced below.
-- The evaluation result is given in the comments below each binding.
-- Example t31 shows that format descriptors are indeed first-class. The
-- definition t32, when uncommented, raises the shown type error because
-- the format descriptor does not match the type of the corresponding
-- argument.
module Text.TotalPrintF
spec :: String -> ExpQ
sprintf :: FPr String b -> b
sscanf :: String -> FSc a b -> b -> Maybe a
(^) :: (FormattingSpec repr) => repr b c -> repr a b -> repr a c
instance Eq FDesc
instance Show FDesc
-- | Type-safe printf and scanf with C-like formatting string We also
-- permit a generic format specifier %a to format or parse any showable
-- and readable value. Our format descriptors are first-class and can be
-- built incrementally. We can use the same format descriptor to format
-- to a string, to the standard output or any other data sink.
-- Furthermore, we can use the same format descriptor to parse from a
-- string or any data source. What we print we can parse, using the same
-- descriptor.
module Text.TFTest
newtype FPrIO a b
FPrIO :: ((IO () -> a) -> b) -> FPrIO a b
instance FormattingSpec FPrIO
-- | http://okmij.org/ftp/typed-formatting/FPrintScan.html
--
-- The initial view to the typed sprintf and sscanf This code defines a
-- simple domain-specific language of string patterns and demonstrates
-- two interpreters of the language: for building strings (sprintf) and
-- parsing strings (sscanf). This code thus solves the problem of typed
-- printf/scanf sharing the same format string posed by Chung-chieh Shan.
--
-- Version: The current version is 1.1, Aug 31, 2008.
--
-- References
--
--
module Text.PrintScan
data F a b
FLit :: String -> F a a
FInt :: F a (Int -> a)
FChr :: F a (Char -> a)
FPP :: PrinterParser b -> F a (b -> a)
(:^) :: F b c -> F a b -> F a c
-- | Printerparsers (injectionprojection pairs)
data PrinterParser a
PrinterParser :: (a -> String) -> (String -> Maybe (a, String)) -> PrinterParser a
-- | a bit of syntactic sugar to avoid hitting the Shift key too many a
-- time
fmt :: (Show b, Read b) => b -> F a (b -> a)
-- | The interpreter for printf It implements Asai's accumulator-less
-- alternative to Danvy's functional unparsing
intp :: F a b -> (String -> a) -> b
-- | The interpreter for scanf
ints :: F a b -> String -> b -> Maybe (a, String)
sprintf :: F String b -> b
sscanf :: String -> F a b -> b -> Maybe a
-- | The format specification is first-class. One can build format
-- specification incrementally This is not the case with OCaml's
-- printf/scanf (where the format specification has a weird typing and is
-- not first class).
--
-- Primitive Printer/parsers
showread :: (Show a, Read a) => PrinterParser a
-- | A better prefixOf function prefix patt str --> Just str' if the
-- String patt is the prefix of String str. The result str' is str with
-- patt removed Otherwise, the result is Nothing
prefix :: String -> String -> Maybe String
-- | Simply-typed Curry-style (nominal) lambda-calculus with integers and
-- zero-comparison Type inference. Hiding the single-threaded state via
-- simple algebraic transformations (beta-expansions).
--
-- http://okmij.org/ftp/Computation/Computation.html#teval
module Language.TEval.TInfTM
data Typ
TInt :: Typ
(:>) :: !Typ -> !Typ -> Typ
TV :: TVarName -> Typ
type TVarName = Int
data Term
V :: VarName -> Term
L :: VarName -> Term -> Term
A :: Term -> Term -> Term
I :: Int -> Term
(:+) :: Term -> Term -> Term
IFZ :: Term -> Term -> Term -> Term
Fix :: Term -> Term
type VarName = String
-- | Type Environment: associating types with free term variables
type TEnv = [(VarName, Typ)]
env0 :: TEnv
lkup :: TEnv -> VarName -> Typ
ext :: TEnv -> (VarName, Typ) -> TEnv
-- | Type Variable Environment: associating types with free type
-- variables
data TVE
TVE :: Int -> (IntMap Typ) -> TVE
-- | Allocate a fresh type variable (see the first component of TVE)
newtv :: TVE -> (Typ, TVE)
tve0 :: TVE
tvlkup :: TVE -> TVarName -> Maybe Typ
tvext :: TVE -> (TVarName, Typ) -> TVE
-- | Type variables are logic variables: hypothetical reasoning
tvsub :: TVE -> Typ -> Typ
-- | shallow substitution; check if tv is bound to anything
-- substantial
tvchase :: TVE -> Typ -> Typ
-- | The unification. If unification failed, return the reason
unify :: Typ -> Typ -> TVE -> Either String TVE
-- | If either t1 or t2 are type variables, they are definitely unbound
unify' :: Typ -> Typ -> TVE -> Either String TVE
-- | Unify a free variable v1 with t2
unifyv :: TVarName -> Typ -> TVE -> Either String TVE
-- | The occurs check: if v appears free in t
occurs :: TVarName -> Typ -> TVE -> Bool
-- | Introducing the combinators to hide single-threaded state tve in one
-- case of teval' (the A case). The other cases stay as they are, to
-- illustrate that our transformation is fully compatible with the
-- earlier code.
type TVEM a = TVE -> (a, TVE)
(>>=) :: TVEM a -> (a -> TVEM b) -> TVEM b
return :: a -> TVEM a
-- | The expression abstracted from the last-but-one re-writing of the
-- A-clause below
--
-- Type reconstruction: abstract evaluation
teval' :: TEnv -> Term -> (TVE -> (Typ, TVE))
teval :: TEnv -> Term -> Typ
instance Show TVE
instance Show Term
instance Eq Term
instance Show Typ
instance Eq Typ
-- | Simply-typed Curry-style (nominal) lambda-calculus with integers and
-- zero-comparison Type inference, of the type and of the environment,
-- aka conditional typechecking This code does not in general infer
-- polymorphic bindings as this is akin to higher-order unification.
--
-- The benefit of the approach: we can handle _open_ terms. Some of them
-- we type check, and some of them we reject. The rejection means the
-- term cannot be typed in _any_ type environment.
--
-- One often hears a complaint against typing: one can evaluate terms we
-- can't even type check. This code shows that we can type check terms we
-- can't even evaluate.
--
-- We cannot evaluate open terms at all, but we can type check them,
-- inferring both the type as well as the _requirement_ on the
-- environments in which the term must be used.
--
-- http://okmij.org/ftp/Computation/Computation.html#teval
module Language.TEval.TInfTEnv
data Typ
TInt :: Typ
(:>) :: !Typ -> !Typ -> Typ
TV :: TVarName -> Typ
type TVarName = Int
data Term
V :: VarName -> Term
L :: VarName -> Term -> Term
A :: Term -> Term -> Term
I :: Int -> Term
(:+) :: Term -> Term -> Term
IFZ :: Term -> Term -> Term -> Term
Fix :: Term -> Term
type VarName = String
-- | Type Environment: associating types with free term variables
type TEnv = [(VarName, Typ)]
env0 :: TEnv
lkup :: TEnv -> VarName -> Typ
ext :: TEnv -> (VarName, Typ) -> TEnv
unext :: TEnv -> VarName -> TEnv
env_map :: (Typ -> Typ) -> TEnv -> TEnv
-- | Merge two environment, using the given function to resolve the
-- conflicts, if any
env_fold_merge :: TEnv -> TEnv -> (Typ -> Typ -> seed -> Either err seed) -> seed -> Either err (TEnv, seed)
-- | Type Variable Environment: associating types with free type
-- variables
data TVE
TVE :: Int -> (IntMap Typ) -> TVE
-- | Allocate a fresh type variable (see the first component of TVE)
newtv :: TVE -> (Typ, TVE)
tve0 :: TVE
tvlkup :: TVE -> TVarName -> Maybe Typ
tvext :: TVE -> (TVarName, Typ) -> TVE
-- | Type variables are logic variables: hypothetical reasoning
tvsub :: TVE -> Typ -> Typ
-- | shallow substitution; check if tv is bound to anything
-- substantial
tvchase :: TVE -> Typ -> Typ
-- | The unification. If unification failed, return the reason
unify :: Typ -> Typ -> TVE -> Either String TVE
-- | If either t1 or t2 are type variables, they are definitely unbound
unify' :: Typ -> Typ -> TVE -> Either String TVE
-- | Unify a free variable v1 with t2
unifyv :: TVarName -> Typ -> TVE -> Either String TVE
-- | The occurs check: if v appears free in t
occurs :: TVarName -> Typ -> TVE -> Bool
merge_env :: TEnv -> TEnv -> (TVE -> (TEnv, TVE))
-- | Type reconstruction: abstract evaluation
teval' :: Term -> (TVE -> (Typ, TEnv, TVE))
-- | Resolve all type variables, as far as possible
teval :: Term -> (Typ, TEnv)
instance Show TVE
instance Show Term
instance Eq Term
instance Show Typ
instance Eq Typ
-- | Simply-typed Curry-style (nominal) lambda-calculus with integers and
-- zero-comparison Type inference
--
-- http://okmij.org/ftp/Computation/Computation.html#teval
module Language.TEval.TInfT
data Typ
TInt :: Typ
(:>) :: !Typ -> !Typ -> Typ
TV :: TVarName -> Typ
type TVarName = Int
data Term
V :: VarName -> Term
L :: VarName -> Term -> Term
A :: Term -> Term -> Term
I :: Int -> Term
(:+) :: Term -> Term -> Term
IFZ :: Term -> Term -> Term -> Term
Fix :: Term -> Term
type VarName = String
-- | Type Environment: associating types with free term variables
type TEnv = [(VarName, Typ)]
env0 :: TEnv
lkup :: TEnv -> VarName -> Typ
ext :: TEnv -> (VarName, Typ) -> TEnv
data TVE
TVE :: Int -> (IntMap Typ) -> TVE
newtv :: TVE -> (Typ, TVE)
tve0 :: TVE
tvlkup :: TVE -> TVarName -> Maybe Typ
tvext :: TVE -> (TVarName, Typ) -> TVE
-- | Type variables are logic variables: hypothetical reasoning
tvsub :: TVE -> Typ -> Typ
-- | shallow substitution; check if tv is bound to anything
-- substantial
tvchase :: TVE -> Typ -> Typ
-- | The unification. If unification failed, return the reason
unify :: Typ -> Typ -> TVE -> Either String TVE
-- | If either t1 or t2 are type variables, they are definitely unbound
unify' :: Typ -> Typ -> TVE -> Either String TVE
-- | Unify a free variable v1 with t2
unifyv :: TVarName -> Typ -> TVE -> Either String TVE
-- | The occurs check: if v appears free in t
occurs :: TVarName -> Typ -> TVE -> Bool
-- | Type reconstruction: abstract evaluation
teval' :: TEnv -> Term -> (TVE -> (Typ, TVE))
-- | Resolve all type variables, as far as possible
teval :: TEnv -> Term -> Typ
instance Show TVE
instance Show Term
instance Eq Term
instance Show Typ
instance Eq Typ
-- | Simply-typed Curry-style (nominal) lambda-calculus with integers and
-- zero-comparison Let-polymorphism via type schemes Type inference
--
-- http://okmij.org/ftp/Computation/Computation.html#teval
module Language.TEval.TInfLetP
data Typ
TInt :: Typ
(:>) :: !Typ -> !Typ -> Typ
TV :: TVarName -> Typ
type TVarName = Int
data TypS
TypS :: [TVarName] -> Typ -> TypS
data Term
V :: VarName -> Term
L :: VarName -> Term -> Term
A :: Term -> Term -> Term
I :: Int -> Term
(:+) :: Term -> Term -> Term
IFZ :: Term -> Term -> Term -> Term
Fix :: Term -> Term
Let :: (VarName, Term) -> Term -> Term
type VarName = String
-- | Type Environment: associating *would-be* types with free term
-- variables
type TEnv = [(VarName, TypS)]
env0 :: TEnv
lkup :: TEnv -> VarName -> TypS
ext :: TEnv -> (VarName, TypS) -> TEnv
-- | Type Variable Environment: associating types with free type
-- variables
data TVE
TVE :: Int -> (IntMap Typ) -> TVE
-- | TVE is the state of a monadic computation
type TVEM = State TVE
-- | Allocate a fresh type variable (see the first component of TVE)
newtv :: TVEM Typ
tve0 :: TVE
tvlkup :: TVE -> TVarName -> Maybe Typ
tvext :: TVE -> (TVarName, Typ) -> TVE
-- | TVE domain predicate: check to see if a TVarName is in the domain of
-- TVE
tvdomainp :: TVE -> TVarName -> Bool
-- | Give the list of all type variables that are allocated in TVE but not
-- bound there
tvfree :: TVE -> [TVarName]
-- | Type variables are logic variables: hypothetical reasoning
tvsub :: TVE -> Typ -> Typ
-- | shallow substitution; check if tv is bound to anything
-- substantial
tvchase :: TVE -> Typ -> Typ
-- | The unification. If unification failed, return the reason
unify :: Typ -> Typ -> TVE -> Either String TVE
-- | If either t1 or t2 are type variables, they are definitely unbound
unify' :: Typ -> Typ -> TVE -> Either String TVE
-- | Unify a free variable v1 with t2
unifyv :: TVarName -> Typ -> TVE -> Either String TVE
-- | The occurs check: if v appears free in t
occurs :: TVarName -> Typ -> TVE -> Bool
-- | Compute (quite unoptimally) the characteristic function of the set
-- forall tvb in fv(tve_before). Union fv(tvsub(tve_after,tvb))
tvdependentset :: TVE -> TVE -> (TVarName -> Bool)
-- | Monadic version of unify
unifyM :: Typ -> Typ -> (String -> String) -> TVEM ()
-- | Given a type scheme, that is, the type t and the list of type
-- variables tvs, for every tvs, replace all of its occurrences in t with
-- a fresh type variable. We do that by creating a substitution tve and
-- applying it to t.
instantiate :: TypS -> TVEM Typ
-- | Given a typechecking action ta yielding the type t, return the type
-- scheme quantifying over _truly free_ type variables in t with respect
-- to TVE that existed before the typechecking action began. Let
-- tve_before is TVE before the type checking action is executed, and
-- tve_after is TVE after the action. A type variable tv is truly free if
-- it is free in tve_after and remains free if the typechecking action
-- were executed in any tve extending tve_before with arbitrary binding
-- to type variables free in tve_before. To be more precise, a type
-- variable tv is truly free with respect to tve_before if: tv notin
-- domain(tve_after) forall tvb in fv(tve_before). tv notin
-- fv(tvsub(tve_after,tvb)) In other words, tv is truly free if it is
-- free and independent of tve_before.
--
-- Our goal is to reproduce the behavior in TInfLetI.hs:
-- generalize/instantiate should mimic multiple executions of the
-- typechecking action. That means we should quantify over all type
-- variables created by ta that are independent of the type environment
-- in which the action may be executed.
generalize :: TVEM Typ -> TVEM TypS
-- | Return the list of type variables in t (possibly with duplicates)
freevars :: Typ -> [TVarName]
-- | Type reconstruction: abstract evaluation
teval' :: TEnv -> Term -> TVEM Typ
-- | Resolve all type variables, as far as possible, and generalize We
-- assume teval will be used for top-level expressions where
-- generalization is appropriate.
teval :: TEnv -> Term -> TypS
-- | non-generalizing teval (as before)
tevalng :: TEnv -> Term -> Typ
instance Show TVE
instance Show Term
instance Eq Term
instance Show TypS
instance Show Typ
instance Eq Typ
-- | Simply-typed Curry-style (nominal) lambda-calculus with integers and
-- zero-comparison Let-polymorphism via inlining Type inference
--
-- http://okmij.org/ftp/Computation/Computation.html#teval
module Language.TEval.TInfLetI
data Typ
TInt :: Typ
(:>) :: !Typ -> !Typ -> Typ
TV :: TVarName -> Typ
type TVarName = Int
data Term
V :: VarName -> Term
L :: VarName -> Term -> Term
A :: Term -> Term -> Term
I :: Int -> Term
(:+) :: Term -> Term -> Term
IFZ :: Term -> Term -> Term -> Term
Fix :: Term -> Term
Let :: (VarName, Term) -> Term -> Term
type VarName = String
-- | Type Environment: associating *would-be* types with free term
-- variables
type TEnv = [(VarName, TVEM Typ)]
env0 :: TEnv
lkup :: TEnv -> VarName -> TVEM Typ
ext :: TEnv -> (VarName, TVEM Typ) -> TEnv
-- | Type Variable Environment: associating types with free type
-- variables
data TVE
TVE :: Int -> (IntMap Typ) -> TVE
-- | TVE is the state of a monadic computation
type TVEM = State TVE
-- | Allocate a fresh type variable (see the first component of TVE)
newtv :: TVEM Typ
tve0 :: TVE
tvlkup :: TVE -> TVarName -> Maybe Typ
tvext :: TVE -> (TVarName, Typ) -> TVE
-- | Type variables are logic variables: hypothetical reasoning
tvsub :: TVE -> Typ -> Typ
-- | shallow substitution; check if tv is bound to anything
-- substantial
tvchase :: TVE -> Typ -> Typ
-- | The unification. If unification failed, return the reason
unify :: Typ -> Typ -> TVE -> Either String TVE
-- | If either t1 or t2 are type variables, they are definitely unbound
unify' :: Typ -> Typ -> TVE -> Either String TVE
-- | Unify a free variable v1 with t2
unifyv :: TVarName -> Typ -> TVE -> Either String TVE
-- | The occurs check: if v appears free in t
occurs :: TVarName -> Typ -> TVE -> Bool
-- | Monadic version of unify
unifyM :: Typ -> Typ -> (String -> String) -> TVEM ()
-- | Type reconstruction: abstract evaluation
teval' :: TEnv -> Term -> TVEM Typ
-- | Resolve all type variables, as far as possible
teval :: TEnv -> Term -> Typ
instance Show TVE
instance Show Term
instance Eq Term
instance Show Typ
instance Eq Typ
-- | Simply-typed Church-style (nominal) lambda-calculus with integers and
-- zero-comparison Type reconstruction, for all subterms
--
-- http://okmij.org/ftp/Computation/Computation.html#teval
module Language.TEval.TEvalNR
data Typ
TInt :: Typ
(:>) :: !Typ -> !Typ -> Typ
data Term
V :: VarName -> Term
L :: VarName -> Typ -> Term -> Term
A :: Term -> Term -> Term
I :: Int -> Term
(:+) :: Term -> Term -> Term
IFZ :: Term -> Term -> Term -> Term
Fix :: Term -> Term
type VarName = String
-- | Type Environment: associating types with free variables
type TEnv = [(VarName, Typ)]
env0 :: TEnv
lkup :: TEnv -> VarName -> Typ
ext :: TEnv -> (VarName, Typ) -> TEnv
-- | A virtual typed AST: associating a type to each subterm
type TermIndex = [Int]
type Typs = Map TermIndex Typ
topterm :: Typ -> Typs
toptyp :: Typs -> Typ
shift :: Int -> Typs -> Typs
-- | Type reconstruction: abstract evaluation
teval :: TEnv -> Term -> Typs
instance Show Term
instance Eq Term
instance Show Typ
instance Eq Typ
-- | Simply-typed Church-style (nominal) lambda-calculus with integers and
-- zero-comparison Type checking
--
-- http://okmij.org/ftp/Computation/Computation.html#teval
module Language.TEval.TEvalNC
data Typ
TInt :: Typ
(:>) :: !Typ -> !Typ -> Typ
data Term
V :: VarName -> Term
L :: VarName -> Typ -> Term -> Term
A :: Term -> Term -> Term
I :: Int -> Term
(:+) :: Term -> Term -> Term
IFZ :: Term -> Term -> Term -> Term
Fix :: Term -> Term
type VarName = String
-- | Type Environment: associating types with free variables
type TEnv = [(VarName, Typ)]
env0 :: TEnv
lkup :: TEnv -> VarName -> Typ
ext :: TEnv -> (VarName, Typ) -> TEnv
-- | Type reconstruction: abstract evaluation
teval :: TEnv -> Term -> Typ
instance Show Term
instance Eq Term
instance Show Typ
instance Eq Typ
-- | Tagless Typed lambda-calculus with integers and the conditional in the
-- higher-order abstract syntax. Haskell itself ensures the object terms
-- are well-typed. Here we use GADT: This file is not in Haskell98
--
-- http://okmij.org/ftp/Computation/Computation.html#teval
module Language.TEval.EvalTaglessI
data Term t
V :: t -> Term t
L :: (Term t1 -> Term t2) -> Term (t1 -> t2)
A :: Term (t1 -> t2) -> Term t1 -> Term t2
I :: Int -> Term Int
(:+) :: Term Int -> Term Int -> Term Int
IFZ :: Term Int -> Term t -> Term t -> Term t
Fix :: Term ((a -> b) -> (a -> b)) -> Term (a -> b)
-- | We no longer need variables or the environment and we do normalization
-- by evaluation.
--
-- Denotational semantics. Why?
evald :: Term t -> t
-- | Operational semantics. Why? GADT are still implemented imperfectly: we
-- the default case in case statements (with cannot happen error), to
-- avoid the warning about inexhaustive pattern match -- although these
-- case-brances can never be executed. Why?
evalo :: Term t -> Term t
instance Show (Term t)
-- | Tagless Typed lambda-calculus with integers and the conditional in the
-- higher-order abstract syntax. Haskell itself ensures the object terms
-- are well-typed. Here we use the tagless final approach.
--
-- http://okmij.org/ftp/Computation/Computation.html#teval
module Language.TEval.EvalTaglessF
class Symantics repr
l :: (Symantics repr) => (repr t1 -> repr t2) -> repr (t1 -> t2)
a :: (Symantics repr) => repr (t1 -> t2) -> repr t1 -> repr t2
i :: (Symantics repr) => Int -> repr Int
(+:) :: (Symantics repr) => repr Int -> repr Int -> repr Int
ifz :: (Symantics repr) => repr Int -> repr t -> repr t -> repr t
fix :: (Symantics repr) => repr ((a -> b) -> (a -> b)) -> repr (a -> b)
-- | Since we rely on the metalanguage for typechecking and hence type
-- generalization, we have to use `let' of the metalanguage.
--
-- It is quite challenging to show terms. Yet, in contrast to the
-- GADT-based approach (EvalTaglessI.hs), we are able to do that, without
-- extending our language with auxiliary syntactic forms. Incidentally,
-- showing of terms is just another way of _evaluating_ them, to strings.
type VarCount = Int
newtype S t
S :: (VarCount -> (String, VarCount)) -> S t
-- | We no longer need variables or the environment and we do normalization
-- by evaluation.
--
-- Denotational semantics. Why?
newtype D t
D :: t -> D t
evald :: D t -> t
instance Symantics D
instance Symantics S
-- | Untyped (nominal) lambda-calculus with integers and the conditional
--
-- http://okmij.org/ftp/Computation/Computation.html#teval
--
--
-- - The Abstract of the lecture notes We expound a view of type
-- checking as evaluation with `abstract values'. Whereas dynamic
-- semantics, evaluation, deals with (dynamic) values like 0, 1, etc.,
-- static semantics, type checking, deals with approximations like int. A
-- type system is sound if it correctly approximates the dynamic behavior
-- and predicts its outcome: if the static semantics predicts that a term
-- has the type int, the dynamic evaluation of the term, if it
-- terminates, will yield an integer.
--
--
-- As object language, we use simply-typed and let-polymorphic lambda
-- calculi with integers and integer operations as constants. We use
-- Haskell as a metalanguage in which to write evaluators, type checkers,
-- type reconstructors and inferencers for the object language.
--
-- We explore the deep relation between parametric polymorphism and
-- inlining. Polymorphic type checking then is an optimization
-- allowing us to type check a polymorphic term at the place of its
-- definition rather than at the places of its use.
--
-- Joint work with Chung-chieh Shan.
--
-- Version The current version is 1.1, July 2008. References lecture.pdf
-- [199K]
module Language.TEval.EvalN
data Term
V :: VarName -> Term
L :: VarName -> Term -> Term
A :: Term -> Term -> Term
I :: Int -> Term
(:+) :: Term -> Term -> Term
IFZ :: Term -> Term -> Term -> Term
type VarName = String
-- | Environment: associating values with free variables
type Env = [(VarName, Value)]
env0 :: Env
lkup :: Env -> VarName -> Value
ext :: Env -> (VarName, Value) -> Env
data Value
VI :: Int -> Value
VC :: (Value -> Value) -> Value
-- | Denotational semantics. Why? How to make it operational?
eval :: Env -> Term -> Value
instance Show Term
instance Eq Term
instance Show Value
-- |
-- http://okmij.org/ftp/Computation/lambda-calc.html#haskell-type-level
--
-- This is the first message in a series on arbitrary type/kind-level
-- computations in the present-day Haskell, and on using of so computed
-- types to give signatures to terms and to drive the selection of
-- overloaded functions. We can define the type TD N to be the type of a
-- tree fib(N)-level deep, and instantiate the read function for the tree
-- of that type. The type computations are largely expressed in a
-- functional language not too unlike Haskell itself.
--
-- In this message we implement call-by-value lambda-calculus with
-- booleans, naturals and case-discrimination. The distinct feature of
-- our implementation, besides its simplicity, is the primary role of
-- type application rather than that of abstraction. Yet we trivially
-- represent closures and higher-order functions. We use proper names for
-- function arguments (rather than deBruijn indices), and yet we avoid
-- the need for fresh name generation, name comparison, and
-- alpha-conversion. We have no explicit environment and no need to
-- propagate and search it, and yet we can partially apply functions.
--
-- Our implementation fundamentally relies on the connection between
-- polymorphism and abstraction, and takes the full advantage of the
-- type-lambda implicitly present in Haskell. The reason for the
-- triviality of our code is the typechecker's already doing most of the
-- work need for an implementation of lambda-calculus.
--
-- Our code is indeed quite simple: its general part has only three
-- lines:
--
--
-- instance E (F x) (F x)
-- instance (E y y', A (F x) y' r) => E ((F x) :< y) r
-- instance (E (x :< y) r', E (r' :< z) r) => E ((x :< y) :< z) r
--
--
-- The first line says that abstractions evaluate to themselves, the
-- second line executes the redex, and the third recurses to find it.
-- Still, we may (and did) write partial applications, the fixpoint
-- combinator, Fibonacci function, and S and K combinators. Incidentally,
-- the realization of the S combinator again takes three lines, two of
-- which build the closures (partial applications) and the third line
-- executes the familiar S-rule.
--
--
-- instance A (F CombS) f (F (CombS,f))
-- instance A (F (CombS,f)) g (F (CombS,f,g))
-- instance E (f :< x :< (g :< x)) r => A (F (CombS,f,g)) x r
--
--
-- Incidentally, the present code constitutes what seems to be the
-- shortest proof that the type system of Haskell with the undecidable
-- instances extension is indeed Turing-complete. That extension is
-- needed for the fixpoint combinator -- which is present in the system
-- described in Luca Cardelli's 1988 manuscript:
--
-- http://lucacardelli.name/Papers/PhaseDistinctions.pdf
--
-- As he wrote, ``Here we have generalized the language of constant
-- expressions to include typed lambda abstraction, application and
-- recursion (because of the latter we do not require compile-time
-- computations to terminate).'' [p9]
--
-- This message is all the code, which runs in GHC 6.4.1 - 6.8.2 (it
-- could well run in Hugs; alas, Hugs did not like infix type
-- constructors like :<).
module Language.TypeLC
-- | First we define some constants
data HTrue
HTrue :: HTrue
data HFalse
HFalse :: HFalse
data Zero
Zero :: Zero
data Su a
Su :: a -> Su a
-- | Indicator for functions, or applicable things:
data F x
class A l a b | l a -> b
-- | The meaning of |A l a b| is that the application to |a| of an
-- applicable thing denoted by |l| yields |b|.
--
-- Surprisingly, this already works. Let us define the boolean Not
-- function
data FNot
-- | The next function is the boolean And. It takes two arguments, so we
-- have to handle currying now.
data FAnd
-- | Commonly, abstraction is held to be `more fundamental', which is
-- reflected in the popular phrase `Lambda-the-Ultimate'. In our system,
-- application is fundamental. An abstraction is a not-yet-applied
-- application -- which is in itself a first-class value. The class A
-- defines the meaning of a function, and an instance of A becomes the
-- definition of a function (clause).
--
-- We have dealt with simple expressions and applicative things. We now
-- build sequences of applications, and define the corresponding big step
-- semantics. We introduce the syntax for applications:
data (:<) f x
-- | and the big-step evaluation function:
class E a b | a -> b
-- | That is all. The rest of the message are the tests. The first one is
-- the type-level equivalent of the following function:
--
--
-- testb x = and (not x) (not (not x))
--
--
-- At the type level, it looks not much differently:
type Testb x = (E ((F FAnd :< (F FNot :< x)) :< (F FNot :< (F FNot :< x))) r) => r
-- | We introduce the applicative fixpoint combinator
data Rec l
-- | and define the sum of two numerals
--
-- At the type level, this looks as follows
data FSum'
-- | now we tie up the knot
type FSum = Rec (F FSum')
type N0 = Zero
type N1 = Su N0
type N2 = Su N1
type N3 = Su N2
test_sum :: (E ((F FSum :< x) :< y) r) => x -> y -> r
-- | Finally, the standard test -- Fibonacci
data Fib'
type Fib = Rec (F Fib')
test_fib :: (E (F Fib :< n) r) => n -> r
-- | Finally, we demonstrate that our calculus is combinatorially complete,
-- by writing the S and K combinators
data CombK
data CombS
-- | A few examples: SKK as the identity
type Test_skk x = (E (((F CombS :< F CombK) :< F CombK) :< x) r) => r
-- | and the representation of numerals in the SK calculus. The expression
-- (F FSum :< Su Zero) is a partial application of the function sum to
-- 1.
type CombZ = F CombS :< F CombK
type CombSu = F CombS :< ((F CombS :< (F CombK :< F CombS)) :< F CombK)
type CombTwo = CombSu :< (CombSu :< CombZ)
test_ctwo :: (E ((CombTwo :< (F FSum :< Su Zero)) :< Zero) r) => r
class Nat a
fromNat :: (Nat a) => a -> Integer
instance (Nat x) => Show (Su x)
instance Show Zero
instance (Nat x) => Nat (Su x)
instance Nat Zero
instance Show HFalse
instance Show HTrue
instance (E ((f :< x) :< (g :< x)) r) => A (F (CombS, f, g)) x r
instance A (F (CombS, f)) g (F (CombS, f, g))
instance A (F CombS) f (F (CombS, f))
instance A (F (CombK, a)) b a
instance A (F CombK) a (F (CombK, a))
instance (E ((F FSum :< (self :< n)) :< (self :< Su n)) r) => A (F (Fib', self)) (Su (Su n)) r
instance A (F (Fib', self)) (Su Zero) (Su Zero)
instance A (F (Fib', self)) Zero (Su Zero)
instance A (F Fib') self (F (Fib', self))
instance (E ((self :< n) :< m) r) => A (F (FSum', self, Su n)) m (Su r)
instance A (F (FSum', self, Zero)) m m
instance A (F (FSum', self)) n (F (FSum', self, n))
instance A (F FSum') self (F (FSum', self))
instance (E ((l :< F (Rec l)) :< x) r) => A (F (Rec l)) x r
instance (E x x') => E (Su x) (Su x')
instance (E (x :< y) r', E (r' :< z) r) => E ((x :< y) :< z) r
instance (E y y', A (F x) y' r) => E (F x :< y) r
instance E (F x) (F x)
instance E Zero Zero
instance E HFalse HFalse
instance E HTrue HTrue
instance A (F (FAnd, HFalse)) a HFalse
instance A (F (FAnd, HTrue)) a a
instance A (F FAnd) x (F (FAnd, x))
instance A (F FNot) HFalse HTrue
instance A (F FNot) HTrue HFalse
-- | http://okmij.org/ftp/Haskell/types.html#computable-types
--
-- Part I of the series introduced the type-level functional language
-- with the notation that resembles lambda-calculus with case
-- distinction, fixpoint recursion, etc. Modulo a bit of syntactic tart,
-- the language of the type functions even looks almost like the pure
-- Haskell. In this message, we show the applications of computable
-- types, to ascribe signatures to terms and to drive the selection of
-- overloaded functions. We can compute the type of a tree of the depth
-- fib(N) or a complex XML type, and instantiate the read function to
-- read the trees of only that shape.
--
-- A telling example of the power of the approach is the ability to use
-- not only (a->) but also (->a) as an unary type function. The
-- former is just (->) a. The latter is considered impossible. In our
-- approach, (->a) is written almost literally as (flip (->) a)
--
-- This series of messages has been inspired by Luca Cardelli's 1988
-- manuscript ``Phase Distinctions in Type Theory''
-- http://lucacardelli.name/Papers/PhaseDistinctions.pdf and by
-- Simon Peyton Jones and Erik Meijer's ``Henk: A Typed Intermediate
-- Language''
-- http://www.research.microsoft.com/~simonpj/Papers/henk.ps.gz
-- which expounds many of the same notions in an excellent tutorial style
-- and in modern terminology.
--
-- I'm very grateful to Chung-chieh Shan for pointing out these papers to
-- me and for thought-provoking discussions.
module Language.TypeFN
-- | Our first example comes from Cardelli's paper: defining the type
-- Prop(n), of n-ary propositions. That is,
--
--
-- Prop(2) should be the type Bool -> Bool -> Bool
-- Prop(3) is the type of functions Bool -> Bool -> Bool -> Bool
--
--
-- etc.
--
-- Cardelli's paper (p. 10) writes this type as
--
--
-- let Prop:: AllKK(N:: NatK) Type =
-- recK(F:: AllKK(N:: NatK) Type)
-- funKK(N:: NatK) caseK N of 0K => Bool; succK(M) => Bool -> F(M);
--
--
--
-- let and2: Prop(2K) =
-- fun(a: Bool) fun(b: Bool) a & b;
--
--
-- Here 0K and 2K are type-level numerals of the kind NatK; recK is the
-- type-level fix-point combinator. The computed type Prop(2) then gives
-- the type to the term and2.
--
-- In our system, this example looks as follows:
data Prop'
type Prop = Rec (F Prop')
type Prop2 = (E (F Prop :< N2) r) => r
-- | We can compute types by applying type functions, just as we can
-- compute values by applying regular functions. Indeed, let us define a
-- StrangeProp of the kind NAT -> Type. StrangeProp(n) is the type of
-- propositions of arity m, where m is fib(n). We compose together the
-- already defined type function Prop2 and the type function Fib in the
-- previous message.
data StrangeProp
oddand4t :: (E (F StrangeProp :< ((F FSum :< N2) :< N2)) r) => r
-- | We introduce the combinator Ntimes: |NTimes f x n| applies f to x n
-- times. This is a sort of fold over numerals.
data Ntimes
data ATC1 c
-- | We can then write the type of n-ary propositions Prop(N) in a
-- different way, as an N-times application of the type constructor
-- (Bool->) to Bool.
type PropN' n = (E (((F Ntimes :< (F (ATC1 ((->) Bool)))) :< Bool) :< n) r) => r
-- | To generalize,
data ATC2 c :: (* -> * -> *)
type SPropN' n = (E (((F Ntimes :< (F (ATC2 (->)) :< Bool)) :< Bool) :< (F Fib :< n)) r) => r
-- | The comparison of ATC1 with ATC2 shows two different ways of defining
-- abstractions: as (F x) terms (`lambda-terms' in our calculus) and as
-- polymorphic types (Haskell type abstractions). The two ways are
-- profoundly related. The more verbose type application notation, via
-- (:<), has its benefits. After we introduce another higher-order
-- function
data Flip
-- | we make a very little change
type SSPropN' n = (E (((F Ntimes :< ((F Flip :< (F (ATC2 (->)))) :< Bool)) :< Bool) :< (F Fib :< n)) r) => r
-- | and obtain quite a different result:
--
--
-- *TypeFN> :t test_sspn4
-- test_sspn4 :: ((((Bool -> Bool) -> Bool) -> Bool) -> Bool) -> Bool
--
--
-- In effect, we were able to use not only (a->) but also (->a) as
-- an unary type function. Moreover, we achieved the latter by almost
-- literally applying the flip function to the arrow type constructor
-- (->).
--
-- Using the type inspection tools (typecast), we can replace the family
-- of functions ATC1, ATC2 with one, kind-polymorphic, polyvariadic
-- function ATC. This approach will be explained in further messages.
--
-- We can use the computed types to drive overloaded functions such as
-- read and show. The specifically instantiated read functions, in
-- particular, will check that a (remotely) received serialized value
-- matches our expectation. Let's consider the type of trees of the depth
-- of at most N.
data Node v els
Node :: v -> [els] -> Node v els
type TreeDN v l n = (E (((F Ntimes :< (F (ATC1 (Node v)))) :< l) :< n) r) => r
instance (Read v, Read els) => Read (Node v els)
instance (Show v, Show els) => Show (Node v els)
instance E (Node v els) (Node v els)
instance (E ((f :< y) :< x) r) => A (F (Flip, f, x)) y r
instance A (F (Flip, f)) x (F (Flip, f, x))
instance A (F Flip) f (F (Flip, f))
instance A (F (ATC2 c)) x (F (ATC1 (c x)))
instance A (F (ATC1 c)) x (c x)
instance (E (((F Ntimes :< f) :< (f :< x)) :< n) r) => A (F (Ntimes, f, x)) (Su n) r
instance A (F (Ntimes, f, x)) Zero x
instance A (F (Ntimes, f)) x (F (Ntimes, f, x))
instance A (F Ntimes) f (F (Ntimes, f))
instance E (a, b) (a, b)
instance E (a -> b) (a -> b)
instance E String String
instance E Int Int
instance E Bool Bool
instance (E (F Prop :< (F Fib :< n)) r) => A (F StrangeProp) n r
instance (E (f :< m) r) => A (F (Prop', f)) (Su m) (Bool -> r)
instance A (F (Prop', f)) Zero Bool
instance A (F Prop') f (F (Prop', f))
-- | Monadic and General Iteratees: incremental input parsers, processors
-- and transformers
--
-- The running example, parts 1 and 2 Part 1 is reading the headers, the
-- sequence of lines terminated by an empty line. Each line is terminated
-- by CR, LF, or CRLF. We should return the headers in order. In the case
-- of error, we should return the headers read so far and the description
-- of the error. Part 2 is reading the headers and reading all the lines
-- from the HTTP-chunk-encoded content that follows the headers. Part 2
-- thus verifies layering of streams, and processing of one stream
-- embedded (chunk encoded) into another stream.
module System.IterateeM
-- | A stream is a (continuing) sequence of elements bundled in Chunks. The
-- first two variants indicate termination of the stream. Chunk [a] gives
-- the currently available part of the stream. The stream is not
-- terminated yet. The case (Chunk []) signifies a stream with no
-- currently available data but which is still continuing. A stream
-- processor should, informally speaking, ``suspend itself'' and wait for
-- more data to arrive. Later on, we can add another variant: IE_block
-- (Ptr CChar) CSize so we could parse right from the buffer.
data StreamG a
EOF :: StreamG a
Err :: String -> StreamG a
Chunk :: [a] -> StreamG a
-- | A particular instance of StreamG: the stream of characters. This
-- stream is used by many input parsers.
type Stream = StreamG Char
-- | Iteratee -- a generic stream processor, what is being folded over a
-- stream When Iteratee is in the done state, it contains the
-- computed result and the remaining part of the stream. In the
-- cont state, the iteratee has not finished the computation and
-- needs more input. We assume that all iteratees are good --
-- given bounded input, they do the bounded amount of computation and
-- take the bounded amount of resources. The monad m describes the sort
-- of computations done by the iteratee as it processes the stream. The
-- monad m could be the identity monad (for pure computations) or the IO
-- monad (to let the iteratee store the stream processing results as they
-- are computed). We also assume that given a terminated stream, an
-- iteratee moves to the done state, so the results computed so far could
-- be returned.
--
-- We could have used existentials instead, by doing the closure
-- conversion
data IterateeG el m a
IE_done :: a -> (StreamG el) -> IterateeG el m a
IE_cont :: (StreamG el -> IterateeGM el m a) -> IterateeG el m a
newtype IterateeGM el m a
IM :: m (IterateeG el m a) -> IterateeGM el m a
unIM :: IterateeGM el m a -> m (IterateeG el m a)
type Iteratee m a = IterateeG Char m a
type IterateeM m a = IterateeGM Char m a
-- | Useful combinators for implementing iteratees and enumerators
liftI :: (Monad m) => IterateeG el m a -> IterateeGM el m a
-- | Just like bind (at run-time, this is indeed exactly bind)
(>>==) :: (Monad m) => IterateeGM el m a -> (IterateeG el m a -> IterateeGM el' m b) -> IterateeGM el' m b
-- | Just like an application -- a call-by-value-like application
(==<<) :: (Monad m) => (IterateeG el m a -> IterateeGM el' m b) -> IterateeGM el m a -> IterateeGM el' m b
-- | The following is a variant of join in the IterateeGM el m
-- monad. When el' is the same as el, the type of joinI is indeed that of
-- true monadic join. However, joinI is subtly different: since generally
-- el' is different from el, it makes no sense to continue using the
-- internal, IterateeG el' m a: we no longer have elements of the type
-- el' to feed to that iteratee. We thus send EOF to the internal
-- Iteratee and propagate its result. This join function is useful when
-- dealing with `derived iteratees' for embedded/nested streams. In
-- particular, joinI is useful to process the result of stake,
-- map_stream, or conv_stream below.
joinI :: (Monad m) => IterateeGM el m (IterateeG el' m a) -> IterateeGM el m a
-- | Read a stream to the end and return all of its elements as a list
stream2list :: (Monad m) => IterateeGM el m [el]
-- | Check to see if the stream is in error
iter_report_err :: (Monad m) => IterateeGM el m (Maybe String)
-- | The analogue of List.break It takes an element predicate and returns a
-- pair: (str, Just c) -- the element c is the first element of
-- the stream satisfying the break predicate; The list str is the prefix
-- of the stream up to but including c (str,Nothing) -- The
-- stream is terminated with EOF or error before any element satisfying
-- the break predicate was found. str is the scanned part of the stream.
-- None of the element in str satisfy the break predicate.
sbreak :: (Monad m) => (el -> Bool) -> IterateeGM el m ([el], Maybe el)
-- | A particular optimized case of the above: skip all elements of the
-- stream satisfying the given predicate -- until the first element that
-- does not satisfy the predicate, or the end of the stream. This is the
-- analogue of List.dropWhile
sdropWhile :: (Monad m) => (el -> Bool) -> IterateeGM el m ()
-- | Attempt to read the next element of the stream Return (Just c) if
-- successful, return Nothing if the stream is terminated (by EOF or an
-- error)
snext :: (Monad m) => IterateeGM el m (Maybe el)
-- | Look ahead at the next element of the stream, without removing it from
-- the stream. Return (Just c) if successful, return Nothing if the
-- stream is terminated (by EOF or an error)
speek :: (Monad m) => IterateeGM el m (Maybe el)
-- | Skip the rest of the stream
skip_till_eof :: (Monad m) => IterateeGM el m ()
-- | Skip n elements of the stream, if there are that many This is the
-- analogue of List.drop
sdrop :: (Monad m) => Int -> IterateeGM el m ()
-- | Iteratee converters for stream embedding The converters show a
-- different way of composing two iteratees: vertical rather
-- than horizontal
--
-- The type of the converter from the stream with elements el_outer to
-- the stream with element el_inner. The result is the iteratee for the
-- outer stream that uses an `IterateeG el_inner m a' to process the
-- embedded, inner stream as it reads the outer stream.
type EnumeratorN el_outer el_inner m a = IterateeG el_inner m a -> IterateeGM el_outer m (IterateeG el_inner m a)
-- | Read n elements from a stream and apply the given iteratee to the
-- stream of the read elements. Unless the stream is terminated early, we
-- read exactly n elements (even if the iteratee has accepted fewer).
stake :: (Monad m) => Int -> EnumeratorN el el m a
-- | Map the stream: yet another iteratee transformer Given the stream of
-- elements of the type el and the function el->el', build a nested
-- stream of elements of the type el' and apply the given iteratee to it.
-- Note the contravariance
map_stream :: (Monad m) => (el -> el') -> EnumeratorN el el' m a
-- | Convert one stream into another, not necessarily in lockstep
-- The transformer map_stream maps one element of the outer stream to one
-- element of the nested stream. The transformer below is more general:
-- it may take several elements of the outer stream to produce one
-- element of the inner stream, or the other way around. The
-- transformation from one stream to the other is specified as IterateeGM
-- el m (Maybe [el']). The Maybe type reflects the possibility of
-- the conversion error.
conv_stream :: (Monad m) => IterateeGM el m (Maybe [el']) -> EnumeratorN el el' m a
-- | Combining the primitive iteratees to solve the running problem:
-- Reading headers and the content from an HTTP-like stream
type Line = String
-- | Read the line of text from the stream The line can be terminated by
-- CR, LF or CRLF. Return (Right Line) if successful. Return (Left Line)
-- if EOF or a stream error were encountered before the terminator is
-- seen. The returned line is the string read so far.
--
-- The code is the same as that of pure Iteratee, only the signature has
-- changed. Compare the code below with GHCBufferIO.line_lazy
line :: (Monad m) => IterateeM m (Either Line Line)
-- | Line iteratees: processors of a stream whose elements are made of
-- Lines
--
-- Collect all read lines and return them as a list see stream2list
--
-- Print lines as they are received. This is the first impure
-- iteratee with non-trivial actions during chunk processing
print_lines :: IterateeGM Line IO ()
-- | Convert the stream of characters to the stream of lines, and apply the
-- given iteratee to enumerate the latter. The stream of lines is
-- normally terminated by the empty line. When the stream of characters
-- is terminated, the stream of lines is also terminated, abnormally.
-- This is the first proper iteratee-enumerator: it is the iteratee of
-- the character stream and the enumerator of the line stream. More
-- generally, we could have used conv_stream to implement enum_lines.
enum_lines :: (Monad m) => EnumeratorN Char Line m a
-- | Convert the stream of characters to the stream of words, and apply the
-- given iteratee to enumerate the latter. Words are delimited by white
-- space. This is the analogue of List.words It is instructive to compare
-- the code below with the code of List.words, which is:
--
--
-- words :: String -> [String]
-- words s = case dropWhile isSpace s of
-- "" -> []
-- s' -> w : words s''
-- where (w, s'') =
-- break isSpace s'
--
--
-- One should keep in mind that enum_words is a more general, monadic
-- function. More generally, we could have used conv_stream to implement
-- enum_words.
enum_words :: (Monad m) => EnumeratorN Char String m a
-- | Enumerators Each enumerator takes an iteratee and returns an iteratee
-- an Enumerator is an iteratee transformer. The enumerator normally
-- stops when the stream is terminated or when the iteratee moves to the
-- done state, whichever comes first. When to stop is of course up to the
-- enumerator...
--
-- We have two choices of composition: compose iteratees or compose
-- enumerators. The latter is useful when one iteratee reads from the
-- concatenation of two data sources.
type EnumeratorGM el m a = IterateeG el m a -> IterateeGM el m a
type EnumeratorM m a = EnumeratorGM Char m a
-- | The most primitive enumerator: applies the iteratee to the terminated
-- stream. The result is the iteratee usually in the done state.
enum_eof :: (Monad m) => EnumeratorGM el m a
-- | Another primitive enumerator: report an error
enum_err :: (Monad m) => String -> EnumeratorGM el m a
-- | The composition of two enumerators: essentially the functional
-- composition It is convenient to flip the order of the arguments of the
-- composition though: in e1 >. e2, e1 is executed first
(>.) :: (Monad m) => EnumeratorGM el m a -> EnumeratorGM el m a -> EnumeratorGM el m a
-- | The pure 1-chunk enumerator It passes a given list of elements to the
-- iteratee in one chunk This enumerator does no IO and is useful for
-- testing of base parsing
enum_pure_1chunk :: (Monad m) => [el] -> EnumeratorGM el m a
-- | The pure n-chunk enumerator It passes a given lift of elements to the
-- iteratee in n chunks This enumerator does no IO and is useful for
-- testing of base parsing and handling of chunk boundaries
enum_pure_nchunk :: (Monad m) => [el] -> Int -> EnumeratorGM el m a
-- | The enumerator of a POSIX Fd Unlike fdRead (which allocates a new
-- buffer on each invocation), we use the same buffer all throughout
enum_fd :: Fd -> EnumeratorM IO a
enum_file :: FilePath -> EnumeratorM IO a
-- | HTTP chunk decoding Each chunk has the following format:
--
--
-- <chunk-size> CRLF <chunk-data> CRLF
--
--
-- where chunk-size is the hexadecimal number; chunk-data
-- is a sequence of chunk-size bytes. The last chunk (so-called
-- EOF chunk) has the format 0 CRLF CRLF (where 0 is an ASCII zero, a
-- character with the decimal code 48). For more detail, see Chunked
-- Transfer Coding, Sec 3.6.1 of the HTTP/1.1 standard:
-- http://www.w3.org/Protocols/rfc2616/rfc2616-sec3.html#sec3.6.1
--
-- The following enum_chunk_decoded has the signature of the enumerator
-- of the nested (encapsulated and chunk-encoded) stream. It receives an
-- iteratee for the embedded stream and returns the iteratee for the
-- base, embedding stream. Thus what is an enumerator and what is an
-- iteratee may be a matter of perspective.
--
-- We have a decision to make: Suppose an iteratee has finished (either
-- because it obtained all needed data or encountered an error that makes
-- further processing meaningless). While skipping the rest of the
-- stream/the trailer, we encountered a framing error (e.g., missing CRLF
-- after chunk data). What do we do? We chose to disregard the latter
-- problem. Rationale: when the iteratee has finished, we are in the
-- process of skipping up to the EOF (draining the source). Disregarding
-- the errors seems OK then. Also, the iteratee may have found an error
-- and decided to abort further processing. Flushing the remainder of the
-- input is reasonable then. One can make a different choice...
enum_chunk_decoded :: (Monad m) => Iteratee m a -> IterateeM m a
instance (Show a) => Show (StreamG a)
instance MonadTrans (IterateeGM el)
instance (Monad m) => Monad (IterateeGM el m)
-- | Random and Binary IO with IterateeM
--
-- http://okmij.org/ftp/Streams.html#random-bin-IO
--
-- Random and binary IO: Reading TIFF
--
-- Iteratees presuppose sequential processing. A general-purpose input
-- method must also support random IO: processing a seek-able input
-- stream from an arbitrary position, jumping back and forth through the
-- stream. We demonstrate random IO with iteratees, as well as reading
-- non-textual files and converting raw bytes into multi-byte quantities
-- such as integers, rationals, and TIFF dictionaries. Positioning of the
-- input stream is evocative of delimited continuations.
--
-- We use random and binary IO to write a general-purpose TIFF library.
-- The library emphasizes incremental processing, relying on iteratees
-- and enumerators for on-demand reading of tag values. The library
-- extensively uses nested streams, tacitly converting the stream of raw
-- bytes from the file into streams of integers, rationals and other
-- user-friendly items. The pixel matrix is presented as a contiguous
-- stream, regardless of its segmentation into strips and physical
-- arrangement.
--
-- We show a representative application of the library: reading a sample
-- TIFF file, printing selected values from the TIFF dictionary,
-- verifying the values of selected pixels and computing the histogram of
-- pixel values. The pixel verification procedure stops reading the pixel
-- matrix as soon as all specified pixel values are verified. The
-- histogram accumulation does read the entire matrix, but incrementally.
-- Neither pixel matrix processing procedure loads the whole matrix in
-- memory. In fact, we never read and retain more than the IO-buffer-full
-- of raw data.
--
-- Version: The current version is 1.1, December 2008.
module System.RandomIO
-- | The type of the IO monad supporting seek requests and endianness The
-- seek_request is not-quite a state, more like a `communication channel'
-- set by the iteratee and answered by the enumerator. Since the base
-- monad is IO, it seems simpler to implement both endianness and seek
-- requests as IORef cells. Their names are grouped in a structure
-- RBState, which is propagated as the `environment.'
newtype RBIO a
RBIO :: (RBState -> IO a) -> RBIO a
unRBIO :: RBIO a -> RBState -> IO a
-- | Generally, RBState is opaque and should not be exported.
data RBState
RBState :: IORef Bool -> IORef (Maybe FileOffset) -> RBState
msb_first :: RBState -> IORef Bool
seek_req :: RBState -> IORef (Maybe FileOffset)
-- | The programmer should use the following functions instead
--
-- To request seeking, the iteratee sets seek_req to (Just
-- desired_offset) When the enumerator answers the request, it sets
-- seek_req back to Nothing
rb_seek_set :: FileOffset -> RBIO ()
rb_seek_answered :: RBIO Bool
rb_msb_first :: RBIO Bool
rb_msb_first_set :: Bool -> RBIO ()
runRB :: RBState -> IterateeGM el RBIO a -> IO (IterateeG el RBIO a)
-- | A useful combinator. Perhaps a better idea would have been to define
-- Iteratee to have (Maybe a) in IE_done? In that case, we could make
-- IterateeGM to be the instance of MonadPlus
bindm :: (Monad m) => m (Maybe a) -> (a -> m (Maybe b)) -> m (Maybe b)
-- | We discard all available input first. We keep discarding the stream s
-- until we determine that our request has been answered: rb_seek_set
-- sets the state seek_req to (Just off). When the request is answered,
-- the state goes back to Nothing. The above features remind one of
-- delimited continuations.
sseek :: FileOffset -> IterateeGM el RBIO ()
-- | An iteratee that reports and propagates an error We disregard the
-- input first and then propagate error. It is reminiscent of
-- abort
iter_err :: (Monad m) => String -> IterateeGM el m ()
-- | Read n elements from a stream and apply the given iteratee to the
-- stream of the read elements. If the given iteratee accepted fewer
-- elements, we stop. This is the variation of stake with the
-- early termination of processing of the outer stream once the
-- processing of the inner stream finished early. This variation is
-- particularly useful for randomIO, where we do not have to care to
-- `drain the input stream'.
stakeR :: (Monad m) => Int -> EnumeratorN el el m a
-- | Iteratees to read unsigned integers written in Big- or Little-endian
-- ways
endian_read2 :: IterateeGM Word8 RBIO (Maybe Word16)
endian_read4 :: IterateeGM Word8 RBIO (Maybe Word32)
-- | The enumerator of a POSIX Fd: a variation of enum_fd that supports
-- RandomIO (seek requests)
enum_fd_random :: Fd -> EnumeratorGM Word8 RBIO a
instance MonadIO RBIO
instance Monad RBIO
-- | A general-purpose TIFF library
--
-- http://okmij.org/ftp/Streams.html#random-bin-IO
--
-- The library gives the user the TIFF dictionary, which the user can
-- search for specific tags and obtain the values associated with the
-- tags, including the pixel matrix.
--
-- The overarching theme is incremental processing: initially, only the
-- TIFF dictionary is read. The value associated with a tag is read only
-- when that tag is looked up (unless the value was short and was packed
-- in the TIFF dictionary entry). The pixel matrix (let alone the whole
-- TIFF file) is not loaded in memory -- the pixel matrix is not even
-- located before it is needed. The matrix is processed incrementally, by
-- a user-supplied iteratee.
--
-- The incremental processing is accomplished by iteratees and
-- enumerators. The enumerators are indeed first-class, they are stored
-- in the interned TIFF dictionary data structure. These enumerators
-- represent the values associated with tags; the values will be read on
-- demand, when the enumerator is applied to a user-given iteratee.
--
-- The library extensively uses nested streams, tacitly converting the
-- stream of raw bytes from the file into streams of integers, rationals
-- and other user-friendly items. The pixel matrix is presented as a
-- contiguous stream, regardless of its segmentation into strips and
-- physical arrangement. The library exhibits random IO and binary
-- parsing, reading of multi-byte numeric data in big- or little-endian
-- formats. The library can be easily adopted for AIFF, RIFF and other
-- IFF formats.
--
-- We show a representative application of the library: reading a sample
-- TIFF file, printing selected values from the TIFF dictionary,
-- verifying the values of selected pixels and computing the histogram of
-- pixel values. The pixel verification procedure stops reading the pixel
-- matrix as soon as all specified pixel values are verified. The
-- histogram accumulation does read the entire matrix, but incrementally.
-- Neither pixel matrix processing procedure loads the whole matrix in
-- memory. In fact, we never read and retain more than the IO-buffer-full
-- of raw data.
module Codec.Image.Tiff
-- | Sample TIFF user code The following is sample code using the TIFF
-- library (whose implementation is in the second part of this file). Our
-- sample code prints interesting information from the TIFF dictionary
-- (such as the dimensions, the resolution and the name of the image)
--
-- The sample file is a GNU logo (from http:www.gnu.org) converted
-- from JPG to TIFF. Copyleft by GNU.
--
-- The main user function. tiff_reader is the library function, which
-- builds the TIFF dictionary. process_tiff is the user function, to
-- extract useful data from the dictionary
--
-- Sample TIFF processing function
--
-- sample processing of the pixel matrix: computing the histogram
compute_hist :: TIFFDict -> IterateeGM Word8 RBIO (Int, IntMap Int)
-- | Another sample processor of the pixel matrix: verifying values of some
-- pixels This processor does not read the whole matrix; it stops as soon
-- as everything is verified or the error is detected
--
-- TIFF library code
--
-- We need a more general enumerator type: enumerator that maps streams
-- (not necessarily in lock-step). This is a flattened (`joinI-ed')
-- EnumeratorN elfrom elto m a
type EnumeratorGMM elfrom elto m a = IterateeG elto m a -> IterateeGM elfrom m a
-- | A TIFF directory is a finite map associating a TIFF tag with a record
-- TIFFDE
type TIFFDict = IntMap TIFFDE
data TIFFDE
TIFFDE :: Int -> TIFFDE_ENUM -> TIFFDE
tiffde_count :: TIFFDE -> Int
tiffde_enum :: TIFFDE -> TIFFDE_ENUM
data TIFFDE_ENUM
TEN_CHAR :: (forall a. EnumeratorGMM Word8 Char RBIO a) -> TIFFDE_ENUM
TEN_BYTE :: (forall a. EnumeratorGMM Word8 Word8 RBIO a) -> TIFFDE_ENUM
TEN_INT :: (forall a. EnumeratorGMM Word8 Integer RBIO a) -> TIFFDE_ENUM
TEN_RAT :: (forall a. EnumeratorGMM Word8 Rational RBIO a) -> TIFFDE_ENUM
-- | Standard TIFF data types
data TIFF_TYPE
TT_NONE :: TIFF_TYPE
TT_byte :: TIFF_TYPE
TT_ascii :: TIFF_TYPE
TT_short :: TIFF_TYPE
TT_long :: TIFF_TYPE
TT_rational :: TIFF_TYPE
TT_sbyte :: TIFF_TYPE
TT_undefined :: TIFF_TYPE
TT_sshort :: TIFF_TYPE
TT_slong :: TIFF_TYPE
TT_srational :: TIFF_TYPE
TT_float :: TIFF_TYPE
TT_double :: TIFF_TYPE
-- | Standard TIFF tags
data TIFF_TAG
TG_other :: Int -> TIFF_TAG
TG_SUBFILETYPE :: TIFF_TAG
TG_OSUBFILETYPE :: TIFF_TAG
TG_IMAGEWIDTH :: TIFF_TAG
TG_IMAGELENGTH :: TIFF_TAG
TG_BITSPERSAMPLE :: TIFF_TAG
TG_COMPRESSION :: TIFF_TAG
TG_PHOTOMETRIC :: TIFF_TAG
TG_THRESHOLDING :: TIFF_TAG
TG_CELLWIDTH :: TIFF_TAG
TG_CELLLENGTH :: TIFF_TAG
TG_FILLORDER :: TIFF_TAG
TG_DOCUMENTNAME :: TIFF_TAG
TG_IMAGEDESCRIPTION :: TIFF_TAG
TG_MAKE :: TIFF_TAG
TG_MODEL :: TIFF_TAG
TG_STRIPOFFSETS :: TIFF_TAG
TG_ORIENTATION :: TIFF_TAG
TG_SAMPLESPERPIXEL :: TIFF_TAG
TG_ROWSPERSTRIP :: TIFF_TAG
TG_STRIPBYTECOUNTS :: TIFF_TAG
TG_MINSAMPLEVALUE :: TIFF_TAG
TG_MAXSAMPLEVALUE :: TIFF_TAG
TG_XRESOLUTION :: TIFF_TAG
TG_YRESOLUTION :: TIFF_TAG
TG_PLANARCONFIG :: TIFF_TAG
TG_PAGENAME :: TIFF_TAG
TG_XPOSITION :: TIFF_TAG
TG_YPOSITION :: TIFF_TAG
TG_FREEOFFSETS :: TIFF_TAG
TG_FREEBYTECOUNTS :: TIFF_TAG
TG_GRAYRESPONSEUNIT :: TIFF_TAG
TG_GRAYRESPONSECURVE :: TIFF_TAG
TG_GROUP3OPTIONS :: TIFF_TAG
TG_GROUP4OPTIONS :: TIFF_TAG
TG_RESOLUTIONUNIT :: TIFF_TAG
TG_PAGENUMBER :: TIFF_TAG
TG_COLORRESPONSEUNIT :: TIFF_TAG
TG_COLORRESPONSECURVE :: TIFF_TAG
TG_SOFTWARE :: TIFF_TAG
TG_DATETIME :: TIFF_TAG
TG_ARTIST :: TIFF_TAG
TG_HOSTCOMPUTER :: TIFF_TAG
TG_PREDICTOR :: TIFF_TAG
TG_WHITEPOINT :: TIFF_TAG
TG_PRIMARYCHROMATICITIES :: TIFF_TAG
TG_COLORMAP :: TIFF_TAG
TG_BADFAXLINES :: TIFF_TAG
TG_CLEANFAXDATA :: TIFF_TAG
TG_CONSECUTIVEBADFAXLINES :: TIFF_TAG
TG_MATTEING :: TIFF_TAG
tag_to_int :: TIFF_TAG -> Int
int_to_tag :: Int -> TIFF_TAG
-- | The library function to read the TIFF dictionary
tiff_reader :: IterateeGM Word8 RBIO (Maybe TIFFDict)
-- | A few conversion procedures
u32_to_float :: Word32 -> Double
u32_to_s32 :: Word32 -> Int32
u16_to_s16 :: Word16 -> Int16
u8_to_s8 :: Word8 -> Int8
note :: [String] -> IterateeGM el RBIO ()
-- | An internal function to load the dictionary. It assumes that the
-- stream is positioned to read the dictionary
load_dict :: IterateeGM Word8 RBIO (Maybe TIFFDict)
-- | Reading the pixel matrix For simplicity, we assume no compression and
-- 8-bit pixels
pixel_matrix_enum :: TIFFDict -> EnumeratorN Word8 Word8 RBIO a
-- | A few helpers for getting data from TIFF dictionary
dict_read_int :: TIFF_TAG -> TIFFDict -> IterateeGM Word8 RBIO (Maybe Integer)
dict_read_ints :: TIFF_TAG -> TIFFDict -> IterateeGM Word8 RBIO (Maybe [Integer])
dict_read_rat :: TIFF_TAG -> TIFFDict -> IterateeGM Word8 RBIO (Maybe Rational)
dict_read_string :: TIFF_TAG -> TIFFDict -> IterateeGM Word8 RBIO (Maybe String)
instance Eq TIFF_TAG
instance Show TIFF_TAG
instance Eq TIFF_TYPE
instance Enum TIFF_TYPE
instance Ord TIFF_TYPE
instance Bounded TIFF_TYPE
instance Show TIFF_TYPE
-- | http://okmij.org/ftp/Haskell/misc.html#catch-MonadIO
--
-- The ability to use functions catch, bracket,
-- catchDyn, etc. in MonadIO other than IO itself has been a
-- fairly frequently requested feature:
--
--
-- http://www.haskell.org/pipermail/glasgow-haskell-users/2003-September/005660.html
--
--
-- http://haskell.org/pipermail/libraries/2003-February/000774.html
--
-- The reason it is not implemented is because these functions cannot be
-- defined for a general MonadIO. However, these functions can be easily
-- defined for a large and interesting subset of MonadIO. The following
-- code demonstrates that. It uses no extensions (other than those needed
-- for the Monad Transformer Library itself), patches no compilers, and
-- proposes no extensions. The generic catch has been useful in a
-- database library (Takusen), where many operations work in a monad
-- (ReaderT Session IO): IO with the environment containing the database
-- session data. Many other foreign libraries have a pattern of passing
-- around various handles, which are better hidden in a monad. Still, we
-- should be able to handle IO errors and user exceptions that arise in
-- these computations.
module Control.CaughtMonadIO
data MyException
MyException :: String -> MyException
-- | The implementation is quite trivial.
class (MonadIO m) => CaughtMonadIO m
gcatch :: (CaughtMonadIO m) => m a -> (Exception -> m a) -> m a
catchDyn :: (Typeable e, CaughtMonadIO m) => m a -> (e -> m a) -> m a
instance Typeable MyException
instance Show MyException
instance (Monoid w, CaughtMonadIO m) => CaughtMonadIO (RWST r w s m)
instance (CaughtMonadIO m) => CaughtMonadIO (StateT s m)
instance (Monoid w, CaughtMonadIO m) => CaughtMonadIO (WriterT w m)
instance (CaughtMonadIO m) => CaughtMonadIO (ReaderT r m)
instance (CaughtMonadIO m, Error e) => CaughtMonadIO (ErrorT e m)
instance CaughtMonadIO IO
-- | Haskell98
--
-- http://okmij.org/ftp/Algorithms.html#pure-cyclic-list
--
-- Pure functional, mutation-free, constant-time-access double-linked
-- lists
--
-- Note that insertions, deletions, lookups have a worst-case complexity
-- of O(min(n,W)), where W is either 32 or 64 (depending on the
-- paltform). That means the access time is bounded by a small constant
-- (32 or 64).
--
-- Pure functional, mutation-free, efficient double-linked lists
--
-- It is always an interesting challenge to write a pure functional and
-- efficient implementation of an imperative algorithm destructively
-- operating a data structure. The functional implementation has a
-- significant benefit of equational reasoning and modularity. We can
-- comprehend the algorithm without keeping the implicit global state in
-- mind. The mutation-free, functional realization has practical
-- benefits: the ease of adding checkpointing, undo and redo. The absence
-- of mutations makes the code multi-threading-safe and helps in porting
-- to distributed or non-shared-memory parallel architectures. On the
-- other hand, an imperative implementation has the advantage of
-- optimality: mutating a component in a complex data structure is a
-- constant-time operation, at least on conventional architectures.
-- Imperative code makes sharing explicit, and so permits efficient
-- implementation of cyclic data structures.
--
-- We show a simple example of achieving all the benefits of an
-- imperative data structure -- including sharing and the efficiency of
-- updates -- in a pure functional program. Our data structure is a
-- doubly-linked, possibly cyclic list, with the standard operations of
-- adding, deleting and updating elements; traversing the list in both
-- directions; iterating over the list, with cycle detection. The code:
--
-- uniformly handles both cyclic and terminated lists; does not
-- rebuild the whole list on updates; updates the value in the current
-- node in time bound by a small constant; does not use or mention any
-- monads; does not use any IORef, STRef, TVars, or any other
-- destructive updates; permits the logging, undoing and redoing of
-- updates, checkpointing; easily generalizes to two-dimensional
-- meshes.
--
-- The algorithm is essentially imperative, thus permitting identity
-- checking and in-place updates, but implemented purely
-- functionally. Although the code uses many local, type safe
-- heaps, there is emphatically no global heap and no global
-- state.
--
-- Version: The current version is 1.2, Jan 7, 2009.
--
-- References
--
-- Haskell-Cafe discussion ``Updating doubly linked lists''. January 2009
module Data.FDList
-- | Representation of the double-linked list
type Ref = Int
data Node a
Node :: a -> Ref -> Ref -> Node a
node_val :: Node a -> a
node_left :: Node a -> Ref
node_right :: Node a -> Ref
-- | Because DList contains the pointer to the current element,
-- DList is also a Zipper
data DList a
DList :: Ref -> Ref -> IntMap (Node a) -> DList a
dl_counter :: DList a -> Ref
dl_current :: DList a -> Ref
dl_mem :: DList a -> IntMap (Node a)
-- | Operations on the DList a
empty :: DList a
-- | In a well-formed list, dl_current must point to a valid node All
-- operations below preserve well-formedness
well_formed :: DList a -> Bool
is_empty :: DList a -> Bool
-- | auxiliary function
get_curr_node :: DList a -> Node a
-- | The insert operation below makes a cyclic list The other operations
-- don't care Insert to the right of the current element, if any Return
-- the DL where the inserted node is the current one
insert_right :: a -> DList a -> DList a
-- | Delete the current element from a non-empty list We can handle both
-- cyclic and terminated lists The right node becomes the current node.
-- If the right node does not exists, the left node becomes current
delete :: DList a -> DList a
get_curr :: DList a -> a
move_right :: DList a -> Maybe (DList a)
-- | If no right, just stay inplace
move_right' :: DList a -> DList a
move_left :: DList a -> Maybe (DList a)
-- | If no left, just stay inplace
move_left' :: DList a -> DList a
fromList :: [a] -> DList a
-- | The following does not anticipate cycles (deliberately)
takeDL :: Int -> DList a -> [a]
-- | Reverse taking: we move left
takeDLrev :: Int -> DList a -> [a]
-- | Update the current node inplace
update :: a -> DList a -> DList a
-- | This one watches for a cycle and terminates when it detects one
toList :: DList a -> [a]