TP | 2 Dec 19:32 2013
Picon

how to factorize propagation of a function over a data type

Hi,

Let us consider the following example:

-----------------------
class FooClass a where
    foo1 :: a -> a
    foo2 :: a -> a

instance FooClass Integer where

    foo1 v = 1
    foo2 v = 2

data Bar = Bar1 Integer
         | Exp1 Bar Bar
         | Exp2 Bar Bar
    deriving Show

instance FooClass Bar where

    foo1 b = case b of
        Bar1 i     -> Bar1 (foo1 i)
        Exp1 b1 b2 -> Exp1 (foo1 b1) (foo1 b2)
        Exp2 b1 b2 -> Exp2 (foo1 b1) (foo1 b2)

    foo2 b = case b of
        Bar1 i     -> Bar1 (foo2 i)
        Exp1 b1 b2 -> Exp1 (foo2 b1) (foo2 b2)
        Exp2 b1 b2 -> Exp2 (foo2 b1) (foo2 b2)
(Continue reading)

Alejandro Serrano Mena | 2 Dec 14:44 2013
Picon

Re: how to factorize propagation of a function over a data type

I have no time now to answer completely, but I would say that type families could help.


2013/12/2 TP <paratribulations <at> free.fr>
Hi,

Let us consider the following example:

-----------------------
class FooClass a where
    foo1 :: a -> a
    foo2 :: a -> a

instance FooClass Integer where

    foo1 v = 1
    foo2 v = 2

data Bar = Bar1 Integer
         | Exp1 Bar Bar
         | Exp2 Bar Bar
    deriving Show

instance FooClass Bar where

    foo1 b = case b of
        Bar1 i     -> Bar1 (foo1 i)
        Exp1 b1 b2 -> Exp1 (foo1 b1) (foo1 b2)
        Exp2 b1 b2 -> Exp2 (foo1 b1) (foo1 b2)

    foo2 b = case b of
        Bar1 i     -> Bar1 (foo2 i)
        Exp1 b1 b2 -> Exp1 (foo2 b1) (foo2 b2)
        Exp2 b1 b2 -> Exp2 (foo2 b1) (foo2 b2)

main = do

let a = Bar1 3
let b = Bar1 4
let c = Exp1 (Exp2 a b) b

print c
print $ foo1 c
print $ foo2 c
-----------------------

We obtain as expected:

$ runghc propagate_with_duplicated_code.hs
Exp1 (Exp2 (Bar1 3) (Bar1 4)) (Bar1 4)
Exp1 (Exp2 (Bar1 1) (Bar1 1)) (Bar1 1)
Exp1 (Exp2 (Bar1 2) (Bar1 2)) (Bar1 2)

My question is related to the code inside the Fooclass instance definition
for Bar: we have repeated code where only "foo1" or "foo2" changes.
So the first idea is to write a higher-order function, but it does not work:

-----------------------
class FooClass a where
    foo1 :: a -> a
    foo2 :: a -> a

instance FooClass Integer where

    foo1 v = 1
    foo2 v = 2

data Bar = Bar1 Integer
         | Exp1 Bar Bar
         | Exp2 Bar Bar
    deriving Show

propagate :: FooClass a => a -> (a->a) -> a
propagate v f = case v of
        Bar1 i     -> Bar1 (f i)
        Exp1 b1 b2 -> Exp1 (f b1) (f b2)
        Exp2 b1 b2 -> Exp2 (f b1) (f b2)

instance FooClass Bar where

    foo1 b = propagate b foo1
    foo2 b = propagate b foo2

main = do

let a = Bar1 3
let b = Bar1 4
let c = Exp1 (Exp2 a b) b

print c
print $ foo1 c
print $ foo2 c
-----------------------

The problem is that the type variable `a` in the definition of `propagate`
cannot match both the type of i, i.e. an integer, and the type of b1 and b2,
i.e. Bar.
Putting the function propagate in the typeclass does not help. How to
factorize my code?

Thanks in advance,

TP

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Daniel Trstenjak | 2 Dec 14:48 2013
Picon

Re: how to factorize propagation of a function over a data type


