Been playing with the partial monad a little longer. Tried to
use it for making the equations of section 3.4 of these nice
lecture notes
http://www.cs.bham.ac.uk/~mhe/papers/entcs87.pdf
hold /definitionally/.
> {-# OPTIONS -fglasgow-exts #-}
Given the suitable codata to capture divergence
> {-co-}data D a = Now a | Later (D a) ; never = Later never
we can not only 'race' two or (infinitely many) more
computations against each other
> Now a \/ _ = Now a
> _ \/ Now a = Now a
> Later d \/ Later e = Later (d \/ e)
but also 'sync' two or finitely more of them.
> Now a /\ Now _ = Now a
> a@(Now _) /\ Later d = Later (a /\ d)
> Later d /\ a@(Now _) = Later (d /\ a)
> Later d /\ Later e = Later (d /\ e)
By quotienting with respect to termination we can have this
initial fragment of the finite sets,
> data Zero -- {}
> type One = D Zero -- {never}
> type Two = D One -- {never,Now never}
allowing us to introduce the subset functor
> type Sub a = a -> Two
which - like the contrapositive of negation - is contravariant.
> ( # ) :: (a -> b) -> Sub b -> Sub a
> ( # ) = flip (.)
((id :: a -> a) # ) = id :: Sub a -> Sub a
((g . f) # ) = (f # ) . (g # )
For example /Sub Two/ gives the topology of the Sierpinski
space, consisting of (const never), id and (const (Now never))
which correspond to {},{Now never} and {never,Now never}
respectively. But there'll be no characteristic function for
{never}.
All this corresponds more to constructive set theory where to
give an element of the union of two sets it suffices to give one
from either one but unlike type theory it's not recorded from
which one.
> union :: Sub a -> Sub a -> Sub a
> union = \u -> \v -> \x -> u x \/ v x
And so Conor's orwell-story
http://sneezy.cs.nott.ac.uk/fplunch/weblog/?p=69
/here/ can only be told with functions, not functors:
> zero :: Sub a
> zero = const never
> nogood f = f # zero -- > zero
> orwell f a b = f # (a `union` b) -- > (f # a) `union` (f # b)
I'd really like to see the partial monad beeing integrated into
epigram, because it not only gives safer general recursion but
allows to express semi-deciadable properties like inequality for
codata.
Cheers,
Sebastian
