-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/
-- | A collection of Oleg Kiselyov's Haskell modules (2008-2010)
--
-- A collection of Oleg Kiselyov's Haskell modules (2008-2010) (released
-- with his permission)
@package liboleg
@version 2010.1.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
-- | Embedding a higher-order domain-specific language (simply-typed
-- lambda-calculus with constants) with a selectable evaluation order:
-- Call-by-value, call-by-name, call-by-need in the same Final Tagless
-- framework This is the Haskell98 version of the code CB.hs located in
-- the same directory as this file
--
--
-- http://okmij.org/ftp/tagless-final/tagless-typed.html#call-by-any
module Language.CB98
-- | The (higher-order abstract) syntax of our DSL
type Arr exp a b = exp a -> exp b
class EDSL exp
lam :: (EDSL exp) => (exp a -> exp b) -> exp (Arr exp a b)
app :: (EDSL exp) => exp (Arr exp a b) -> exp a -> exp b
int :: (EDSL exp) => Int -> exp Int
add :: (EDSL exp) => exp Int -> exp Int -> exp Int
sub :: (EDSL exp) => exp Int -> exp Int -> exp Int
-- | A convenient abbreviation
let_ :: (EDSL exp) => exp a -> (exp a -> exp b) -> exp b
-- | A sample EDSL term
t :: (EDSL exp) => exp Int
-- | Interpretation of EDSL expressions as values of the host language
-- (Haskell) An EDSL expression of type a is interpreted as a Haskell
-- value of the type SName m a, SValue m a or SLazy m a, where m is a
-- Monad (the parameter of the interpretation).
newtype SName m a
SN :: m a -> SName m a
unSN :: SName m a -> m a
runName :: SName m a -> m a
-- | The addition (x add x) is performed twice because y is bound to
-- a computation, and y is evaluated twice
--
-- A more elaborate example
t1 :: (EDSL exp) => exp Int
-- | A better example
t2 :: (EDSL exp) => exp Int
-- | The result of subtraction was not needed, and so it was not performed
-- OTH, (int 5 add int 5) was computed four times
--
-- Call-by-value
newtype SValue m a
SV :: m a -> SValue m a
unSV :: SValue m a -> m a
-- | We reuse most of EDSL (SName) except for lam
vn :: SValue m x -> SName m x
nv :: SName m x -> SValue m x
runValue :: SValue m a -> m a
-- | We now evaluate the previously written tests t, t1, t2 under the new
-- interpretation
--
-- Call-by-need
share :: (MonadIO m) => m a -> m (m a)
newtype SLazy m a
SL :: m a -> SLazy m a
unSL :: SLazy m a -> m a
ln :: SLazy m x -> SName m x
nl :: SName m x -> SLazy m x
runLazy :: SLazy m a -> m a
instance (MonadIO m) => EDSL (SLazy m)
instance (MonadIO m) => MonadIO (SLazy m)
instance (Monad m) => Monad (SLazy m)
instance (MonadIO m) => EDSL (SValue m)
instance (MonadIO m) => MonadIO (SValue m)
instance (Monad m) => Monad (SValue m)
instance (MonadIO m) => EDSL (SName m)
instance (MonadIO m) => MonadIO (SName m)
instance (Monad m) => Monad (SName m)
-- | Embedding a higher-order domain-specific language (simply-typed
-- lambda-calculus with constants) with a selectable evaluation order:
-- Call-by-value, call-by-name, call-by-need in the same Final Tagless
-- framework
--
--
-- http://okmij.org/ftp/tagless-final/tagless-typed.html#call-by-any
module Language.CB
-- | Our EDSL is typed. EDSL types are built from the following two type
-- constructors:
data IntT
data (:->) a b
-- | We could have used Haskell's type Int and the arrow -> constructor.
-- We would like to emphasize however that EDSL types need not be
-- identical to the host language types. To give the type system to EDSL,
-- we merely need labels -- which is what IntT and :-> are
--
-- The (higher-order abstract) syntax of our DSL
class EDSL exp
lam :: (EDSL exp) => (exp a -> exp b) -> exp (a :-> b)
app :: (EDSL exp) => exp (a :-> b) -> exp a -> exp b
int :: (EDSL exp) => Int -> exp IntT
add :: (EDSL exp) => exp IntT -> exp IntT -> exp IntT
sub :: (EDSL exp) => exp IntT -> exp IntT -> exp IntT
-- | A convenient abbreviation
let_ :: (EDSL exp) => exp a -> (exp a -> exp b) -> exp b
-- | A sample EDSL term
t :: (EDSL exp) => exp IntT
-- | Interpretation of EDSL types as host language types The type
-- interpretation function Sem is parameterized by m, which is
-- assumed to be a Monad.
-- | Interpretation of EDSL expressions as values of the host language
-- (Haskell) An EDSL expression of the type a is interpreted as a Haskell
-- value of the type S l m a, where m is a Monad (the parameter of the
-- interpretation) and l is the label for the evaluation order (one of
-- Name, Value, or Lazy). (S l m) is not quite a monad -- only up to the
-- Sem interpretation
newtype S l m a
S :: m (Sem m a) -> S l m a
unS :: S l m a -> m (Sem m a)
-- | Call-by-name
data Name
runName :: S Name m a -> m (Sem m a)
-- | Evaluating:
--
--
-- t = (lam $ \x -> let_ (x `add` x)
-- $ \y -> y `add` y) `app` int 10
--
--
-- The addition (x add x) is performed twice because y is bound to
-- a computation, and y is evaluated twice
t1 :: (EDSL exp) => exp IntT
-- | A better example
t2 :: (EDSL exp) => exp IntT
-- | The result of subtraction was not needed, and so it was not performed
-- | OTH, (int 5 add int 5) was computed four times
data Value
-- | We reuse most of EDSL (S Name) except for lam
vn :: S Value m x -> S Name m x
nv :: S Name m x -> S Value m x
runValue :: S Value m a -> m (Sem m a)
share :: (MonadIO m) => m a -> m (m a)
data Lazy
-- | We reuse most of EDSL (S Name) except for lam
ln :: S Lazy m x -> S Name m x
nl :: S Name m x -> S Lazy m x
runLazy :: S Lazy m a -> m (Sem m a)
instance (MonadIO m) => EDSL (S Lazy m)
instance (MonadIO m) => EDSL (S Value m)
instance (MonadIO m) => EDSL (S Name m)
-- | 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
-- | Type-class overloaded functions: second-order typeclass programming
-- with backtracking
--
-- http://okmij.org/ftp/Haskell/types.html#poly2
module Control.Poly2
-- | The classes of types used in the examples below
type Fractionals = Float :*: (Double :*: HNil)
type Nums = Int :*: (Integer :*: (AllOf Fractionals :*: HNil))
type Ords = Bool :*: (Char :*: (AllOf Nums :*: HNil))
type Eqs = AllOf (TypeCl OpenEqs) :*: (AllOfBut Ords Fractionals :*: HNil)
-- | The Fractionals, Nums and Ords above are closed. But Eqs is open
-- (i.e., extensible), due to the following:
data OpenEqs
-- | Why we call Nums etc. a type class rather than a type set? The
-- following does not work: type synonyms can't be recursive.
--
--
-- type Russel = AllOfBut () Russel :*: HNil
--
--
-- But the more elaborate version does, with the expected result:
data RusselC
type Russel = AllOfBut () (TypeCl RusselC) :*: HNil
data AllOf x
data AllOfBut x y
data TypeCl x
-- | Classifies if the type x belongs to the open class labeled l The
-- result r is either HTrue or HFalse
class TypeCls l x r | l x -> r
-- | Deciding the membership in a closed class, specified by enumeration,
-- union and difference
data Member tl
class MemApp bf t x r | bf t x -> r
-- | we avoid defining a new class like MemApp above. I guess, after Apply,
-- we don't need a single class ever?
data MemCase2 h t x
-- | A type class for instance guards and back-tracking Here, pred and f
-- are labels and n is of a kind numeral.
class GFN n f a pred | n f a -> pred
-- | The guard that always succeeds (cf. otherwise in Haskell)
data Otherwise
newtype GFn f
GFn :: f -> GFn f
newtype GFnA n f
GFnA :: f -> GFnA n f
newtype GFnTest n f flag
GFnTest :: f -> GFnTest n f flag
-- | A generic function that tests if its argument is a member of Eqs
data IsAnEq
IsAnEq :: IsAnEq
-- | The main test: approximate equality. See the article for the
-- description.
data PairOf t
data ApproxEq
ApproxEq :: ApproxEq
data ApproxEq'
ApproxEq' :: ApproxEq'
data HNil
HNil :: HNil
data (:*:) a b
(:*:) :: a -> b -> :*: a b
data HTrue
data HFalse
data Z
Z :: Z
newtype S n
S :: n -> S n
class TypeCast a b | a -> b, b -> a
typeCast :: (TypeCast a b) => a -> b
class TypeCast' t a b | t a -> b, t b -> a
typeCast' :: (TypeCast' t a b) => t -> a -> b
class TypeCast'' t a b | t a -> b, t b -> a
typeCast'' :: (TypeCast'' t a b) => t -> a -> b
class TypeEq x y b | x y -> b
class Apply f a r | f a -> r
apply :: (Apply f a r) => f -> a -> r
instance [overlap ok] Apply (x -> y) x y
instance [overlap ok] (TypeCast HFalse b) => TypeEq x y b
instance [overlap ok] TypeEq x x HTrue
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] Apply (GFnA n ApproxEq') a Bool
instance [overlap ok] (TypeCast pred Otherwise) => GFN n ApproxEq' a pred
instance [overlap ok] (Num x, Ord x) => Apply (GFnA Z ApproxEq') (x, x) Bool
instance [overlap ok] GFN Z ApproxEq' (x, x) (PairOf (Member Nums))
instance [overlap ok] (Fractional x, Ord x) => Apply (GFnA (S Z) ApproxEq') (x, x) Bool
instance [overlap ok] GFN (S Z) ApproxEq' (x, x) (PairOf (Member Fractionals))
instance [overlap ok] Apply (GFnA n ApproxEq) a Bool
instance [overlap ok] (TypeCast pred Otherwise) => GFN n ApproxEq a pred
instance [overlap ok] (Apply (GFn ApproxEq) (x, x) Bool, Eq x) => Apply (GFnA (S (S (S Z))) ApproxEq) ((x, x), (x, x)) Bool
instance [overlap ok] GFN (S (S (S Z))) ApproxEq ((x, x), (x, x)) (PairOf (PairOf (Member Nums)))
instance [overlap ok] (Eq x) => Apply (GFnA (S (S Z)) ApproxEq) (x, x) Bool
instance [overlap ok] GFN (S (S Z)) ApproxEq (x, x) (PairOf (Member Eqs))
instance [overlap ok] (Num x, Ord x) => Apply (GFnA (S Z) ApproxEq) (x, x) Bool
instance [overlap ok] GFN (S Z) ApproxEq (x, x) (PairOf (Member Nums))
instance [overlap ok] (Fractional x, Ord x) => Apply (GFnA Z ApproxEq) (x, x) Bool
instance [overlap ok] GFN Z ApproxEq (x, x) (PairOf (Member Fractionals))
instance [overlap ok] (TypeCast r HFalse) => Apply (PairOf t) x r
instance [overlap ok] (Apply t x r) => Apply (PairOf t) (x, x) r
instance [overlap ok] (Apply (GFn IsAnEq) x Bool, Apply (GFn IsAnEq) y Bool) => Apply (GFnA (S Z) IsAnEq) (x, y) Bool
instance [overlap ok] GFN (S Z) IsAnEq (x, y) Otherwise
instance [overlap ok] Apply (GFnA n IsAnEq) a Bool
instance [overlap ok] (TypeCast pred Otherwise) => GFN n IsAnEq a pred
instance [overlap ok] Apply (GFnA Z IsAnEq) a Bool
instance [overlap ok] GFN Z IsAnEq a (Member Eqs)
instance [overlap ok] (GFN (S n) f a pred, Apply pred a flag, Apply (GFnTest (S n) f flag) a b) => Apply (GFnTest n f HFalse) a b
instance [overlap ok] (Apply (GFnA n f) a b) => Apply (GFnTest n f HTrue) a b
instance [overlap ok] (GFN Z f a pred, Apply pred a flag, Apply (GFnTest Z f flag) a b) => Apply (GFn f) a b
instance [overlap ok] Apply Otherwise a HTrue
instance [overlap ok] (Apply (Member (AllOf h :*: t)) x r) => Apply (MemCase2 h t x) HFalse r
instance [overlap ok] (Apply (Member t) x r) => Apply (MemCase2 h t x) HTrue r
instance [overlap ok] (Apply (Member t) x r) => MemApp HFalse t x r
instance [overlap ok] MemApp HTrue t x HTrue
instance [overlap ok] (Apply (Member exc) x bf, Apply (MemCase2 h t x) bf r) => Apply (Member (AllOfBut h exc :*: t)) x r
instance [overlap ok] (Apply (Member h) x bf, MemApp bf t x r) => Apply (Member (AllOf h :*: t)) x r
instance [overlap ok] (TypeEq h x bf, MemApp bf t x r) => Apply (Member (h :*: t)) x r
instance [overlap ok] (TypeCls l x r) => Apply (Member (TypeCl l)) x r
instance [overlap ok] Apply (Member HNil) x HFalse
instance [overlap ok] (TypeCast r HFalse) => TypeCls l x r
instance [overlap ok] (Apply (Member Russel) x r) => TypeCls RusselC x r
instance [overlap ok] TypeCls OpenEqs () HTrue
-- | Extensible Denotational Semantics
--
-- This work is a generalization of /Extensible Denotational Language
-- Specifications Robert Cartwright, Matthias Felleisen Theor. Aspects of
-- Computer Software, 1994/ http://citeseer.ist.psu.edu/69837.html
--
-- to be referred to as EDLS.
--
-- We implement the enhanced EDLS in Haskell and add delimited control.
-- To be precise, we implement the Base interpreter (whose sole
-- operations are Loop and Error) and the following extensions: CBV
-- lambda-calculus, Arithmetic, Storage, Control. The extensions can be
-- added to the Base interpreter in any order and in any combination.
--
-- Our implementation has the following advantages over EDLS:
--
--
-- - support for delimited control * support for a local storage
-- (including `thread-local' storage and general delimited dynamic
-- binding) * extensions do not have to be composed explicitly, and so
-- the composition order truly does not matter. In the original EDLS, one
-- had to write interpreter composition explicitly. In our approach, an
-- extension is pulled in automatically if the program includes the
-- corresponding syntactic forms. For example, if a program contains
-- storage cell creation and dereference operations, the Storage
-- extension will automatically be used to interpret the program.
--
--
-- Our main departure from EDLS is is the removal of the `central
-- authority'. There is no semantic admin function. Rather,
-- admin is part of the source language and can be used at any place in
-- the code. The `central authority' of EDLS must be an extensible
-- function, requiring meta-language facilities to implement (such as
-- quite non-standard Scheme modules). We do not have central authority.
-- Rather, we have bureaucracy: each specific effect handler interprets
-- its own effects as it can, throwing the rest upstairs for
-- higher-level bureaucrats to deal with. Extensibility arises
-- automatically.
--
-- We take the meaning of a program to be the union of Values and
-- (unfulfilled) Actions. If the meaning of the program is a (non-bottom)
-- value, the program is terminating. If the meaning of the program is an
-- Action -- the program finished with an error, such as an action to
-- access a non-existing storage cell, or shift without reset, or a
-- user-raised error.
--
-- Incidentally, EDLS stresses on p. 2 (the last full paragraph) that
-- their schema critically relies on the distinction between a complete
-- program and a nested program phrase. Our contribution (which is the
-- consequence of removing the central admin, making it first-class) is
-- eliminating such a distinction! EDLS says, at the very top of p. 3,
-- that the handle in the effect message ``is roughly a conventional
-- continuation.'' Because the admin of EDLS is outside of the
-- program (at the point of infinity, so to speak), its continuation
-- indeed appears undelimited. By making our admin a part of the
-- source language, we recognize the handle in the effect message for
-- what it is: a _delimited_ continuation.
--
-- As we see below, the Control aspect is orthogonal to the CBV aspect.
-- So, we can just as easily replace the CBV extension with the CBN
-- extension, which will give us the denotation of delimited control in
-- CBN.
--
-- We shall be using Haskell to express denotations, taking advantage of
-- the fact that Haskell values are lifted. See also the remark
-- on p21 of EDLS: someone (ref. [4]) showed that sets and partial
-- functions can suffice...
--
-- Our program denotations are stable: they have the same form regardless
-- of a particular composition of modular interpreters. See Section 3.5
-- of EDLS for precise formulation (and the last paragraph of Section 3.4
-- for concise informal statement of stability). Also see the comparison
-- with the monads on p. 20: different monads assign numeral radically
-- different meanings, depending on the monad. But in EDLS, a numeral has
-- exactly the same denotation.
--
-- The meaning of an expression is also the same and stable, no matter
-- what the interpreter is: it is a function from Env to Computations
-- (the latter being the union of values and unfulfilled effects -- the
-- same union mentioned above).
--
-- However, by using handlers, some effect messages can be subtracted:
-- so, strictly speaking, the denotation of a fragment is V +
-- effect-message-issued - effect-messages handled. There seem to be a
-- connection with effect systems.
--
-- Additional notes on EDLS:
--
-- The abstract and p. 2 (especially the last full paragraph) are so
-- well-written!
--
-- p. 5, bottom: ``It [ref x.x, where ref means what it does in ML] is a
-- closed expression that does not diverge, is not a value, and cannot be
-- reduced to a value without affecting the context. We refer to such
-- results as _effects_.''
--
-- Beginning of Section 3 and App A give a very good introduction to the
-- denotational semantics.
--
-- p. 6: ``Algebraically speaking, the interpreter is (roughly) a
-- homomorphism from syntax to semantics''
--
-- ``A straightforward representation of an evaluation context is a
-- function from values to computations, which directly corresponds to
-- its operational usage as a function from syntactic values to
-- expressions.'' (p. 8). EDLS then notices that the handle has
-- the same type as the denotation of a context. Footnote 6 notes that
-- handler is roughly the composition combinator for functions from
-- values to computations [contexts!] and it superficially relates to
-- [bind] but does not satisfy all monad laws.
--
-- The last of EDLS Sec 3.5, p. 15: ``Informally speaking, this property
-- [stable denotations] asserts that in the framework of extensible
-- semantics, the addition of a programming construct corresponds to the
-- addition of a new `dimension' to the space of meaning. [The
-- equations, featuring injection and projection functions, make that
-- precise and clear.] The reader may want to contrast this general
-- statement with the numerous papers on the relationship between direct
-- and continuation semantics.''
--
-- The practical consequence of the lack of stability of denotations for
-- monads is that monadic transformers put layers upon layers of thunks,
-- which have to be carried over _in full_ from one sub-expression into
-- the other, even if no single subexpression uses all of the features.
--
-- The present code is not written in idiomatic Haskell and does not take
-- advantage of types at all. The ubiquitous projections from the
-- universal domain tantamount to ``dynamic typing.'' The code is
-- intentionally written to be close to the EDLS paper, emphasizing
-- denotational semantics (whose domains are untyped). One can certainly
-- do better, for example, employ user-defined datatypes for tagged
-- values, avoiding the ugly string-tagged VT.
module Control.ExtensibleDS
-- | The universal domain Yes, it is untyped... But Denot semantics is like
-- this anyway... Bottom is the implicit member of this domain.
data Value
VI :: Int -> Value
VS :: String -> Value
VP :: Value -> Value -> Value
VF :: (Value -> Value) -> Value
VT :: Tag -> Value -> Value
type Tag = String
type Action = Value
-- | Computations: just like in EDLS The strictness of inV guarantees that
-- inV bottom = bottom, as on Fig. 3 of EDLS Error is always a part of
-- the computation
data Comp
InV :: !Value -> Comp
InFX :: (Value -> Comp) -> Action -> Comp
-- | Auxiliary functions
newtype V
V :: String -> V
type Env v = V -> v
-- | Note that inV is essentially the identity partial
-- continuation
--
-- The error raise action and its tag
--
-- The universal handler of actions It propagates the action request InFX
-- up. Since we do case-analysis on the first argument, v, the handler is
-- strict in that argument. That is, handler bottom ==> bottom, as
-- required by Fig. 3 of EDLS. The last clause is essentially the
-- denotation of a `control channel'
--
-- Expressions and their interpretations This is an open data type and an
-- open function. Haskell typeclasses are ideal for that.
--
-- This is the function curlyM of EDLS
class Interpretor exp
interpret :: (Interpretor exp) => exp -> Env Value -> Comp
-- | The base language has only two expressions: omega and error See Fig. 3
-- (p. 7) of EDLS
data BE_err
BE_err :: BE_err
data BE_omega
BE_omega :: BE_omega
-- | The meaning of a program
--
-- Extension: Call-by-Value: see a part Fig. 4 of EDLS (or, Fig. 8)
--
-- We add closures (procedures) to the Base
type Proc = Value -> Comp
class PV u
inP :: (PV u) => Proc -> u
prP :: (PV u) => u -> Maybe (Proc)
type Var = V
data Lam e
Lam :: V -> e -> Lam e
data App e1 e2
(:@) :: e1 -> e2 -> App e1 e2
-- | Create a few variables for use in examples
vy :: Var
vr :: Var
vf :: Var
vx :: Var
-- | Denotations of the new actions (injproj tofrom the Universal
-- Domain)
--
-- inject and project computations
inComp :: Comp -> Value
prComp :: Value -> Maybe Comp
-- | Extension: Arithmetic: see a part Fig. 4 of EDLS
class PN u
inN :: (PN u) => Int -> u
prN :: (PN u) => u -> Maybe Int
data IntC
IntC :: Int -> IntC
data Add1
Add1 :: Add1
-- | Extension: State: see Fig. 5 of EDLS
newtype Loc
Loc :: Int -> Loc
class PL u
inL :: (PL u) => Loc -> u
prL :: (PL u) => u -> Maybe Loc
-- | a better idea is Loc -> Maybe Value, so that when lookup fails, we
-- can re-throw that Deref or Set message. That would make the storage
-- extensible... The first component of the pair is the allocation
-- counter
type Sto = (Int, Loc -> Value)
inSto :: Sto -> Value
prSto :: Value -> Maybe Sto
init_sto :: Sto
-- | new expressions
data Ref e
Ref :: e -> Ref e
data Deref e
Deref :: e -> Deref e
data Set e1 e2
Set :: e1 -> e2 -> Set e1 e2
-- | Now we need a storage admin It is treated as an expression in the
-- source language!
data StoAdmin e
StoAdmin :: Sto -> e -> StoAdmin e
inControl :: (Value -> Comp) -> Value
prControl :: Value -> Maybe (Value -> Comp)
data Control e
Control :: e -> Control e
data ControlAdmin e
ControlAdmin :: e -> ControlAdmin e
instance Eq Loc
instance Show Loc
instance Eq V
instance Show V
instance (Interpretor e) => Interpretor (ControlAdmin e)
instance (Interpretor e) => Interpretor (Control e)
instance PL Value
instance (Interpretor e) => Interpretor (StoAdmin e)
instance (Interpretor e1, Interpretor e2) => Interpretor (Set e1 e2)
instance (Interpretor e) => Interpretor (Deref e)
instance (Interpretor e) => Interpretor (Ref e)
instance PN Value
instance Interpretor Add1
instance Interpretor IntC
instance PV Value
instance (Interpretor e1, Interpretor e2) => Interpretor (App e1 e2)
instance (Interpretor e) => Interpretor (Lam e)
instance Interpretor V
instance Interpretor BE_err
instance Interpretor BE_omega
instance Show Comp
instance Show Value
-- | Variable state monad
--
-- http://okmij.org/ftp/Computation/monads.html#param-monad
--
-- The familiar State monad lets us represent computations with a state
-- that can be queried and updated. The state must have the same type
-- during the entire computation however. One sometimes wants to express
-- a computation where not only the value but also the type of the state
-- can be updated -- while maintaining static typing. We wish for a
-- parameterized monad that indexes each monadic type by an
-- initial (type)state and a final (type)state. The effect of an
-- effectful computation thus becomes apparent in the type of the
-- computation, and so can be statically reasoned about.
module Control.VarStateM
-- | A parameterized monad
class Monadish m
gret :: (Monadish m) => a -> m p p a
gbind :: (Monadish m) => m p q a -> (a -> m q r b) -> m p r b
-- | Inject regular monads to be monadish things too
newtype MW m p q a
MW :: m a -> MW m p q a
unMW :: MW m p q a -> m a
-- | First, use the regular Monad.State
--
-- Now, wrap in MW
--
-- Introduce the variable-type state
newtype VST m si so v
VST :: (si -> m (so, v)) -> VST m si so v
runVST :: VST m si so v -> si -> m (so, v)
vsget :: (Monad m) => VST m si si si
vsput :: (Monad m) => so -> VST m si so ()
-- | Try polymorphic recursion, over the state. crec1 invokes itself, and
-- changes the type of the state from some si to Bool.
crec1 :: (Enum si, Monad m) => VST m si si Int
-- | Another example, to illustrate locking and static reasoning about the
-- locking state
data Locked
Locked :: Locked
data Unlocked
Unlocked :: Unlocked
data LIO p q a
LIO :: IO a -> LIO p q a
unLIO :: LIO p q a -> IO a
lput :: String -> LIO p p ()
lget :: LIO p p String
lock :: LIO Unlocked Locked ()
unlock :: LIO Locked Unlocked ()
instance Monadish LIO
instance (Monad m) => Monadish (VST m)
instance (Monad m) => Monadish (MW m)
-- | Implementation of the calculus lambda-sr-let
--
--
-- Polymorphic delimited continuations
-- Asai and Kameyama, APLAS 2007
-- http://logic.cs.tsukuba.ac.jp/~kam/paper/aplas07.pdf
-- hereafter, AK07
--
--
-- This embedding of the AK07 calculus into Haskell is another proof that
-- AK07 admit type inference algorithm. In all the tests below, all the
-- types are inferred.
module Control.ShiftResetGenuine
-- | Parameterized monad. This is almost the same monad used in the
-- Region-IO and TFP07 paper See also
--
--
-- Robert Atkey, Parameterised Notions of Computation, Msfp2006
-- http://homepages.inf.ed.ac.uk/ratkey/param-notions.pdf
--
--
-- and
--
--
-- http://www.haskell.org/pipermail/haskell/2006-December/018917.html
--
class Monadish m
ret :: (Monadish m) => tau -> m a a tau
bind :: (Monadish m) => m b g sigma -> (sigma -> m a b tau) -> m a g tau
-- | Inject regular monads to be monadish things too
newtype MW m p q a
MW :: m a -> MW m p q a
unMW :: MW m p q a -> m a
-- | some syntactic sugar
--
-- The continuation monad parameterized by two answer types We represent
-- the the effectful expression e, whose type is characterized by the
-- judgement
--
--
-- Gamma; a |- e:tau; b
--
--
-- as a parameterized monad C a b tau. We represent an effectful function
-- type sigmaa -> taub of the calculus as an arrow type sigma
-- -> C a b tau. Incidentally, this notational convention
-- expresses the rule fun in AK07
newtype C a b tau
C :: ((tau -> a) -> b) -> C a b tau
unC :: C a b tau -> (tau -> a) -> b
-- | The rules from AK07 as they are (see Fig 3)
reset :: C sigma tau sigma -> C a a tau
-- | shift.
shift :: ((tau -> C t t a) -> C s b s) -> C a b tau
run :: C tau tau tau -> tau
-- | The append example from AK07, section 2.1
--
-- The sprintf test: Sec 2.3 of AK07 The paper argues this test requires
-- both the changing of the answer type and polymorphism (fmt is used
-- polymorphically in stest3)
int :: Int -> String
str :: String -> String
instance Monadish C
instance (Monad m) => Monadish (MW m)
-- | 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
-- | Haskell with only one typeclass
--
-- http://okmij.org/ftp/Haskell/Haskell1/Class1.hs
--
-- http://okmij.org/ftp/Haskell/types.html#Haskell1
--
-- How to make ad hoc overloading less ad hoc while defining no type
-- classes. For clarity, we call as Haskell1 the language Haskell98 with
-- no typeclass declarations but with a single, pre-defined typeclass C
-- (which has two parameters related by a functional dependency). The
-- programmers may not declare any typeclasses; but they may add
-- instances to C and use them. We show on a series of examples that
-- despite the lack of typeclass declarations, Haskell1 can express all
-- the typeclass code of Haskell98 plus multi-parameter type classes and
-- even some (most useful?) functional dependencies.
--
-- Haskell1 is not a new language and requires no new compilers; rather,
-- it is a subset of the current Haskell. The removal of
-- typeclass declarations is merely the matter of discipline.
module Data.Class1
-- | The one and only type class present in Haskell1
class C l t | l -> t
ac :: (C l t) => l -> t
-- | Example 1: Building overloaded numeric functions, the analogue of Num.
-- The following defines overloaded numeric functions `a la carte'. We
-- shall see how to bundle such methods into what Haskell98 calls
-- classes
data Add a
data Mul a
data FromInteger a
-- | We can now define the generic addition. We use the operation +$ to
-- avoid the confusion with Prelude.(+)
--
-- In H98, the overloaded addition was a method. In Haskell1, it is an
-- ordinary (bounded polymorphic) function The signature looks a bit
-- ugly; we'll see how to simplify it a bit
(+$) :: (C (Add a) (a -> a -> a)) => a -> a -> a
-- | We now illustrate overloading over datatypes other than basic ones. We
-- define dual numbers (see Wikipedia)
data Dual a
Dual :: a -> a -> Dual a
-- | Here is a different, perhaps simpler, way of defining signatures of
-- overloaded functions. The constraint C is inferred and no longer has
-- to be mentioned explicitly
mul_sig :: a -> a -> a
mul_as :: a -> Mul a
-- | and the corresponding overloaded function (which in Haskell98 was a
-- method) Again, we chose a slightly different name to avoid the
-- confusion with the Prelude
frmInteger :: (C (FromInteger a) (Integer -> a)) => Integer -> a
-- | We can define generic function at will, using already defined
-- overloaded functions. For example,
data SHOW a
shw :: (C (SHOW a) (a -> String)) => a -> String
-- | Finally, we demonstrate overloading of non-functional values, such as
-- minBound and maxBound. These are not methods in the classical
-- sense.
data MinBound a
mnBound :: (C (MinBound a) a) => a
-- | We are defining a super-set of monads, so called `restricted monads'.
-- Restricted monads include all ordinary monads; in addition, we can
-- define a SET monad. See
-- http://okmij.org/ftp/Haskell/types.html#restricted-datatypes
data RET m :: (* -> *) a
data BIND m :: (* -> *) a b
ret :: (C (RET m a) (a -> m a)) => a -> m a
bind :: (C (BIND m a b) (m a -> (a -> m b) -> m b)) => (m a -> (a -> m b) -> m b)
instance (Show a) => Show (Dual a)
instance (C (SHOW a) (a -> String)) => C (SHOW (Maybe a)) (Maybe a -> String)
instance C (BIND (Either e) a b) (Either e a -> (a -> Either e b) -> Either e b)
instance C (RET (Either e) a) (a -> Either e a)
instance C (BIND Maybe a b) (Maybe a -> (a -> Maybe b) -> Maybe b)
instance C (RET Maybe a) (a -> Maybe a)
instance C (MinBound Bool) Bool
instance C (MinBound Int) Int
instance (C (SHOW a) (a -> String)) => C (SHOW (Dual a)) (Dual a -> String)
instance C (SHOW Float) (Float -> String)
instance C (SHOW Int) (Int -> String)
instance (C (FromInteger a) (Integer -> a)) => C (FromInteger (Dual a)) (Integer -> Dual a)
instance C (FromInteger Float) (Integer -> Float)
instance C (FromInteger Int) (Integer -> Int)
instance (C (Add a) (a -> a -> a), C (Mul a) (a -> a -> a)) => C (Mul (Dual a)) (Dual a -> Dual a -> Dual a)
instance C (Mul Float) (Float -> Float -> Float)
instance C (Mul Int) (Int -> Int -> Int)
instance (C (Add a) (a -> a -> a)) => C (Add (Dual a)) (Dual a -> Dual a -> Dual a)
instance C (Add Float) (Float -> Float -> Float)
instance C (Add Int) (Int -> Int -> Int)
-- | Haskell with only one typeclass
--
-- http://okmij.org/ftp/Haskell/Haskell1/Class2.hs
--
-- http://okmij.org/ftp/Haskell/types.html#Haskell1
--
-- How to make ad hoc overloading less ad hoc while defining no type
-- classes. Haskell1' -- the extension of Haskell1 with functional
-- dependencies, and bounded-polymorphic higher-rank types
module Data.Class2
-- | Some functional dependencies: implementing Monad Error As it turns
-- out, some functional dependencies are expressible already in Haskell1.
-- The example is MonadError, which in Haskell' has the form
data ERROR a
strMsg :: (C (ERROR a) (String -> a)) => String -> a
data ThrowError m :: (* -> *) a
throwError :: (C (ThrowError m a) (e -> m a), C (RET m a) t1, C (BIND m a b) t2) => e -> m a
data CatchError m :: (* -> *) a
catchError :: (C (CatchError m a) (m a -> (e -> m a) -> m a)) => m a -> (e -> m a) -> m a
data FC1 a b c
fc1 :: (C (FC1 a b c) (a -> b -> c)) => a -> b -> c
data FC2 a b c
fc2 :: (C (FC2 a b c) (a -> b -> c)) => a -> b -> c
data FC3 a b c
fc3 :: (C (FC3 a b c) (a -> b -> c)) => a -> b -> c
data FromList e
fromList :: (C (FromList e) (Int -> [e] -> array)) => Int -> [e] -> array
data Index e
indexA :: (C (Index e) (array -> Int -> e)) => (array -> Int -> e)
data NUM a
NUM :: (a -> a -> a) -> (a -> a -> a) -> (Integer -> a) -> (a -> String) -> NUM a
nm_add :: NUM a -> a -> a -> a
nm_mul :: NUM a -> a -> a -> a
nm_fromInteger :: NUM a -> Integer -> a
nm_show :: NUM a -> a -> String
data CLS a
(+$$) :: (C (CLS (NUM a)) (NUM a)) => a -> a -> a
(*$$) :: (C (CLS (NUM a)) (NUM a)) => a -> a -> a
nshw :: (C (CLS (NUM a)) (NUM a)) => a -> String
nfromI :: (C (CLS (NUM a)) (NUM a)) => Integer -> a
data PACK
PACK :: a -> PACK
class TypeCast a b | a -> b, b -> a
typeCast :: (TypeCast a b) => a -> b
class TypeCast' t a b | t a -> b, t b -> a
typeCast' :: (TypeCast' t a b) => t -> a -> b
class TypeCast'' t a b | t a -> b, t b -> a
typeCast'' :: (TypeCast'' t a b) => t -> a -> b
instance TypeCast'' () a a
instance (TypeCast'' t a b) => TypeCast' t a b
instance (TypeCast' () a b) => TypeCast a b
instance (C (Add a) (a -> a -> a), C (Mul a) (a -> a -> a), C (FromInteger a) (Integer -> a), C (SHOW a) (a -> String)) => C (CLS (NUM a)) (NUM a)
instance (C (Index a) (ara -> Int -> a), C (Index b) (arb -> Int -> b)) => C (Index (a, b)) ((ara, arb) -> Int -> (a, b))
instance C (Index Char) (String -> Int -> Char)
instance C (Index Bool) ((Int, Integer) -> Int -> Bool)
instance (C (FromList a) (Int -> [a] -> ara), C (FromList b) (Int -> [b] -> arb)) => C (FromList (a, b)) (Int -> [(a, b)] -> (ara, arb))
instance C (FromList Char) (Int -> [Char] -> String)
instance C (FromList Bool) (Int -> [Bool] -> (Int, Integer))
instance (TypeCast (FC3 Bool b c) (FC3 Bool Char Int)) => C (FC3 Bool b c) (Bool -> Char -> Int)
instance (TypeCast c Int) => C (FC2 Bool Char c) (Bool -> Char -> Int)
instance C (FC1 Bool Char Int) (Bool -> Char -> Int)
instance C (CatchError (Either e) a) (Either e a -> (e -> Either e a) -> Either e a)
instance C (ThrowError (Either e) a) (e -> Either e a)
instance C (ERROR String) (String -> String)
-- | 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]