- Contemporary messages sorted: [ by date ] [ by thread ] [ by subject ] [ by author ] [ by messages with attachments ]

From: Jan Christiansen <jac_at_informatik.uni-kiel.de>

Date: Wed, 03 Sep 2008 09:26:18 +0200

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

Date: Wed, 03 Sep 2008 09:26:18 +0200

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

*
This archive was generated by hypermail 2.3.0
: Mi Jul 28 2021 - 07:15:03 CEST
*