Hi,
I just came across Comonads and asked myself how they are connected
with Monads and function inversion in Curry.
We can implement a function inversion on basis of function patterns
as follows.
inv :: (a -> b) -> b -> a
inv f b = inv' b
where
inv' (f a) = a
We can as well implement ''inv'' by means of a free variable and
equality but this would make functions defined using ''inv'' to be
strict.
While return has type ''a -> m a'' the corresponding function of a
Comonad ''extract'' has type ''m a -> a''. For the example I will use
lists as an instance of monad here.
return :: a -> [a]
return x = [x]
The type of ''extract'' suggests that we can implement it as the
inverison of ''return''.
extract :: [a] -> a
extract = inv return
But sadly this is not equivenlent with the standard defintion made in
Haskell as it is defined as follows.
extract :: [a] -> a
extract = head
The difference is that the inverse of ''return'' will fail if it is
applied to ''[1,2]'' while ''extract'' yields ''1''. This is probably
not the intended behaviour of extract.
In Curry we can define ''return'' as follows. In this case the
inverse of ''return'' is "equivalent" to ''head''.
return :: a -> [a]
return x = x:xs
where
xs free
Sadly this implementation of ''return'' does not fulfil the monad
laws as (>>= return) /= id.
Although ''inv return'' is not equivalent with the standard Haskell
implementation of ''extract'' we can prove that it does fulfil the
comonad law ''(=>>) extract == id''.
(=>>) extract
-- def of extract
= inv (>>= inv (inv return))
-- inv (inv f) == f
= inv (>>= return)
-- monad law: (>>= return) == id
= inv id
-- inv id == id
= id
Note that there is no formal justification for the laws used here
like ''inv (inv f) == f''. Note furthermore that we do not make use
of the fact that we used a list instance. That is, this is true for
any monad instance.
Similar to ''extract'' we can try to define ''(=>>)'' in terms of
''(>>=)''.
(>>=) :: [a] -> (a -> [b]) -> [b]
m >>= k = foldr ((++) . k) [] m
(=>>) :: ([a] -> b) -> [a] -> [b]
k =>> m = inv (>>= inv k) m
The problem is that we are not able to prove the second law of
comonads ''extract . (f =>>) == f''.
extract . (f =>>)
-- def extract and (=>>)
= inv return . inv (>>= inv f)
-- inv f . inv g == inv (g . f)
= inv ((>>= inv f) . return)
-- monad law: (>>= k) . return == k
= inv (inv f)
-- inv (inv f) = f
= f
Well this looks nice but there is a flaw. The equation ''inv (f . g)
== inv f . inv g'' is wrong. Let us instantiate ''f'' and ''g'' as
follows.
g () = True:g ()
f l = head l
While ''inv (f . g) True'' yields ''()'' ''(inv f . inv g) True''
does not terminate. I think we get something like
inv (f . g) <= inv f . inv g
for any ''f'' and any ''g''. Therefore ''extract . (f =>>)'' is less
defined then ''f''. I think it would be possible to find a more
precise condition for which ''f'' and ''g'' the left hand side is
less defined.
I think we can do similar things for fold and unfold. That is, if we
have a fold we get the unfold for free (sadly with restrictions
caused by the inequality of ''inv (f . g)'' and ''inv f . inv g'').
Cheers Jan
_______________________________________________
curry mailing list
curry_at_lists.RWTH-Aachen.DE
http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry
Received on Mi Sep 03 2008 - 09:37:14 CEST