> class FooClass a where
>     foo1 :: a -> a
>     foo2 :: a -> a
> 
> instance FooClass Integer where
> 
>     foo1 v = 1
>     foo2 v = 2
> 
> data Bar = Bar1 Integer
>          | Exp1 Bar Bar
>          | Exp2 Bar Bar
>     deriving Show
> 
> instance FooClass Bar where
>     
>     foo1 b = case b of
>         Bar1 i     -> Bar1 (foo1 i)
>         Exp1 b1 b2 -> Exp1 (foo1 b1) (foo1 b2)
>         Exp2 b1 b2 -> Exp2 (foo1 b1) (foo1 b2)
> 
>     foo2 b = case b of
>         Bar1 i     -> Bar1 (foo2 i)
>         Exp1 b1 b2 -> Exp1 (foo2 b1) (foo2 b2)
>         Exp2 b1 b2 -> Exp2 (foo2 b1) (foo2 b2)

I think you're really asking for a generics library like 'uniplate':
http://community.haskell.org/~ndm/darcs/uniplate/uniplate.htm

Greetings,
Daniel
Vo Minh Thu | 2 Dec 14:47 2013
Picon

Re: how to factorize propagation of a function over a data type

You can replace your `propagate` function by this one:

    propagate :: Bar -> (Integer -> Integer) -> Bar
    propagate v f = case v of
        Bar1 i     -> Bar1 (f i)
        Exp1 b1 b2 -> Exp1 (propagate b1 f) (propagate b2 f)
        Exp2 b1 b2 -> Exp2 (propagate b1 f) (propagate b2 f)

In your code, you were applying the same (w.r.t. to its type) `f` to
Bar and Integer.

Also, your Bar data type contains, at its leaf, an Intger, not a `a`.

You might want to look at functors, and `fmap` too.

2013/12/2 TP <paratribulations <at> free.fr>:
> Hi,
>
> Let us consider the following example:
>
> -----------------------
> class FooClass a where
>     foo1 :: a -> a
>     foo2 :: a -> a
>
> instance FooClass Integer where
>
>     foo1 v = 1
>     foo2 v = 2
>
> data Bar = Bar1 Integer
>          | Exp1 Bar Bar
>          | Exp2 Bar Bar
>     deriving Show
>
> instance FooClass Bar where
>
>     foo1 b = case b of
>         Bar1 i     -> Bar1 (foo1 i)
>         Exp1 b1 b2 -> Exp1 (foo1 b1) (foo1 b2)
>         Exp2 b1 b2 -> Exp2 (foo1 b1) (foo1 b2)
>
>     foo2 b = case b of
>         Bar1 i     -> Bar1 (foo2 i)
>         Exp1 b1 b2 -> Exp1 (foo2 b1) (foo2 b2)
>         Exp2 b1 b2 -> Exp2 (foo2 b1) (foo2 b2)
>
> main = do
>
> let a = Bar1 3
> let b = Bar1 4
> let c = Exp1 (Exp2 a b) b
>
> print c
> print $ foo1 c
> print $ foo2 c
> -----------------------
>
> We obtain as expected:
>
> $ runghc propagate_with_duplicated_code.hs
> Exp1 (Exp2 (Bar1 3) (Bar1 4)) (Bar1 4)
> Exp1 (Exp2 (Bar1 1) (Bar1 1)) (Bar1 1)
> Exp1 (Exp2 (Bar1 2) (Bar1 2)) (Bar1 2)
>
> My question is related to the code inside the Fooclass instance definition
> for Bar: we have repeated code where only "foo1" or "foo2" changes.
> So the first idea is to write a higher-order function, but it does not work:
>
> -----------------------
> class FooClass a where
>     foo1 :: a -> a
>     foo2 :: a -> a
>
> instance FooClass Integer where
>
>     foo1 v = 1
>     foo2 v = 2
>
> data Bar = Bar1 Integer
>          | Exp1 Bar Bar
>          | Exp2 Bar Bar
>     deriving Show
>
> propagate :: FooClass a => a -> (a->a) -> a
> propagate v f = case v of
>         Bar1 i     -> Bar1 (f i)
>         Exp1 b1 b2 -> Exp1 (f b1) (f b2)
>         Exp2 b1 b2 -> Exp2 (f b1) (f b2)
>
> instance FooClass Bar where
>
>     foo1 b = propagate b foo1
>     foo2 b = propagate b foo2
>
> main = do
>
> let a = Bar1 3
> let b = Bar1 4
> let c = Exp1 (Exp2 a b) b
>
> print c
> print $ foo1 c
> print $ foo2 c
> -----------------------
>
> The problem is that the type variable `a` in the definition of `propagate`
> cannot match both the type of i, i.e. an integer, and the type of b1 and b2,
> i.e. Bar.
> Putting the function propagate in the typeclass does not help. How to
> factorize my code?
>
> Thanks in advance,
>
> TP
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe <at> haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
TP | 2 Dec 20:37 2013
Picon

