lazy-lambda-calculus: f98beed07dc86947cf281bef3f013fd923be22bd
1: {-# Language FlexibleInstances #-}
2: {-# Language MultiParamTypeClasses #-}
3: {-# Language FlexibleContexts #-}
4: {-# Language ExistentialQuantification #-}
5: {-# Language DeriveDataTypeable #-}
6:
7: module Control.Monad.Partial where
8:
9: import Control.Monad
10: import qualified Control.Monad.Fail as Fail
11: import Control.Monad.Fix
12: import Data.Data
13: import Data.Maybe
14: import Data.Nat
15: import Data.Typeable
16: import Test.LazySmallCheck2012 hiding (Nat, Term, Const)
17: import Test.LazySmallCheck2012.Core hiding (Term, C)
18:
19: -- Partial results are either a value (Now) or a partial result (Later).
20: data Partial a = Now a
21: | Later (Partial a)
22: deriving (Show, Eq, Typeable, Data)
23:
24: -- Delay mapping until we have a result (if ever).
25: instance Functor Partial where
26: fmap f (Now x) = Now (f x)
27: fmap f (Later x) = Later (fmap f x)
28:
29: -- Delay applications until we have a function (if ever)
30: instance Applicative Partial where
31: pure = Now
32: (Now f) <*> x = f <$> x
33: (Later f) <*> x = Later (f <*> x)
34:
35: -- Compose functions once the first one halts (if ever)
36: instance Monad Partial where
37: return = Now
38: (Now x) >>= f = f x
39: (Later x) >>= f = Later (x >>= f)
40:
41: -- Backwards compatibility
42: fail = Fail.fail
43:
44: -- Failure (e.g. a failed pattern-match) is an infinite loop
45: instance Fail.MonadFail Partial where
46: fail _ = fix Later
47:
48: -- Choose between values by picking whichever halts first. This is like the
49: -- 'min' function on Nat, and hence associative; likewise infinite loops are the
50: -- identity. If it's a tie, the first argument is returned (arbitrarily), which
51: -- breaks commutativity.
52: instance Alternative Partial where
53: empty = Fail.fail "empty"
54: Now x <|> _ = Now x
55: _ <|> Now y = Now y
56: Later x <|> Later y = Later (x <|> y)
57:
58: -- Inherit mzero and mplus from Alternative
59: instance MonadPlus Partial where
60:
61: -- Generate arbitrary delayed values
62: instance Serial a => Serial (Partial a) where
63: series = cons1 Now \/ cons1 Later
64:
65: -- See if we have a result yet
66: finished (Now _) = True
67: finished _ = False
68:
69: laterCount (Now _) = 0
70: laterCount (Later x) = S (laterCount x)
71:
72: -- Give a computation N steps to halt
73: force :: Nat -> Partial a -> Maybe a
74: force 0 _ = Nothing
75: force n (Now x) = Just x
76: force n (Later x) = force (n-1) x
77:
78: -- Conservative decision procedure
79: trueIn n x = fromMaybe False (force n x)
80:
81: -- Lax decision procedure
82: notFalseIn n x = fromMaybe True (force n x)
83:
84: cast' :: (Typeable a, Typeable b) => a -> Partial b
85: cast' x = fromMaybe mzero (cast x)
Generated by git2html.