diff --git a/Control/CaughtMonadIO.hs b/Control/CaughtMonadIO.hs new file mode 100644 --- /dev/null +++ b/Control/CaughtMonadIO.hs @@ -0,0 +1,118 @@ +-- +-- | +-- +-- +-- The ability to use functions 'catch', 'bracket', 'catchDyn', etc. in +-- MonadIO other than IO itself has been a fairly frequently requested +-- feature: +-- +-- +-- +-- < 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)) + diff --git a/Language/TypeFN.hs b/Language/TypeFN.hs new file mode 100644 --- /dev/null +++ b/Language/TypeFN.hs @@ -0,0 +1,208 @@ +-- +-- | +-- +-- +-- +-- 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'' +-- +-- and by Simon Peyton Jones and Erik Meijer's ``Henk: A Typed +-- Intermediate Language'' +-- +-- 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 + + diff --git a/Language/TypeLC.hs b/Language/TypeLC.hs new file mode 100644 --- /dev/null +++ b/Language/TypeLC.hs @@ -0,0 +1,258 @@ +-- +-- | +-- +-- +-- 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: +-- +-- +-- +-- 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)) + + diff --git a/liboleg.cabal b/liboleg.cabal --- a/liboleg.cabal +++ b/liboleg.cabal @@ -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