It's interesting to notice that there's nothing with that type on hoogle (Haskell language search engine), so it's not the type of any common utility.
On the other hand, you can still say quite a bit on functions of that type, drawing from type and set theory.
First, let's name a generic function with that type k:(A→B)→A . It's possible to show that k cannot be parametric in both types. If it were, (0→0)→0 would be valid, which is absurd (0→0 has an element!). It' also possible to show that if k is not parametric in one type, it must have access to at least an element of that type (think about (A→0)→A and (0→B)→0).
A simple cardinality argument also shows that k must be many-to-one (that is, non injective): unless B is 1 (the one element type), |BA|>|A|
There is an interesting operator that uses k, which I call interleave:
interleave:((A→B)→A)→(A→B)→B
Trivially, interleave=λk,f.f(k(f))
It's interesting because partially applying interleave to some k has the type (A→B)→B, which is the type of continuations, and I suspect that this is what underlies the common usage of such operators.
It's interesting to notice that there's nothing with that type on hoogle (Haskell language search engine), so it's not the type of any common utility.
On the other hand, you can still say quite a bit on functions of that type, drawing from type and set theory.
First, let's name a generic function with that type k:(A→B)→A . It's possible to show that k cannot be parametric in both types. If it were, (0→0)→0 would be valid, which is absurd (0→0 has an element!). It' also possible to show that if k is not parametric in one type, it must have access to at least an element of that type (think about (A→0)→A and (0→B)→0).
A simple cardinality argument also shows that k must be many-to-one (that is, non injective): unless B is 1 (the one element type), |BA|>|A|
There is an interesting operator that uses k, which I call interleave:
interleave:((A→B)→A)→(A→B)→B
Trivially, interleave=λk,f.f(k(f))
It's interesting because partially applying interleave to some k has the type (A→B)→B, which is the type of continuations, and I suspect that this is what underlies the common usage of such operators.