Expressing "self-composable" functions at the type level
Hi, I'm wondering if there's some way to express that a function can be composed with itself at the type level. Due to polymorphism this is not quite the same as saying that the domain and co-domain match. Example: swap :: (a, b) -> (b, a) swap . swap :: (a, b) -> (a, b) I'd like to write a function such as (in pseudocode): involute :: ((a -> b) &&& (b -> a)) -> (a -> a) involute f = f . f But I obviously can't write down the type for (a -> b) &&& (b -> a) Perhaps this can be done with some typeclass hackery? -- Ignas
Due to polymorphism this is not quite the same as saying that the domain and co-domain match.
I believe it's the same as saying that the type of the co-domain can be refined to the type of the domain. Self-composability is already expressed at the type level, although it may not be immediately clear. In the case of swap, it might seem like it's not possible because (b, a) can be refined to (a, b) only if a = b, but when we compose swap with itself we get fresh names for the type variables, and (b, a) can indeed be refined to (a1, b1). Trying to type (swap . swap) we find that the first swap has type (a, b) -> (b, a) and the second swap has type (a1, b1) -> (b1, a1) so if we set b = a1 and a = b1 then we recover the type (b1, a1) -> (b1, a1). Alex On 2013-11-09, at 6:46 PM, Ignas Vyšniauskas wrote:
Hi,
I'm wondering if there's some way to express that a function can be composed with itself at the type level. Due to polymorphism this is not quite the same as saying that the domain and co-domain match.
Example:
swap :: (a, b) -> (b, a) swap . swap :: (a, b) -> (a, b)
I'd like to write a function such as (in pseudocode):
involute :: ((a -> b) &&& (b -> a)) -> (a -> a) involute f = f . f
But I obviously can't write down the type for (a -> b) &&& (b -> a)
Perhaps this can be done with some typeclass hackery?
-- Ignas _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
On 11/10/2013 01:14 AM, Alexander Vieth wrote:
Due to polymorphism this is not quite the same as saying that the domain and co-domain match.
I believe it's the same as saying that the type of the co-domain can be refined to the type of the domain. Self-composability is already expressed at the type level, although it may not be immediately clear.
In the case of swap, it might seem like it's not possible because (b, a) can be refined to (a, b) only if a = b, but when we compose swap with itself we get fresh names for the type variables, and (b, a) can indeed be refined to (a1, b1). Trying to type (swap . swap) we find that the first swap has type (a, b) -> (b, a) and the second swap has type (a1, b1) -> (b1, a1) so if we set b = a1 and a = b1 then we recover the type (b1, a1) -> (b1, a1).
Hmm, you are right, I didn't quite think through the case of swap. Thanks! Another case would be to consider a function like: double :: a -> (a, a) double x = \x -> (x, x) then (double . double) is possible, but (I think) it's impossible to write a function for such compositions in general: e.g. Prelude> let involute = \f -> f . f Prelude> :t involute (\x -> (x, x)) <interactive>:1:18: Occurs check: cannot construct the infinite type: t0 = (t0, t1) I guess this is simply not type-able in System F? -- Ignas
On Sat, Nov 9, 2013 at 7:53 PM, Ignas Vyšniauskas
I guess this is simply not type-able in System F?
There are System F types that can accomplish some cases of this; just not Hindley-Milner types. For instance: twicePair :: (forall a. a -> (a, a)) -> (forall a. a -> ((a,a),(a,a))) twicePair f = f . f That is, of course, very specific to your example. Doing significantly better is harder, and I don't think you'll ever get to the real type you want, which is: twice : ((a -> b) ∩ (b -> c)) -> a -> c I.E. look up interstection types if you're into this stuff. They tend to be less popular than quantifier-based polymorphism, though.
Hi, On 11/10/2013 03:18 AM, Dan Doel wrote:
Doing significantly better is harder, and I don't think you'll ever get to the real type you want, which is:
twice : ((a -> b) ∩ (b -> c)) -> a -> c
I.E. look up interstection types if you're into this stuff. They tend to be less popular than quantifier-based polymorphism, though.
I think the problem is that having intersection types implies subtyping, and subtyping is obviously troublesome. Essentially the same problem [as mine] is discussed in an old thread, where a partial ("value-level") solution is proposed via typeclass hackery: http://www.haskell.org/pipermail/haskell-cafe/2006-January/013868.html -- Ignas
participants (3)
-
Alexander Vieth -
Dan Doel -
Ignas Vyšniauskas