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
