liboleg 0.1 → 0.1.0.1

raw patch · 4 files changed

+592/−7 lines, 4 filesdep +mtlPVP: minor bump suggested

API additions: PVP suggests at least a minor version bump

Dependencies added: mtl

API changes (from Hackage documentation)

Files

• Control/CaughtMonadIO.hs +118/−0
• Language/TypeFN.hs +208/−0
• Language/TypeLC.hs +258/−0
• liboleg.cabal +8/−7

@@ -0,0 +1,118 @@+-- +-- |+-- <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.+-- ++{-# OPTIONS -fglasgow-exts #-}++module Control.CaughtMonadIO where++import Data.Typeable+import Data.Dynamic+import Control.Monad.Trans+import Control.Exception hiding (catch, catchDyn)+import qualified Control.Exception (catch)+import Control.Monad.Reader+import Control.Monad.Writer+import Control.Monad.State+import Control.Monad.RWS+import Control.Monad.Error++---------------------  Tests++data MyException = MyException String deriving (Show, Typeable)++testfn True = throwDyn (MyException "thrown")+testfn False = return True++testc m = catchDyn (m >>= return . show) (\ (MyException s) -> return s)++test1 = do tf True >>= print; tf False >>= print+  where+   tf x = runReaderT (runWriterT (testc (do+                                          tell "begin"+                                          r <- ask+                                          testfn r))) x++{-+*CaughtMonadIO> test1+("thrown","")+("True","begin")+-}+++test2 = do tf True >>= print; tf False >>= print;+  where+   tf x = runReaderT (runErrorT (do+                                  r <- ask+                                  testfn r `catchDyn` +                                   (\ (MyException s) -> throwError s))) x++{-+*CaughtMonadIO> test2+Left "thrown"+Right True+-}+++-- | The implementation is quite trivial.+class MonadIO m => CaughtMonadIO m where+     gcatch :: m a -> (Exception -> m a) -> m a++instance CaughtMonadIO IO where+     gcatch = Control.Exception.catch++instance (CaughtMonadIO m, Error e) => CaughtMonadIO (ErrorT e m) where+     gcatch m f = mapErrorT (\m -> gcatch m (\e -> runErrorT $ f e)) m++-- | The following is almost verbatim from `Control.Monad.Error'+-- Section "MonadError instances for other monad transformers"+--+instance CaughtMonadIO m => CaughtMonadIO (ReaderT r m) where+     gcatch m f = ReaderT $ +                  \r -> gcatch (runReaderT m r) (\e -> runReaderT (f e) r)++-- | The following instances presume that an exception that occurs in+-- 'm' discard the state accumulated since the beginning of 'm's execution.+-- If that is not desired -- don't use StateT. Rather, allocate+-- IORef and carry that _immutable_ value in a ReaderT. The accumulated+-- state will thus persist. One can always use IORefs within+-- any MonadIO.+instance (Monoid w, CaughtMonadIO m) => CaughtMonadIO (WriterT w m) where+         m `gcatch` h = WriterT $ runWriterT m+                 `gcatch` \e -> runWriterT (h e)++instance CaughtMonadIO m => CaughtMonadIO (StateT s m) where+         m `gcatch` h = StateT $ \s -> runStateT m s+                 `gcatch` \e -> runStateT (h e) s++instance (Monoid w, CaughtMonadIO m) => CaughtMonadIO (RWST r w s m) where+         m `gcatch` h = RWST $ \r s -> runRWST m r s+                 `gcatch` \e -> runRWST (h e) r s+++catchDyn :: (Typeable e, CaughtMonadIO m) => m a -> (e -> m a) -> m a+catchDyn m f = gcatch m (\e -> maybe (throw e) f ((dynExceptions e) +                                                   >>= fromDynamic))+

@@ -0,0 +1,208 @@+-- +-- |+-- +-- <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.+-- ++{-# LANGUAGE KindSignatures, TypeOperators, EmptyDataDecls, Rank2Types #-}+{-# LANGUAGE FlexibleContexts, FlexibleInstances, TypeSynonymInstances  #-}+{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies #-}+{-# LANGUAGE UndecidableInstances #-}+module Language.TypeFN where++import Language.TypeLC                 -- Load part I of this series (prev message)+++-- | 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'+instance A (F Prop') f (F (Prop',f))+instance A (F (Prop',f)) Zero Bool+instance E (f :< m) r => A (F (Prop',f)) (Su m) (Bool -> r)+type Prop  = Rec (F Prop')++type Prop2 = E (F Prop :< N2) r => r+and2 = (\x y -> x && y) `asTypeOf` (undefined:: Prop2)+++-- | 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+instance E (F Prop :< (F Fib :< n)) r => A (F StrangeProp) n r++oddand4t :: E (F StrangeProp :< (F FSum :< N2 :< N2)) r => r+oddand4t = undefined++oddand5 = (\x1 x2 x3 x4 -> ((x1 && x2 && x3) &&) . and2 x4)+    `asTypeOf` oddand4t++-- > *DepType> :t oddand4t+-- > oddand4t :: Bool -> Bool -> Bool -> Bool -> Bool -> Bool++-- | We can do better, with the help of higher-order type functions.  First+-- we declare a few standard Haskell type constants as constants in our+-- calculus, with trivial evaluation rules+--+instance E Bool Bool +instance E Int Int+instance E String String+instance E (a->b) (a->b)              -- We could just as well evaluate under+instance E (a,b) (a,b)                -- these++-- | 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+instance A (F Ntimes) f (F (Ntimes,f)) +instance A (F (Ntimes,f)) x (F (Ntimes,f,x))+instance A (F (Ntimes,f,x)) Zero x +instance E (F Ntimes :< f :< (f :< x) :< n) r => A (F (Ntimes,f,x)) (Su n) r++data ATC1 c+instance A (F (ATC1 c)) x (c x)++-- | 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+and2' = (\x y -> x && y) `asTypeOf` (undefined:: PropN' N2)+++-- | To generalize,+--+data ATC2 (c :: * -> * -> *)+instance A (F (ATC2 c)) x (F (ATC1 (c x))) -- currying of type constructors++type SPropN' n = E(F Ntimes :< (F (ATC2 (->)) :< Bool) :< Bool+                            :< (F Fib :< n)) r => r+test_spn4 = undefined::SPropN' (Su N3)++-- > *TypeFN> :t test_spn4+-- > test_spn4 :: Bool -> Bool -> Bool -> Bool -> Bool -> Bool++-- | 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+instance A (F Flip) f (F (Flip,f))+instance A (F (Flip,f)) x (F (Flip,f,x))+instance E (f :< y :< x) r => A (F (Flip,f,x)) y r++-- | we make a very little change+--+type SSPropN' n = E(F Ntimes :< (F Flip :< (F (ATC2 (->))) :< Bool) :< Bool+                             :< (F Fib :< n)) r => r+test_sspn4 = undefined::SSPropN' (Su N3)++-- | 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] deriving (Read, Show)+type TreeDN v l n = E(F Ntimes :< (F (ATC1 (Node v))) :< l :< n) r => r+instance E (Node v els) (Node v els)++read_tree3 s = (read s) `asTypeOf` (undefined:: TreeDN Int String N3)++-- > *TypeFN> :t read_tree3+-- > read_tree3 :: String -> Node Int (Node Int (Node Int String))+++-- | The ability of computed types to drive the selection of overloaded+-- functions has wider implications. We can remove the need for+-- functional dependencies, or simulate functional dependencies when they+-- cannot apply. For example, one may define a multi-parameter typeclass+-- but cannot assert functional dependencies, because not all instances+-- satisfy them.  Therefore, using the methods of the class may require+-- complex and annoying type annotations. Computed types remove the need+-- to manually write these annotations; the typechecker can compute them+-- itself.  This subject is to be explored further.+-- +-- The last example showed computations of polymorphic types, which,+-- unsurprisingly, have the form of type abstractions. Our calculus is+-- built around the deep connection between type+-- abstraction/instantiation and functional abstraction/application.+ttree3_1 = read_tree3 "Node 1 [Node 2 []]"+ttree3_2 = read_tree3 "Node 1 [Node 2 [Node 3 [\"ok\"]]]"+ttree3_3 = read_tree3 "Node 0 [Node 1 [Node 2 [Node 3 [\"ok\"]]]]"++-- > *TypeFN> ttree3_2+-- > Node 1 [Node 2 [Node 3 ["ok"]]]+-- > *TypeFN> ttree3_3+-- > *** Exception: Prelude.read: no parse++

@@ -0,0 +1,258 @@+-- +-- |+-- <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 :<).+-- ++{-# LANGUAGE TypeOperators, ScopedTypeVariables, EmptyDataDecls, Rank2Types #-}+{-# LANGUAGE FlexibleContexts, FlexibleInstances, ScopedTypeVariables  #-}+{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies #-}+{-# LANGUAGE UndecidableInstances #-}+module Language.TypeLC where++-- | First we define some constants+data HTrue  = HTrue+data HFalse = HFalse++data Zero = Zero+data Su a = Su a++-- | Indicator for functions, or applicable things:+data F x++-- and the applicator+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++-- | by case analysis:+instance A (F FNot) HTrue  HFalse+instance A (F FNot) HFalse HTrue++-- | The next function is the boolean And. It takes two arguments, so we+-- have to handle currying now.+--+data FAnd++-- | Applying And to an argument makes a closure, waiting for the second+-- argument.+instance A (F FAnd) x (F (FAnd,x))++-- | When we receive the second argument, we are in the position to produce+-- the result. Again, we use the case analysis.+--+instance A (F (FAnd,HTrue))  a  a+instance A (F (FAnd,HFalse)) a  HFalse++-- | 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+infixl 1 :<++-- | and the big-step evaluation function:+--+class E a b | a -> b++-- | Constants evaluate to themselves+--+instance E HTrue HTrue+instance E HFalse HFalse+instance E Zero Zero++-- | Abstractions are values and so evaluate to themselves+--+instance E (F x) (F x)++-- | Familiar rules for applications+--+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++-- | Other particular rules+--+instance E x x' => E (Su x) (Su x')++-- | 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+testb1_t = undefined :: Testb HTrue+testb1_f = undefined :: Testb HFalse+++-- | We introduce the applicative fixpoint combinator+--+data Rec l+instance E (l :< (F (Rec l)) :< x) r => A (F (Rec l)) x r+++-- | and define the sum of two numerals+--+fix f = f (fix f)+vsum = fix (\self n m -> case n of 0 -> m+                                   (n+1) -> 1 + (self n m))++-- | At the type level, this looks as follows+data FSum'            -- first define the non-recursive function++instance A (F FSum') self (F (FSum',self))+instance A (F (FSum',self)) n (F (FSum',self,n)) -- build closures+instance A (F (FSum',self,Zero)) m m+instance E (self :< n :< m) r => A (F (FSum',self,(Su n))) m (Su r)++-- | now we tie up the knot+type FSum  = Rec (F FSum')   ++-- After we define a few sample numerals, we can add them++type N0 = Zero; type N1 = Su N0; type N2 = Su N1; type N3 = Su N2+(n0::N0, n1::N1, n2::N2, n3::N3) = undefined++test_sum :: E (F FSum :< x :< y) r => x -> y -> r+test_sum = undefined++test_sum_2_3 = test_sum n2 n3++--  *TypeLC> :t test_sum_2_3+--  test_sum_2_3 :: Su (Su (Su (Su (Su Zero))))+++-- | Finally, the standard test -- Fibonacci++vfib = fix(\self n -> case n of 0 -> 1+                                1 -> 1+                                (n+2) -> (self n) + (self (n+1)))+++data Fib'++instance A (F Fib') self (F (Fib',self))    -- build closure+instance A (F (Fib',self)) Zero (Su Zero)+instance A (F (Fib',self)) (Su Zero) (Su Zero)+instance E (F FSum :< (self :< n) :< (self :< (Su n))) r +     => A (F (Fib',self)) (Su (Su n)) r+++type Fib  = Rec (F Fib')+test_fib :: E (F Fib :< n) r => n -> r+test_fib = undefined++test_fib_5 = test_fib (test_sum n3 n2)+++-- | Finally, we demonstrate that our calculus is combinatorially complete,+-- by writing the S and K combinators+--+data CombK+instance A (F CombK) a (F (CombK,a))+instance A (F (CombK,a)) b a++data CombS+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++-- | A few examples: SKK as the identity+--+type Test_skk x = E (F CombS :< F CombK :< F CombK :< x) r => r+test_skk1 = undefined:: Test_skk HTrue++-- | 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+test_ctwo = undefined+++-- | We define the instances of Show to be able to show things. We define+-- the instances in a way that the value is not required.++instance Show HTrue  where show _ = "HTrue"+instance Show HFalse where show _ = "HFalse"+class Nat a where fromNat :: a -> Integer+instance Nat Zero where fromNat _ = 0+instance Nat x => Nat (Su x) where fromNat _ = succ (fromNat (undefined::x))+instance Show Zero  where show _ = "N0"+instance Nat x => Show (Su x) where+    show x = "N" ++ (show (fromNat x))++

@@ -1,5 +1,5 @@ name:           liboleg-version:        0.1+version:        0.1.0.1 license:        BSD3 license-file:   LICENSE author:         Oleg Kiselyov@@ -14,17 +14,18 @@  library     build-depends:-            base, containers+            base, containers, mtl      exposed-modules:             Data.FDList++            Control.CaughtMonadIO++            Language.TypeLC+            Language.TypeFN+             Text.PrintScan             Text.PrintScanF-------    extensions:         ---            GADTs---      ghc-options:             -funbox-strict-fields