Re: how to factorize propagation of a function over a data type

Vo Minh Thu wrote:

> You can replace your `propagate` function by this one:
> 
>     propagate :: Bar -> (Integer -> Integer) -> Bar
>     propagate v f = case v of
>         Bar1 i     -> Bar1 (f i)
>         Exp1 b1 b2 -> Exp1 (propagate b1 f) (propagate b2 f)
>         Exp2 b1 b2 -> Exp2 (propagate b1 f) (propagate b2 f)
> 
> In your code, you were applying the same (w.r.t. to its type) `f` to
> Bar and Integer.
> Also, your Bar data type contains, at its leaf, an Intger, not a `a`.

You are right, I made a stupid error in my code. The following version 
indeed works:

----------------
class FooClass a where
    foo1 :: a -> a
    foo2 :: a -> a

instance FooClass Integer where

    foo1 v = 1
    foo2 v = 2

data Bar = Bar1 Integer
         | Exp1 Bar Bar
         | Exp2 Bar Bar
    deriving Show

-- The following line works because there are only integers in the leaves.
propagate :: Bar -> (Integer -> Integer) -> Bar
propagate v f = case v of
        Bar1 i     -> Bar1 (f i)
        Exp1 b1 b2 -> Exp1 (propagate b1 f) (propagate b2 f)
        Exp2 b1 b2 -> Exp2 (propagate b1 f) (propagate b2 f)

instance FooClass Bar where

    foo1 b = propagate b foo1
    foo2 b = propagate b foo2

main = do

let a = Bar1 3
let b = Bar1 4
let c = Exp1 (Exp2 a b) b

print c
print $ foo1 c
print $ foo2 c
----------------

However, if we add another type in the leaves, we cannot use the solution 
above.

----------------
class FooClass a where
    foo1 :: a -> a
    foo2 :: a -> a

instance FooClass Integer where

    foo1 v = 1
    foo2 v = 2

instance FooClass Float where

    foo1 v = 0.25
    foo2 v = 0.5

data Bar = Bar1 Integer
         | Bar2 Float
         | Exp1 Bar Bar
         | Exp2 Bar Bar
    deriving Show

-- This time the following line does not work.
propagate :: Bar -> (Integer -> Integer) -> Bar
-- The following line does not work either.
-- propagate :: FooClass a => Bar -> (a->a) -> Bar
propagate v f = case v of
        Bar1 i     -> Bar1 (f i)
        Bar2 i     -> Bar2 (f i)
        Exp1 b1 b2 -> Exp1 (propagate b1 f) (propagate b2 f)
        Exp2 b1 b2 -> Exp2 (propagate b1 f) (propagate b2 f)

instance FooClass Bar where

    foo1 b = propagate b foo1
    foo2 b = propagate b foo2

main = do

let a = Bar1 3
let b = Bar1 4
let c = Exp1 (Exp2 a b) b

print c
print $ foo1 c
print $ foo2 c
----------------
Andras Slemmer | 2 Dec 17:21 2013
Picon

Re: how to factorize propagation of a function over a data type

There are several ways to approach this problem. What you are basically trying to do is map a function over the leaves of your datastructure. So naturally a function that comes to mind is:

mapBar :: (Integer -> Integer) -> (Float -> Float) -> Bar -> Bar
mapBar f _ (Bar1 i) = Bar1 (f i)
mapBar _ g (Bar2 r) = Bar2 (g r)
mapBar f g (Exp1 e1 e2) = Exp1 (mapBar f g e1) (mapBar f g e2)
mapBar f g (Exp2 e1 e2) = Exp2 (mapBar f g e1) (mapBar f g e2)

