<html><head></head><body class="ApplePlainTextBody" dir="auto" style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;"><br><blockquote type="cite">On 03.01.2016, at 22:30, Theodore Lief Gannon <tanuki@gmail.com> wrote:<br><br> sum :: Num a => a -> (a -> a)<br> f :: (a -> a) -> (a -> a)<br><br>To really drive it home, let's play with synonyms.<br><br> type Endo' a = (a -> a)<br><br>Endo already exists as a newtype in Data.Monoid, thus Endo' here. Now:<br><br> sum :: Num a => a -> Endo' a<br> f :: Endo' a -> Endo’ a<br></blockquote><br>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.<br><br>if type checking of "f sum" assumes the type variable "a" to be of type Endo' in f, it concludes: <br><br>sum takes Endo' to Endo' Endo'<br><br>which looks equivalent to trying to construct an infinite type.<br><br>The type checker seems not to worry about the more obvious arity/Num restriction of sum, which makes the result more interesting.<br><br>More generally, if <br><br>1) f is a function that maps a function to a function of the same type (a -> a) -> (a -> a)<br>2) sum is a function that maps a value of type b to a function from (b -> b)<br>3) then their composition “f sum” would have two constraints: <br><span class="Apple-tab-span" style="white-space:pre"> </span>sum maps value a into function b = (a -> a)<br><span class="Apple-tab-span" style="white-space:pre"> </span>but f assumes equality between a and b, <br><span class="Apple-tab-span" style="white-space:pre"> </span>so that the required type would be one where a = (a -> a).<br><br>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.<br><br><br><blockquote type="cite">On 03.01.2016, at 22:50, Imants Cekusins <imantc@gmail.com> wrote:<br>Could you think of a useful practical example of <br><br>(a->a->a) . (a->a->a)<br></blockquote><br><br>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!<br><br>I could imagine useful variants of function application, but that is pure speculation.<br><br><br><br></body></html>