Re: New PAKCS release (Version 1.8.0)

From: Sebastian Hanowski <seha_at_informatik.uni-kiel.de>
Date: Mon, 02 Apr 2007 17:16:57 +0200

* Am 30.03.07 schrieb Emilio Jesús Gallego Arias:
> Hi Sebastian,
>
> Sebastian Hanowski <seha_at_informatik.uni-kiel.de> writes:
>
> > looks like you're essentially aiming at a monadic semantics of
> > non-determnism.
> > The above equation could also be formulated like this
> >
> > [(x,x) | x <- coin] == uncurry zip (coin,coin)
> >
> > However, using the list monad to model non-determnism seems to have
> > never been appreciated much by the FLP community because disjunction
> > realized as concatenation is biased.
>
> Right. Could you provide me more details about what do you think the
> bias is?

Expressing choice by appending lists leads to backtracking which is
incomplete in presence of infinite paths. Like 0 will never be
considered here:

                [1..] ++ [0]

> By the way, I'm not very confident that using monads is the way to,
> but I want to play with them nevertheless, to see what kind of Curry
> one get. I know of some papers who have attempted this, and certainly
> the result was cool.

Structuring non-deterministic computations with a monad certainly has it's
advantages.
But besides functional programming FLP seems to have strong roots in term
rewriting and logic programming. Which could speak against seeing
non-determinism as a mere effect in otherwise purely functional
programs.

Which is not to say that monads aren't useful too when taking FL
programs as algebraic theories. For example given a signature as a functorial
datatype

        data Sig a = Leaf | Branch a a
        Sig :: (a -> b) -> Sig a -> Sig b
        Sig _ Leaf = Leaf
        Sig f (Branch l r) = Branch (f l) (f r)

one gets the type of terms from this signature built over a set of variables x

        data TermSig x = Var x | Con (Sig (TermSig x))
        TermSig :: (a -> b) -> TermSig a -> TermSig b
        TermSig f (Var x) = Var (f x)
        TermSig f (Con t) = Con (Sig (TermSig f) t)

which is a monad with the Var constructor embedding values

        return :: x -> TermSig x
        return = Var
        
and substitution beeing the bind operation

        (>>=) :: TermSig x -> (x -> TermSig y) -> TermSig y
        (Var x) >>= f = f x
        (Con t) >>= f = Con (Sig (>>= f) t)


Best regards,
Sebastian

_______________________________________________
curry mailing list
curry_at_lists.RWTH-Aachen.DE
http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry
Received on Mi Apr 11 2007 - 11:56:46 CEST

This archive was generated by hypermail 2.3.0 : Fr Mär 29 2024 - 07:15:08 CET