Free theorem for `forall z. (A,z) -> (B,z)`?

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
9 messages Options
Reply | Threaded
Open this post in threaded view
|

Free theorem for `forall z. (A,z) -> (B,z)`?

Conal Elliott
Suppose `g :: forall z. (A,z) -> (B,z)`. Is it necessarily the case that `g = first f` for some `f :: A -> B` (where `first f (a,b) = (f a, b)`), perhaps as a free theorem for the type of `g`?

Note that `(A,)` and `(B,)` are functors and that `g` is a natural transformation, so `g . fmap h == fmap h . g` for any `h :: u -> v`.
Equivalently, `g . second h == second h . g` (where `second h (a,b) = (a, h b)`).

Thanks,  -- Conal

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Free theorem for `forall z. (A,z) -> (B,z)`?

Joachim Breitner-2
Hi Conal,

Am Sonntag, den 22.07.2018, 21:29 -0700 schrieb Conal Elliott:
> Suppose `g :: forall z. (A,z) -> (B,z)`. Is it necessarily the case
> that `g = first f` for some `f :: A -> B` (where `first f (a,b) = (f
> a, b)`), perhaps as a free theorem for the type of `g`?

there used to be a free theorem calculator at
http://www-ps.iai.uni-bonn.de/ft
but it seems to be down :-(

There is a shell client, ftshell, lets see what it says…
it does not build with ghc-8.0 any more :-(

Ah, but lambdabot understands @free:

<nomeata>   @free g :: forall z. (A,z) -> (B,z)
<lambdabot> $map_Pair $id f . g = g . $map_Pair $id f

Which is basically what you are writing here:

> Note that `(A,)` and `(B,)` are functors and that `g` is a natural
> transformation, so `g . fmap h == fmap h . g` for any `h :: u -> v`.
> Equivalently, `g . second h == second h . g` (where `second h (a,b) =
> (a, h b)`).

Doesn’t that already answer the question? Let’s try to make it more
rigorous. I define

f :: A -> B
f a = fst (g (a, ())

and now want to prove that g = first f, using the free theorem… which
is tricky, because the free theorem is actually not as strong as it
could be; it should actually be phrased in terms of relations relation,
which might help with the proof.

So let me try to calculate the free theorem by hand, following
https://www.well-typed.com/blog/2015/05/parametricity/

g is related to itself by the relation

   [forall z. (A,z) -> (B,z)]

and we can calculate

  g [forall z. (A,z) -> (B,z)] g
↔ ∀ z z' Rz, g [(A,z) -> (B,z)] g -- Rz relates z and z'
↔ ∀ z z' Rz, ∀ p p', p [(A,z)] p' → g p [(B,z)] g p'
↔ ∀ z z' Rz, ∀ p p', fst p = fst p' ∧ snd p Rz snd p' →
      fst (g p) = fst (g p') ∧ snd (g p) Rz snd (g p')
↔ ∀ z z' Rz, ∀ a x x', x Rz x' →
      fst (g (a,x)) = fst (g (a,x')) ∧
snd (g (a,x)) Rz snd (g (a,x'))

We can use this to show
 
   ∀ (a,x :: z). fst (g (a,x)) = f a

using (this is the tricky part that requires thinking)

   z := z, z' := (), Rz := λ_ _ -> True, a := a, x := x, x' := ()

as then the theorem implies

  fst (g (a,x)) = fst (g (a, ()) = f a.

We can also use it to show

   ∀ (a,x :: z). snd (g (a,x)) = x

using

   z := z, z' := z, Rz := const (= x), a := a, x := x, x' := x

as then the theorem implies, under the true assumption  x Rz z'

  (snd (g (a,x))) Rz (snd (g (a,x')))
  ↔ snd (g (a,x)) = x

And from

   ∀ (a,x :: z). fst (g (a,x)) = f a
   ∀ (a,x :: z). snd (g (a,x)) = x

we can conclude that

  g = first f

as intended.

Cheers,
Joachim



--
Joachim Breitner
  [hidden email]
  http://www.joachim-breitner.de/

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.

signature.asc (849 bytes) Download Attachment
Reply | Threaded
Open this post in threaded view
|

Re: Free theorem for `forall z. (A,z) -> (B,z)`?

Conal Elliott
Thank you, Joachim! I'm refreshing my memory of free theorem construction from that blog post. Regards, -- Conal

On Mon, Jul 23, 2018 at 8:33 AM, Joachim Breitner <[hidden email]> wrote:
Hi Conal,

Am Sonntag, den 22.07.2018, 21:29 -0700 schrieb Conal Elliott:
> Suppose `g :: forall z. (A,z) -> (B,z)`. Is it necessarily the case
> that `g = first f` for some `f :: A -> B` (where `first f (a,b) = (f
> a, b)`), perhaps as a free theorem for the type of `g`?

there used to be a free theorem calculator at
http://www-ps.iai.uni-bonn.de/ft
but it seems to be down :-(

There is a shell client, ftshell, lets see what it says…
it does not build with ghc-8.0 any more :-(

Ah, but lambdabot understands @free:

<nomeata>   @free g :: forall z. (A,z) -> (B,z)
<lambdabot> $map_Pair $id f . g = g . $map_Pair $id f

Which is basically what you are writing here:

> Note that `(A,)` and `(B,)` are functors and that `g` is a natural
> transformation, so `g . fmap h == fmap h . g` for any `h :: u -> v`.
> Equivalently, `g . second h == second h . g` (where `second h (a,b) =
> (a, h b)`).

Doesn’t that already answer the question? Let’s try to make it more
rigorous. I define

f :: A -> B
f a = fst (g (a, ())

and now want to prove that g = first f, using the free theorem… which
is tricky, because the free theorem is actually not as strong as it
could be; it should actually be phrased in terms of relations relation,
which might help with the proof.

So let me try to calculate the free theorem by hand, following
https://www.well-typed.com/blog/2015/05/parametricity/

g is related to itself by the relation

   [forall z. (A,z) -> (B,z)]

and we can calculate

  g [forall z. (A,z) -> (B,z)] g
↔ ∀ z z' Rz, g [(A,z) -> (B,z)] g -- Rz relates z and z'
↔ ∀ z z' Rz, ∀ p p', p [(A,z)] p' → g p [(B,z)] g p'
↔ ∀ z z' Rz, ∀ p p', fst p = fst p' ∧ snd p Rz snd p' →
      fst (g p) = fst (g p') ∧ snd (g p) Rz snd (g p')
↔ ∀ z z' Rz, ∀ a x x', x Rz x' →
      fst (g (a,x)) = fst (g (a,x')) ∧
snd (g (a,x)) Rz snd (g (a,x'))

We can use this to show

   ∀ (a,x :: z). fst (g (a,x)) = f a

using (this is the tricky part that requires thinking)

   z := z, z' := (), Rz := λ_ _ -> True, a := a, x := x, x' := ()

as then the theorem implies

  fst (g (a,x)) = fst (g (a, ()) = f a.

We can also use it to show

   ∀ (a,x :: z). snd (g (a,x)) = x

using

   z := z, z' := z, Rz := const (= x), a := a, x := x, x' := x

as then the theorem implies, under the true assumption  x Rz z'

  (snd (g (a,x))) Rz (snd (g (a,x')))
  ↔ snd (g (a,x)) = x

And from

   ∀ (a,x :: z). fst (g (a,x)) = f a
   ∀ (a,x :: z). snd (g (a,x)) = x

we can conclude that

  g = first f

as intended.

Cheers,
Joachim



--
Joachim Breitner
  [hidden email]
  http://www.joachim-breitner.de/


_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Free theorem for `forall z. (A,z) -> (B,z)`?

Joachim Breitner-2
Hi,

I felt inspired to revive the free theorem calculator and gave it a new
home (and a modern, browser-only, FRP-based implementation):

http://free-theorems.nomeata.de/

which prints

   forall t1,t2 in TYPES, R in REL(t1,t2).
    forall (x, y) in lift{(,)}(id,R).
     (g_{t1} x, g_{t2} y) in lift{(,)}(id,R)

as the free theorem, which is (if one squints) the same as my

  ∀ z z' Rz, ∀ a x x', x Rz x' →
      fst (g (a,x)) = fst (g (a,x')) ∧ snd (g (a,x)) Rz snd (g (a,x'))

Enjoy,
Joachim

Am Montag, den 23.07.2018, 10:56 -0700 schrieb Conal Elliott:

> Thank you, Joachim! I'm refreshing my memory of free theorem construction from that blog post. Regards, -- Conal
>
> On Mon, Jul 23, 2018 at 8:33 AM, Joachim Breitner <[hidden email]> wrote:
> > Hi Conal,
> >
> > Am Sonntag, den 22.07.2018, 21:29 -0700 schrieb Conal Elliott:
> > > Suppose `g :: forall z. (A,z) -> (B,z)`. Is it necessarily the case
> > > that `g = first f` for some `f :: A -> B` (where `first f (a,b) = (f
> > > a, b)`), perhaps as a free theorem for the type of `g`?
> >
> > there used to be a free theorem calculator at
> > http://www-ps.iai.uni-bonn.de/ft
> > but it seems to be down :-(
> >
> > There is a shell client, ftshell, lets see what it says…
> > it does not build with ghc-8.0 any more :-(
> >
> > Ah, but lambdabot understands @free:
> >
> > <nomeata>   @free g :: forall z. (A,z) -> (B,z)
> > <lambdabot> $map_Pair $id f . g = g . $map_Pair $id f
> >
> > Which is basically what you are writing here:
> >
> > > Note that `(A,)` and `(B,)` are functors and that `g` is a natural
> > > transformation, so `g . fmap h == fmap h . g` for any `h :: u -> v`.
> > > Equivalently, `g . second h == second h . g` (where `second h (a,b) =
> > > (a, h b)`).
> >
> > Doesn’t that already answer the question? Let’s try to make it more
> > rigorous. I define
> >
> > f :: A -> B
> > f a = fst (g (a, ())
> >
> > and now want to prove that g = first f, using the free theorem… which
> > is tricky, because the free theorem is actually not as strong as it
> > could be; it should actually be phrased in terms of relations relation,
> > which might help with the proof.
> >
> > So let me try to calculate the free theorem by hand, following
> > https://www.well-typed.com/blog/2015/05/parametricity/
> >
> > g is related to itself by the relation
> >
> >    [forall z. (A,z) -> (B,z)]
> >
> > and we can calculate
> >
> >   g [forall z. (A,z) -> (B,z)] g
> > ↔ ∀ z z' Rz, g [(A,z) -> (B,z)] g -- Rz relates z and z'
> > ↔ ∀ z z' Rz, ∀ p p', p [(A,z)] p' → g p [(B,z)] g p'
> > ↔ ∀ z z' Rz, ∀ p p', fst p = fst p' ∧ snd p Rz snd p' →
> >       fst (g p) = fst (g p') ∧ snd (g p) Rz snd (g p')
> > ↔ ∀ z z' Rz, ∀ a x x', x Rz x' →
> >       fst (g (a,x)) = fst (g (a,x')) ∧
> > snd (g (a,x)) Rz snd (g (a,x'))
> >
> > We can use this to show
> >
> >    ∀ (a,x :: z). fst (g (a,x)) = f a
> >
> > using (this is the tricky part that requires thinking)
> >
> >    z := z, z' := (), Rz := λ_ _ -> True, a := a, x := x, x' := ()
> >
> > as then the theorem implies
> >
> >   fst (g (a,x)) = fst (g (a, ()) = f a.
> >
> > We can also use it to show
> >
> >    ∀ (a,x :: z). snd (g (a,x)) = x
> >
> > using
> >
> >    z := z, z' := z, Rz := const (= x), a := a, x := x, x' := x
> >
> > as then the theorem implies, under the true assumption  x Rz z'
> >
> >   (snd (g (a,x))) Rz (snd (g (a,x')))
> >   ↔ snd (g (a,x)) = x
> >
> > And from
> >
> >    ∀ (a,x :: z). fst (g (a,x)) = f a
> >    ∀ (a,x :: z). snd (g (a,x)) = x
> >
> > we can conclude that
> >
> >   g = first f
> >
> > as intended.
> >
> > Cheers,
> > Joachim
> >
> >
> >
> > _______________________________________________
> > Haskell-Cafe mailing list
> > To (un)subscribe, modify options or view archives go to:
> > http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
> > Only members subscribed via the mailman list are allowed to post.
--
Joachim Breitner
  [hidden email]
  http://www.joachim-breitner.de/

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.

signature.asc (849 bytes) Download Attachment
Reply | Threaded
Open this post in threaded view
|

Re: Free theorem for `forall z. (A,z) -> (B,z)`?

John Wiegley-2
>>>>> "JB" == Joachim Breitner <[hidden email]> writes:

JB> I felt inspired to revive the free theorem calculator and gave it a new
JB> home (and a modern, browser-only, FRP-based implementation):

Thank you, Joachim! I've used that calculator often, and was sad to see it
shut down.

--
John Wiegley                  GPG fingerprint = 4710 CF98 AF9B 327B B80F
http://newartisans.com                          60E1 46C4 BD1A 7AC1 4BA2

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.

signature.asc (671 bytes) Download Attachment
Reply | Threaded
Open this post in threaded view
|

Re: Free theorem for `forall z. (A,z) -> (B,z)`?

David Feuer
In reply to this post by Joachim Breitner-2
Thank you! Are you going to add a place for auxiliary definitions? Perhaps also a few default definitions like lambdabot uses? As it is, there doesn't seem to be a way to use non-Prelude to constructors. One more thing, that was missing from the original: a good explanation of what the output means. "lift" is particularly mysterious. Lambdabot seems to replace these with calls to normal Haskell functions. Perhaps that can be done sometimes? One last thing: the FRP interface seems a bit *too* responsive. It's not fun to see error messages flashing on and off as I type. Perhaps it would make sense to add a delay before activating one of those?

On Tue, Jul 24, 2018, 1:38 PM Joachim Breitner <[hidden email]> wrote:
Hi,

I felt inspired to revive the free theorem calculator and gave it a new
home (and a modern, browser-only, FRP-based implementation):

http://free-theorems.nomeata.de/

which prints

   forall t1,t2 in TYPES, R in REL(t1,t2).
    forall (x, y) in lift{(,)}(id,R).
     (g_{t1} x, g_{t2} y) in lift{(,)}(id,R)

as the free theorem, which is (if one squints) the same as my

  ∀ z z' Rz, ∀ a x x', x Rz x' →
      fst (g (a,x)) = fst (g (a,x')) ∧ snd (g (a,x)) Rz snd (g (a,x'))

Enjoy,
Joachim

Am Montag, den 23.07.2018, 10:56 -0700 schrieb Conal Elliott:
> Thank you, Joachim! I'm refreshing my memory of free theorem construction from that blog post. Regards, -- Conal
>
> On Mon, Jul 23, 2018 at 8:33 AM, Joachim Breitner <[hidden email]> wrote:
> > Hi Conal,
> >
> > Am Sonntag, den 22.07.2018, 21:29 -0700 schrieb Conal Elliott:
> > > Suppose `g :: forall z. (A,z) -> (B,z)`. Is it necessarily the case
> > > that `g = first f` for some `f :: A -> B` (where `first f (a,b) = (f
> > > a, b)`), perhaps as a free theorem for the type of `g`?
> >
> > there used to be a free theorem calculator at
> > http://www-ps.iai.uni-bonn.de/ft
> > but it seems to be down :-(
> >
> > There is a shell client, ftshell, lets see what it says…
> > it does not build with ghc-8.0 any more :-(
> >
> > Ah, but lambdabot understands @free:
> >
> > <nomeata>   @free g :: forall z. (A,z) -> (B,z)
> > <lambdabot> $map_Pair $id f . g = g . $map_Pair $id f
> >
> > Which is basically what you are writing here:
> >
> > > Note that `(A,)` and `(B,)` are functors and that `g` is a natural
> > > transformation, so `g . fmap h == fmap h . g` for any `h :: u -> v`.
> > > Equivalently, `g . second h == second h . g` (where `second h (a,b) =
> > > (a, h b)`).
> >
> > Doesn’t that already answer the question? Let’s try to make it more
> > rigorous. I define
> >
> > f :: A -> B
> > f a = fst (g (a, ())
> >
> > and now want to prove that g = first f, using the free theorem… which
> > is tricky, because the free theorem is actually not as strong as it
> > could be; it should actually be phrased in terms of relations relation,
> > which might help with the proof.
> >
> > So let me try to calculate the free theorem by hand, following
> > https://www.well-typed.com/blog/2015/05/parametricity/
> >
> > g is related to itself by the relation
> >
> >    [forall z. (A,z) -> (B,z)]
> >
> > and we can calculate
> >
> >   g [forall z. (A,z) -> (B,z)] g
> > ↔ ∀ z z' Rz, g [(A,z) -> (B,z)] g -- Rz relates z and z'
> > ↔ ∀ z z' Rz, ∀ p p', p [(A,z)] p' → g p [(B,z)] g p'
> > ↔ ∀ z z' Rz, ∀ p p', fst p = fst p' ∧ snd p Rz snd p' →
> >       fst (g p) = fst (g p') ∧ snd (g p) Rz snd (g p')
> > ↔ ∀ z z' Rz, ∀ a x x', x Rz x' →
> >       fst (g (a,x)) = fst (g (a,x')) ∧
> > snd (g (a,x)) Rz snd (g (a,x'))
> >
> > We can use this to show
> >
> >    ∀ (a,x :: z). fst (g (a,x)) = f a
> >
> > using (this is the tricky part that requires thinking)
> >
> >    z := z, z' := (), Rz := λ_ _ -> True, a := a, x := x, x' := ()
> >
> > as then the theorem implies
> >
> >   fst (g (a,x)) = fst (g (a, ()) = f a.
> >
> > We can also use it to show
> >
> >    ∀ (a,x :: z). snd (g (a,x)) = x
> >
> > using
> >
> >    z := z, z' := z, Rz := const (= x), a := a, x := x, x' := x
> >
> > as then the theorem implies, under the true assumption  x Rz z'
> >
> >   (snd (g (a,x))) Rz (snd (g (a,x')))
> >   ↔ snd (g (a,x)) = x
> >
> > And from
> >
> >    ∀ (a,x :: z). fst (g (a,x)) = f a
> >    ∀ (a,x :: z). snd (g (a,x)) = x
> >
> > we can conclude that
> >
> >   g = first f
> >
> > as intended.
> >
> > Cheers,
> > Joachim
> >
> >
> >
> > _______________________________________________
> > Haskell-Cafe mailing list
> > To (un)subscribe, modify options or view archives go to:
> > http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
> > Only members subscribed via the mailman list are allowed to post.
--
Joachim Breitner
  [hidden email]
  http://www.joachim-breitner.de/
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Free theorem for `forall z. (A,z) -> (B,z)`?

Joachim Breitner-2
Hi,

Am Dienstag, den 24.07.2018, 14:22 -0400 schrieb David Feuer:
> Thank you! Are you going to add a place for auxiliary definitions?

You wish is my command:
https://github.com/nomeata/free-theorems-static-webui/commit/eb8e820

Should be online in 10mins or so.

> Perhaps also a few default definitions like lambdabot uses?

What do you mean? It has this background theory:
https://github.com/nomeata/free-theorems-static-webui/blob/master/src/KnownDeclarations.hs
(copied from free-theorems-webui)

> As it is, there doesn't seem to be a way to use non-Prelude to
> constructors.

That is fixed now, is it?

> One more thing, that was missing from the original: a good
> explanation of what the output means. "lift" is particularly
> mysterious. Lambdabot seems to replace these with calls to normal
> Haskell functions. Perhaps that can be done sometimes?

Pull requests welcome :-)

> One last thing: the FRP interface seems a bit *too* responsive. It's
> not fun to see error messages flashing on and off as I type. Perhaps
> it would make sense to add a delay before activating one of those?

I guess I can use
https://hackage.haskell.org/package/reflex-dom-0.3/candidate/docs/Reflex-Dom-Time.html
for this somehow. But I guess I only want to delay errors, not
successes – I will give it a shot.

Cheers,
Joachim
--
Joachim Breitner
  [hidden email]
  http://www.joachim-breitner.de/

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.

signature.asc (849 bytes) Download Attachment
Reply | Threaded
Open this post in threaded view
|

Re: Free theorem for `forall z. (A,z) -> (B,z)`?

Joachim Breitner-2
Hi,

Am Dienstag, den 24.07.2018, 14:47 -0400 schrieb Joachim Breitner:
> I guess I can use
> https://hackage.haskell.org/package/reflex-dom-0.3/candidate/docs/Reflex-Dom-Time.html
> for this somehow. But I guess I only want to delay errors, not
> successes – I will give it a shot

Sure, why not:
https://github.com/nomeata/free-theorems-static-webui/commit/20c9aca

it seems to work. If some reflex-expert could check if this makes
sense, that would be great:

-- | Errors are delayed, but successes go through immediatelly
delayError :: (PerformEvent t m, MonadHold t m, TriggerEvent t m, MonadIO (Performable m)) =>
    Dynamic t (Either a b) -> m (Dynamic t (Either a b))
delayError d = do
    delayedEvents <- delay 0.5 (updated d)
    d' <- holdDyn Nothing (Just <$> delayedEvents)
    return $ do
        now <- d
        past <- d'
        return $ case (past, now) of
            (Nothing, _)     -> now    -- before any delayed events arrive
            (_, Right _ )    -> now  -- current value is good
            (Just x, Left _) -> x -- current value is bad, delay

Cheers,
Joachim

--
Joachim Breitner
  [hidden email]
  http://www.joachim-breitner.de/

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.

signature.asc (849 bytes) Download Attachment
Reply | Threaded
Open this post in threaded view
|

Re: Free theorem for `forall z. (A,z) -> (B,z)`?

David Feuer
Personally, I'm old-fashioned. I don't mind having to press a button to make it go. But my preferences are obviously not the end of the discussion.

On Tue, Jul 24, 2018, 3:15 PM Joachim Breitner <[hidden email]> wrote:
Hi,

Am Dienstag, den 24.07.2018, 14:47 -0400 schrieb Joachim Breitner:
> I guess I can use
> https://hackage.haskell.org/package/reflex-dom-0.3/candidate/docs/Reflex-Dom-Time.html
> for this somehow. But I guess I only want to delay errors, not
> successes – I will give it a shot

Sure, why not:
https://github.com/nomeata/free-theorems-static-webui/commit/20c9aca

it seems to work. If some reflex-expert could check if this makes
sense, that would be great:

-- | Errors are delayed, but successes go through immediatelly
delayError :: (PerformEvent t m, MonadHold t m, TriggerEvent t m, MonadIO (Performable m)) =>
    Dynamic t (Either a b) -> m (Dynamic t (Either a b))
delayError d = do
    delayedEvents <- delay 0.5 (updated d)
    d' <- holdDyn Nothing (Just <$> delayedEvents)
    return $ do
        now <- d
        past <- d'
        return $ case (past, now) of
            (Nothing, _)     -> now    -- before any delayed events arrive
            (_, Right _ )    -> now  -- current value is good
            (Just x, Left _) -> x -- current value is bad, delay

Cheers,
Joachim

--
Joachim Breitner
  [hidden email]
  http://www.joachim-breitner.de/
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.