# minor update on infinite data + free variables

From: Sebastian Hanowski <sebastian_hanowski_at_gmx.de>
Date: Mon, 22 Feb 2016 07:21:01 +0100

In my attempt write 'negative' versions of stream generating programs, I
overenthusiastically leveraged an unsafe language primitive.

fib | head xs =:= 1
& head (tail xs) =:= 1
& tail (tail xs) =:<= zipWith (+) xs (tail xs) = xs
where xs free

Trying to improve on this I used the language feature which is built on
top of this primitive.

We're used to gain access to *smaller* parts of input to programs
defined with function patterns.

However when matching on function patterns which *shrink* their
arguments, we actually get our variables grown into unspecified context

fibaux (tail (tail xs)) | head xs =:= 1
& head (tail xs) =:= 1 = xs

fib' = xs
where
xs = fibaux (zipWith (+) xs (tail xs))

Making this explicit can prove valueable.

push a = a : _
shift t = _ : t

Now here's my attempt to get as close as possible to my original
equations using hopefully less controversal means only.

Given 'equalizers'

a =?= b | a =:= b = a
(a:as) =??= (b:bs) = a =?= b : as =??= bs

we can fit together our partially defined data structures like pieces of
a puzzle.

fib'' = (push 1
=??=
shift (push 1)
=??=
shift (shift (zipWith (+) xs (tail xs))))
=??= xs
where xs free

Factoring out the noise of pushing and shifting into an operator and
inlining identities we arrive at this:

fib''' = (head xs =?= 1
&= head (tail xs) =?= 1
&= tail (tail xs) =??= zipWith (+) xs (tail xs)) =??= xs
where xs free

I better confess right now that I've really just reintroduced 'cons'.

infixr 5 &=
h &= t = push h
=??=
shift t

At least my desired equations are expressible and do get solved.

But unfortunately I have to exhibit the structure of the stream albeit
'overlayed' with those equations which suffice to define it in the first
place.
Narrowing head and tail should be enough to build the data structure.

Anyway if you unintendedly arrive from where you started, at least
sometimes you've brought something new home with you.

For example here's a small fixpoint operator for stream functions

fix f = s =??= f s
where s free

working well also for classic formulations with constructor forms.

fix (\s -> 1:1:zipWith (+) s (tail s))

Happy streaming

Sebastian
_______________________________________________
curry mailing list
curry_at_lists.RWTH-Aachen.DE
http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry

Received on Di Feb 23 2016 - 15:50:59 CET

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