* Am 23.04.07 schrieb Claus Reinke:
[..]
> i already was a fan of Wadler's list of successes trick, but did not yet know about
> monads, there's no discussion of separating effects by types, only fragments of
Compared to nowadays where monads are the mullet of functional
programming, it must have been exciting times when Wadler initiated this
volta of taking a means to localize effects in program semantics as a
device to structure effectful programs.
By the way, Curry doesn't impose a downcase-convention on identifiers.
So you can give your monad a look pretty similar to conventional
category theory notation.
data T a
T :: (a -> b) -> T a -> T b
T = unknown
type Id a = a
-- unit
eta{- a -} :: Id a -> T a
eta{- a -} = unknown
type TT a = T(T a)
-- multiplication
mu{- a -} :: TT a -> T a
mu{- a -} = unknown
-- unit laws
-- mu . etaT = id = mu . Teta
etaT{- a -} :: Id(T a) -> T(T a)
etaT{- a -} = eta{- T a -}
Teta{- a -} :: T(Id a) -> T(T a)
Teta{- a -} = T eta{- a -}
-- associativity
-- mu . muT = mu . Tmu
muT{- a -} :: TT(T a) -> T(T a)
muT{- a -} = mu{- T a -}
Tmu{- a -} :: T(TT a) -> T(T a)
Tmu{- a -} = T mu{- a -}
Conor McBride uses those 'inlined' multiline comments to show how the
target type of primitive recursion get's instantiated in the higher
order case.
Thought this might be useful too to explain the natural transformations
that arise from composing the functor T with the natural transformations eta
and mu.
Best regards,
Sebastian
_______________________________________________
curry mailing list
curry_at_lists.RWTH-Aachen.DE
http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry
Received on Di Apr 24 2007 - 09:56:57 CEST