erin/UniqueState.dcl

   1 definition module UniqueState
   2
   3 :: Maybe a = Just a | Nothing
   4
   5 class Functor f
   6 where
   7         fmap :: u:(v:a -> w:b) *(f v:a) -> *(f w:b)
   8
   9 class Applicative f | Functor f
  10 where
  11         (<*>) infixl 4 :: *(f v:(w:a -> x:b)) *(f w:a) -> *(f x:b)
  12         pure :: u:a -> *(f u:a)
  13
  14 class Monad m | Applicative m
  15 where
  16         bind :: *(m v:b) w:(v:b -> *(m x:c)) -> *(m x:c)
  17         (>>=) infixl 1 :: *(m v:b) w:(v:b -> *(m x:c)) -> *(m x:c)
  18         (>>=) ma a2mb :== bind ma a2mb
  19         (>>|) infixl 1 :: *(m v:b) w:(v:b -> *(m x:c)) -> *(m x:c)
  20         (>>|) ma mb :== ma >>= \_ -> mb
  21         return :: u:a -> *(m u:a) | Applicative m
  22         return x :== pure x
  23
  24 :: State s a = State .(s -> .(a, s))
  25
  26 runState :: u:(State .s .a) .s -> v:(.a,.s), [u <= v]
  27
  28 instance Functor (State String)
  29 instance Applicative (State String)
  30 instance Monad (State String)
  31
  32 instance Functor Maybe
  33 instance Applicative Maybe
  34 instance Monad Maybe