From: Sebastian Hanowski <>
Date: Fri, 27 Oct 2017 07:37:09 +0200


 When I began to exploit narrowing for hiding constructors in infinite list=
s I
needed to be able to unify them lazily.

Earlier definitions I gave just looked too involved. Only recently I found a
neater way to do this.

        (~=) = zipWith (=:=)

        (x:xs) `given` (p:ps) | p = x : (xs `given` ps)

        fibs | head xs =:= 1
             & head (tail xs) =:= 1 = xs `given` (tail (tail xs) ~==
 zipWith (+) xs (tail xs))

             where xs free

 This also carries over to giving your program as a specification in terms =
the "interface" of infinite lists in message passing style.

        infixr 0 `and`

        xs `and` ys = xs `given` (xs ~= ys) =

        proj `is` img = emb img where emb (proj preimg) = preimg

        fibs = head `is` 1
               (head . tail) `is` 1
               (tail . tail) `is` zipWith (+) fibs (tail fibs)

 Monads where introduced to computer science to give semantics to effectful
programs. On paper. Only later they were used as a device to structure
effectful programs.

Can we do the same to bisimulations?

Instead of proving properties of our programs, why not express them directl=
y in
terms of the desired properties?

Have a nice weekend,

curry mailing list
Received on Fr Okt 27 2017 - 09:49:19 CEST

This archive was generated by hypermail 2.3.0 : Di Dez 05 2023 - 07:15:14 CET