And the Bar instance becomes

instance FooClass Bar where
    foo1 = mapBar foo1 foo1
    foo2 = mapBar foo2 foo2

As far as I understand this is not what you're looking for, as you want the mapBar function to be agnostic wrt what type the leaves contain. The minimal assumption that this requires is that the leaf types are a member of FooClass, and indeed you can write such a map:

mapBar :: (forall a. FooClass a => a -> a) -> Bar -> Bar
mapBar f (Bar1 i) = Bar1 (f i)
mapBar f (Bar2 r) = Bar2 (f r)
mapBar f (Exp1 e1 e2) = Exp1 (mapBar f e1) (mapBar f e2)
mapBar f (Exp2 e1 e2) = Exp2 (mapBar f e1) (mapBar f e2)

instance FooClass Bar where
    foo1 = mapBar foo1
    foo2 = mapBar foo2

I think this is closer to what you were looking for. The above map requires -XRankNTypes, because mapBar requires a function that is fully polymorphic ('a' will instantiate to Integer and Float respectively). If you haven't used higher ranked types before I think it is instructive to think about why the above signature works and the one you wrote doesn't. In particular think about at which point the polymorphic type 'a' is instantiated in both cases, or rather what the "scope" of 'a' is.


On 2 December 2013 19:37, TP <paratribulations <at> free.fr> wrote:
Vo Minh Thu wrote:

> You can replace your `propagate` function by this one:
>
>     propagate :: Bar -> (Integer -> Integer) -> Bar
>     propagate v f = case v of
>         Bar1 i     -> Bar1 (f i)
>         Exp1 b1 b2 -> Exp1 (propagate b1 f) (propagate b2 f)
>         Exp2 b1 b2 -> Exp2 (propagate b1 f) (propagate b2 f)
>
> In your code, you were applying the same (w.r.t. to its type) `f` to
> Bar and Integer.
> Also, your Bar data type contains, at its leaf, an Intger, not a `a`.

You are right, I made a stupid error in my code. The following version
indeed works:

----------------
class FooClass a where
    foo1 :: a -> a
    foo2 :: a -> a

instance FooClass Integer where

    foo1 v = 1
    foo2 v = 2

data Bar = Bar1 Integer
         | Exp1 Bar Bar
         | Exp2 Bar Bar
    deriving Show

-- The following line works because there are only integers in the leaves.
propagate :: Bar -> (Integer -> Integer) -> Bar
propagate v f = case v of
        Bar1 i     -> Bar1 (f i)
        Exp1 b1 b2 -> Exp1 (propagate b1 f) (propagate b2 f)
        Exp2 b1 b2 -> Exp2 (propagate b1 f) (propagate b2 f)

instance FooClass Bar where

    foo1 b = propagate b foo1
    foo2 b = propagate b foo2

main = do

let a = Bar1 3
let b = Bar1 4
let c = Exp1 (Exp2 a b) b

print c
print $ foo1 c
print $ foo2 c
----------------

However, if we add another type in the leaves, we cannot use the solution
above.

----------------
class FooClass a where
    foo1 :: a -> a
    foo2 :: a -> a

instance FooClass Integer where

    foo1 v = 1
    foo2 v = 2

instance FooClass Float where

    foo1 v = 0.25
    foo2 v = 0.5

data Bar = Bar1 Integer
         | Bar2 Float
         | Exp1 Bar Bar
         | Exp2 Bar Bar
    deriving Show

-- This time the following line does not work.
propagate :: Bar -> (Integer -> Integer) -> Bar
-- The following line does not work either.
-- propagate :: FooClass a => Bar -> (a->a) -> Bar
propagate v f = case v of
        Bar1 i     -> Bar1 (f i)
        Bar2 i     -> Bar2 (f i)
        Exp1 b1 b2 -> Exp1 (propagate b1 f) (propagate b2 f)
        Exp2 b1 b2 -> Exp2 (propagate b1 f) (propagate b2 f)

