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)