[Haskell-beginners] infinite type

[Julian Rohrhuber]

> On 03.01.2016, at 22:30, Theodore Lief Gannon <tanuki at gmail.com> wrote:
> 
>    sum :: Num a => a -> (a -> a)
>    f :: (a -> a) -> (a -> a)
> 
> To really drive it home, let's play with synonyms.
> 
>    type Endo' a = (a -> a)
> 
> Endo already exists as a newtype in Data.Monoid, thus Endo' here. Now:
> 
>    sum :: Num a => a -> Endo' a
>    f :: Endo' a -> Endo’ a

ok, this makes sense to me now – thank you very much for your patience. I’m trying to make the conclusion explicit, so please correct me if I’m wrong.

if type checking of "f sum" assumes the type variable "a" to be of type Endo' in f, it concludes: 

sum takes Endo' to Endo' Endo'

which looks equivalent to trying to construct an infinite type.

The type checker seems not to worry about the more obvious arity/Num restriction of sum, which makes the result more interesting.

More generally, if 

1) f is a function that maps a function to a function of the same type (a -> a) -> (a -> a)
2) sum is a function that maps a value of type b to a function from (b -> b)
3) then their composition “f sum” would have two constraints: 
	sum maps value a into function b = (a -> a)
	but f assumes equality between a and b, 
	so that the required type would be one where a = (a -> a).

which is possibly inconsistent, e.g. when it is interpreted as a definition of a set which has as its elements all sets of pairs of elements of that same set.


> On 03.01.2016, at 22:50, Imants Cekusins <imantc at gmail.com> wrote:
> Could you think of a useful practical example of 
> 
> (a->a->a) . (a->a->a)


Good question. I indeed had nothing else in mind but to reason about functions. Which is quite practical if you are trying to understand haskell!

I could imagine useful variants of function application, but that is pure speculation.