erin/UniqueState.icl

   1 implementation module UniqueState
   2
   3 import StdEnv
   4
   5 runState :: u:(State .s .a) .s -> v:(.a,.s), [u <= v]
   6 runState (State f) s = f s
   7
   8 instance Functor (State String)
   9 where
  10         //fmap :: u:(v:a -> w:b) x:(State String v:a) -> x:(State String w:b), [x <= u,x <= v,x <= w]
  11         fmap f a = State (\s
  12                 # (a`, s`) = runState a s
  13                 = (f a`, s`))
  14
  15 instance Applicative (State String)
  16 where
  17         //(<*>) infixl 4 :: u:(State String v:(w:a -> x:b)) y:(State String w:a) -> z:(State String x:b), [z <= u,u <= v,y <= w,z <= x,z <= y]
  18         (<*>) f a = State (\s
  19                 # (f`, s`) = runState f s
  20                 # (a`, s``) = runState a s`
  21                 = (f` a`, s``))
  22
  23         //pure :: u:a -> v:(State String u:a), [v <= u]
  24         pure x = State (\s -> (x, s))
  25
  26 instance Monad (State String)
  27 where
  28         //bind :: u:(State String v:a) w:(v:a -> x:(State String y:b)) -> x:(State String y:b), [x <= u,u <= v,x <= w,x <= y]
  29         bind a f = State (\s
  30                 # (v, s`) = runState a s
  31                 # a` = f v
  32                 = runState a` s`)
  33
  34 instance Functor Maybe
  35 where
  36         fmap f (Just x) = Just (f x)
  37         fmap _ _ = Nothing
  38
  39 instance Applicative Maybe
  40 where
  41         (<*>) (Just f) (Just x) = Just (f x)
  42         (<*>) _ _ = Nothing
  43
  44         pure x = Just x
  45
  46 instance Monad Maybe
  47 where
  48         bind (Just x) f = f x
  49         bind _ _ = Nothing