Re: Curry-on to infinity

From: Sebastian Hanowski <sebastian_hanowski_at_gmx.de>
Date: Mon, 21 Dec 2015 19:40:58 +0100


Dear Sergio


please let me try to convince you that we both agree on this subject.

On Mon, Dec 21, 2015 at 09:36:01AM -0800, h7sa_at_pdx.edu wrote:
> The constructors are hidden by tail and head.

This is my point too. I started to fancy Curry for allowing me to leave out
constructors because of the narrowing behaviour of the projections.
And that lazy equality constraints give just enough freedom to use this at
infinite data allowing to give behavioral specifications.

> Let me introduce a new function, cons, which also hides the constructors.
> These functions are related by
>
> head (cons x xs) = x
> tail (cons x xs) = xs

This view is shared by the second point of my original post. You can
reintroduce pattern matching for 'unseen' data by function patterns.
But I only used this style for the definition of the auxiliary zipWith.

        module Stream(Stream,(>:)) where

        data Stream a = SCons a (Stream a)

        infix r 5
        (>:) :: a -> Stream a -> Stream a
        a >: as = SCons a as

    snip X< ------

        import Stream

        sHead :: Stream a -> a
        sHead (a>:_) = a

        sTail :: Stream a -> Stream a
        sTail (_>:as) = as

        sZipWith :: (a -> b -> c) -> Stream a -> Stream b -> Stream c
        sZipWith f (a>:as) (b>:bs) = f a b >: sZipWith f as bs


Thank you for the elegant derivation which I wasn't capable of
doing but which would have made my point clear by time.


Best regards

Sebastian

> Now I recode fibmatch as
>
> fibmatch xs = cons _ (cons _ xs)
>
> which gives
>
> fib | head xs =:= 1
> & head (tail xs) =:= 1 = xs
> where
> xs = cons _ (cons _ (zipWith (+) xs (tail xs)))
>
> now satisfy the conditions on xs
>
> fib = xs
> where
> xs = cons 1 (cons 1 (zipWith (+) xs (tail xs)))
>
> now eliminate the renaming
>
> fib = cons 1 (cons 1 (zipWith (+) fib (tail fib)))
>
> On Mon, 21 Dec 2015, at 09:15, Sebastian Hanowski <sebastian_hanowski_at_gmx.de> wrote:
>
> > On Tue, Dec 15, 2015 at 03:44:34PM +0100, Michael Hanus wrote:
> > [...]
> > > Hence, the challenge is open...
> >
> > This is my last resort:
> >
> > fibmatch (tail (tail xs)) = xs
> >
> > fib | head xs =:= 1
> > & head (tail xs) =:= 1 = xs
> > where
> > xs = fibmatch (zipWith (+) xs (tail xs))
> >
> > No non-linear patterns. No (=:<=). And no constructors.
> >
> > But unfortunately it features too much cyclicity which I had liked to avoid.
> >
> > Think it's time now for a principled retreat.
> >
> >
> > Best regards
> >
> > Sebastian
_______________________________________________
curry mailing list
curry_at_lists.RWTH-Aachen.DE
http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry

Received on Mo Dez 21 2015 - 23:31:22 CET

This archive was generated by hypermail 2.3.0 : Do Feb 01 2024 - 07:15:12 CET