instance FooClass Bar where

    foo1 b = propagate b foo1
    foo2 b = propagate b foo2

main = do

let a = Bar1 3
let b = Bar1 4
let c = Exp1 (Exp2 a b) b

print c
print $ foo1 c
print $ foo2 c
----------------

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
TP | 2 Dec 23:01 2013
Picon

Re: how to factorize propagation of a function over a data type

Andras Slemmer wrote:

> As far as I understand this is not what you're looking for, as you want
> the mapBar function to be agnostic wrt what type the leaves contain. The
> minimal assumption that this requires is that the leaf types are a member
> of FooClass, and indeed you can write such a map:
> 
> mapBar :: (forall a. FooClass a => a -> a) -> Bar -> Bar
> mapBar f (Bar1 i) = Bar1 (f i)
> mapBar f (Bar2 r) = Bar2 (f r)
> mapBar f (Exp1 e1 e2) = Exp1 (mapBar f e1) (mapBar f e2)
> mapBar f (Exp2 e1 e2) = Exp2 (mapBar f e1) (mapBar f e2)
> 
> instance FooClass Bar where
>     foo1 = mapBar foo1
>     foo2 = mapBar foo2
> 
> I think this is closer to what you were looking for. The above map
> requires -XRankNTypes, because mapBar requires a function that is fully
> polymorphic ('a' will instantiate to Integer and Float respectively). If
> you haven't used higher ranked types before I think it is instructive to
> think about why the above signature works and the one you wrote doesn't.
> In particular think about at which point the polymorphic type 'a' is
> instantiated in both cases, or rather what the "scope" of 'a' is.

Thanks a lot. This solution has already been proposed to me in the afternoon 
by JC Mincke in a private communication.

Indeed I did not know RankNTypes. I think I understand your explanation in 
terms of "scope" of 'a':

In the type signature

propagate :: (FooClass a)=> Bar -> (a->a) -> Bar

which is in fact implicitly

propagate :: forall a. (FooClass a)=> Bar -> (a->a) -> Bar

it is supposed that the type signature of propagate is valid for a given 
value of the type variable a, i.e. a given type. Thus we obtain an error if 
we apply recursively propagate to different types in the code of propagate. 
Whereas in the type signature

propagate :: Bar -> (forall a. (FooClass a) => a->a) -> Bar

the type signature of propagate is such that it allows several values for 
the type variable `a` in its second argument `a->a`.

PS: a working code corresponding to my last example:

