StackOverflow2013

Note that there are some explanatory texts on larger screens.

plurals

PO
text
Body
copied!<p>Not sure if this is exactly what you want, but here is an implementation that enforces the correct number of steps and requires there to be zero steps left at the end. For simplicity, I'm using a monad instead of a monad transformer over IO. Note that I am not using the Prelude monad to do what I'm doing.</p> <p><strong>UPDATE</strong>:</p> <p>Now can extract the number of remaining steps. Run the following with -XRebindableSyntax</p> <pre><code>{-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE FunctionalDependencies #-} module Test where import Prelude hiding (Monad(..)) import qualified Prelude as Old (Monad(..)) ----------------------------------------------------------- data Z = Z data S n = S type Zero = Z type One = S Zero type Two = S One type Three = S Two type Four = S Three ----------------------------------------------------------- class Peano n where peano :: n fromPeano :: n -> Integer instance Peano Z where peano = Z fromPeano Z = 0 instance Peano (S Z) where peano = S fromPeano S = 1 instance Peano (S n) => Peano (S (S n)) where peano = S fromPeano s = n `seq` (n + 1) where prev :: S (S n) -> (S n) prev S = S n = fromPeano $ prev s ----------------------------------------------------------- class (Peano s, Peano p) => Succ s p | s -> p where instance Succ (S Z) Z where instance Succ (S n) n => Succ (S (S n)) (S n) where ----------------------------------------------------------- infixl 1 >>=, >> class ParameterisedMonad m where return :: a -> m s s a (>>=) :: m s1 s2 t -> (t -> m s2 s3 a) -> m s1 s3 a fail :: String -> m s1 s2 a fail = error (>>) :: ParameterisedMonad m => m s1 s2 t -> m s2 s3 a -> m s1 s3 a x >> f = x >>= \_ -> f ----------------------------------------------------------- newtype PIO p q a = PIO { runPIO :: IO a } instance ParameterisedMonad PIO where return = PIO . Old.return PIO io >>= f = PIO $ (Old.>>=) io $ runPIO . f ----------------------------------------------------------- data Progress p n a = Progress a instance ParameterisedMonad Progress where return = Progress Progress x >>= f = let Progress y = f x in Progress y runProgress :: Peano n => n -> Progress n Zero a -> a runProgress _ (Progress x) = x runProgress' :: Progress p Zero a -> a runProgress' (Progress x) = x task :: Peano n => n -> Progress n n () task _ = return () task' :: Peano n => Progress n n () task' = task peano step :: Succ s n => Progress s n () step = Progress () stepsLeft :: Peano s2 => Progress s1 s2 a -> (a -> Integer -> Progress s2 s3 b) -> Progress s1 s3 b stepsLeft prog f = prog >>= flip f (fromPeano $ getPeano prog) where getPeano :: Peano n => Progress s n a -> n getPeano prog = peano procedure1 :: Progress Three Zero String procedure1 = do task' step task (peano :: Two) -- any other Peano is a type error --step -- uncommenting this is a type error step -- commenting this is a type error step return "hello" procedure2 :: (Succ two one, Succ one zero) => Progress two zero Integer procedure2 = do task' step `stepsLeft` \_ n -> do step return n main :: IO () main = runPIO $ do PIO $ putStrLn $ runProgress' procedure1 PIO $ print $ runProgress (peano :: Four) $ do n <- procedure2 n' <- procedure2 return (n, n') </code></pre>

Querying!

Guidance

An individual column

Larger individual text columns get their own page to allow for proper reading.

SQuiL has stopped working due to an internal error.

If you are curious you may find further information in the browser console, which is accessible through the devtools (F12).

Reload