Make the most of Now

 Apologies to the people  who are only in here to  catch epigram code in
their inbox.
But the partial monad ist discussed  as a device for structuring partial
programming in epigram.
And since I wrote these programs mainly to  get a grip on - a very short
prefix of - the discussion Bas Spitters  and Thorsten had on this list a
while ago, I drop them here.

> {-# OPTIONS -fglasgow-exts #-}

General recursion  augments every data  type with an extra  element, the
divergent compution.

>-- data Empty ; bot = bot :: Empty

Thorsten  and  others  have  suggested  to make  this  manifest  in  the
signature of a program, capturing partiality with the delay monad

> data{- codata -}  D a = Now a | Later (D a) ; never = Later never
 
> instance Monad D where
>         return        = Now
>         Now a   >>= f = f a
>         Later d >>= f = Later (d >>= f)

which allows for a notion of a 'race'

> (%) :: D a -> D a -> D a
 
> Now a     % _         = Now a
> _         % Now a     = Now a
> Later d   % Later e   = Later (d % e)
 
('synchronisation' is also at hand)

> (&) :: D a -> D a -> D a
 
> 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)

The delay  monad explains for example  why the /trivial/ fixed  point of
monadic computations isn't very useful.

>-- class Monad m => MonadFix m where
>--         mfix :: (a -> m a) -> m a

>-- instance MonadFix D where
>--         mfix f = f =<< (mfix f)
 
Because taking

> bot = never

this mfix computes  the /least fixed point/ of a  partial program lifted
to a partial domain. Which clearly is bot.

---------------------------------------------------------------------------

Topologists with a heart for computability theory are fond of this datatype

>-- data S = T ; bot = bot :: S

which allows the type of /definable characteristic functions/ of subsets
to be defined as this

>-- type Open a = a -> S

and things start to get interesting with programs of type Open S.

But to be able to define the union of subsets

>-- u `union` v = \x -> u x `or` v x

one needs the following equations to hold.

>-- T   `or` T   = T
>-- T   `or` bot = T
>-- bot `or` T   = T
>-- bot `or` bot = bot

Enter the delay monad...

Quotienting with respect to termination

> top = {- Later $ ... Later $ -} Now never

makes  at  least  the  important  ones from  the  above  equations  hold
/definitionally/.

>-- top % bot ~~> top
>-- bot % top ~~> top

And we can head for a 'subobject classifier'.

> data Zero               {- -}
> type One = D Zero       {- bot -}
> type Omega = D One      {- bot,top -} ; top :: Omega

Now, before you go "Boring!" just because of this

> type Sub a = a -> Omega

> empty :: Sub a  
> empty = const bot

> whole :: Sub a
> whole = const top

consider again the topology of the Sierpinski space.

> [{- -}_,{-top-}_,{-bot,top-}_] = [empty,id,whole] :: [Sub Omega]

Why is {-bot-} :: Sub Omega  missing?

Union and intersection are now definable

> (\/),(/\) :: Sub a -> Sub a -> Sub a

> u \/ v = \a -> u a % v a
> u /\ v = \a -> u a & v a

and readily extend to the countable and finite cases respectively.

> (\/.), (/\.) :: [Sub a] -> Sub a

> (\/.) = foldr (\u v -> u \/ (Later . v)) empty

> (/\.) = foldr (/\) whole

Please note that

> locale :: Sub a -> [Sub a] -> Sub a
> locale =  \   u -> \us     -> u /\ (us \/.)

is well defined even if us is /countable/.

And we can have a poor man's roll your own TT:

> subzero :: Zero -> a
> subzero = \_    -> error ['0'..]

>-- (%),(&) :: Omega -> Omega -> Omega

> type Prop = Sub One

> false :: Prop
> false = \i -> case i of
>                 Now x   -> subzero x
>                 Later d -> Later (false d)

> true :: Prop
> true = Now            -- see subject line


Alladat must  have to with 'coalgebras  give rise to toposes'.  But that
requires more hunting & gathering at the library on my part.


Best regards,
Sebastian