-------------
{-# LANGUAGE RankNTypes #-}

class FooClass a where
    foo1 :: a -> a
    foo2 :: a -> a

instance FooClass Integer where

    foo1 v = 1
    foo2 v = 2

instance FooClass Float where

    foo1 v = 0.25
    foo2 v = 0.5

data Bar  = Bar1 Integer
         | Bar2 Float
         | Exp1 Bar Bar
         | Exp2 Bar Bar
    deriving Show

propagate :: Bar -> (forall a. (FooClass a) => a->a) -> Bar
propagate v f = case v of
        Bar1 i     -> Bar1 (f i)
        Bar2 fl    -> Bar2 (f fl)
        Exp1 b1 b2 -> Exp1 (propagate b1 f) (propagate b2 f)
        Exp2 b1 b2 -> Exp2 (propagate b1 f) (propagate b2 f)
-- The two previous lines may be replaced by:
--         Exp1 b1 b2 -> Exp1 (f b1) (f b2)
--         Exp2 b1 b2 -> Exp2 (f b1) (f b2)

instance FooClass Bar where

    foo1 b = propagate b foo1
    foo2 b = propagate b foo2

main = do

let a = Bar1 3
let b = Bar1 4
let c = Bar2 0.4
let d = Exp1 (Exp2 a c) b

print d
print $ foo1 d
print $ foo2 d
---------------
TP | 2 Dec 23:28 2013
Picon

Re: how to factorize propagation of a function over a data type

TP wrote:

> propagate :: Bar -> (forall a. (FooClass a) => a->a) -> Bar

In fact, I do not understand why we have to add the typeclass constraint 
(FooClass a).
Indeed, there is no mention to foo1 and foo2 functions (members of the 
FooClass typeclass) in the code of propagate:

-------
propagate v f = case v of
        Bar1 i     -> Bar1 (f i)
        Exp1 b1 b2 -> Exp1 (propagate b1 f) (propagate b2 f)
        Exp2 b1 b2 -> Exp2 (propagate b1 f) (propagate b2 f)
-------

propagate deals with any function a priori, not only foo1 and foo2. So how 
to understand the need for this typeclass constraint?

TP
Andras Slemmer | 2 Dec 20:11 2013
Picon

Re: how to factorize propagation of a function over a data type

The reason you need the typeclass constraint is not in the use of 'f' but rather in the use of propagate and what you pass in to it (foo1/foo2 here). If you leave away the typeclass constraint what you're left with is:

propagate' Bar -> (forall a. a->a) -> Bar

The implementation of this function is the same as before, however your use of propagate' is restricted:
forall a. a->a is a very "strict" type, in fact the only inhabitant of this type is 'id' (and bottom, but disregard that here), which means the only way to call propagate is to pass in 'id'. Try it yourself!

Related note: there is a proof that in fact the only inhabitant of (forall a. a -> a) is 'id' and it is the consequence of the "parametricity" property. It is a very neat result I suggest you look it up!


On 2 December 2013 22:28, TP <paratribulations <at> free.fr> wrote:
TP wrote:

> propagate :: Bar -> (forall a. (FooClass a) => a->a) -> Bar

In fact, I do not understand why we have to add the typeclass constraint
(FooClass a).
Indeed, there is no mention to foo1 and foo2 functions (members of the
FooClass typeclass) in the code of propagate:

-------
propagate v f = case v of
        Bar1 i     -> Bar1 (f i)
        Exp1 b1 b2 -> Exp1 (propagate b1 f) (propagate b2 f)
        Exp2 b1 b2 -> Exp2 (propagate b1 f) (propagate b2 f)
-------

propagate deals with any function a priori, not only foo1 and foo2. So how
to understand the need for this typeclass constraint?

TP

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
TP | 3 Dec 03:30 2013
Picon

Re: how to factorize propagation of a function over a data type

Andras Slemmer wrote:

> The reason you need the typeclass constraint is not in the use of 'f' but
> rather in the use of propagate and what you pass in to it (foo1/foo2
> here). If you leave away the typeclass constraint what you're left with
> is:
> 
> propagate' Bar -> (forall a. a->a) -> Bar
> 
> The implementation of this function is the same as before, however your
> use of propagate' is restricted:
> forall a. a->a is a very "strict" type, in fact the only inhabitant of
> this type is 'id' (and bottom, but disregard that here), which means the
> only way to call propagate is to pass in 'id'. Try it yourself!

Indeed I have tried, it works as you say.

> Related note: there is a proof that in fact the only inhabitant of (forall
> a. a -> a) is 'id' and it is the consequence of the "parametricity"
> property. It is a very neat result I suggest you look it up!

Interesting. I have tried to google on the topic, but I find mainly research 
articles. For example:

https://www.google.fr/search?client=ubuntu&channel=fs&q=haskell+%22parametricity+property%22&ie=utf-8&oe=utf-8&gws_rd=cr&ei=P_acUvboDse_0QX9mYDADQ#channel=fs&q=%22parametricity+property%22+haskell

Are there textbooks where a proof of this fact could be found? I'm an 
autodidact (who also benefits from help of guys like you), I don't know what 
lectures on type theory at university level could look like.

Thanks

TP
Tom Ellis | 2 Dec 22:58 2013
Picon

Re: how to factorize propagation of a function over a data type

On Mon, Dec 02, 2013 at 10:30:11PM -0400, TP wrote:
> Andras Slemmer wrote:
> > Related note: there is a proof that in fact the only inhabitant of (forall
> > a. a -> a) is 'id' and it is the consequence of the "parametricity"
> > property. It is a very neat result I suggest you look it up!
> 
> Are there textbooks where a proof of this fact could be found? I'm an 
> autodidact (who also benefits from help of guys like you), I don't know what 
> lectures on type theory at university level could look like.

I guess the most accessible reference might be Wadler 1989 "Theorems for
Free".

    http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.38.9875

Tom

Gmane