Re: New PAKCS release (Version 1.8.0)

From: Sebastian Hanowski <seha_at_informatik.uni-kiel.de>
Date: Tue, 24 Apr 2007 07:33:22 +0200

* 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

This archive was generated by hypermail 2.3.0 : Do Jun 20 2024 - 07:15:08 CEST