CODEWITHSUNDEEP
haskell
Clinton
Clinton

Reputation: 23135

Tricky type signature for pairs of reversed pairs

Lets say I have the following data type:

data D a b = D (a,b) (b,a)

And I want to define the following function on it:

apply f (D x y) = D (f x) (f y)

What is the type signature of apply?

Here are some examples of f which are okay:

f :: a -> a -- OK
f :: (a, b) -> (b, a) -- OK
f :: (a, b) -> ((a, c), (b, c)) -- OK

In all of the above cases, we end up with a valid type D.

But this is not okay:

f :: (a, b) -> (a, a)

Because when we send such a function through apply we end up having to attempt to construct D (a,a) (b,b) which is not valid unless a = b.

I can't seem to work out a type signature to express all this? Also, in general, is there a way to get GHC to tell me what these signatures should be?

Typed Holes Edit:

In an attempt to find the type using typed holes, I tried the following:

x = apply _ (D (1::Int,'a') ('b',2::Int))

And got:

Found hole ‘_’ with type: (Int, Int) -> (b, b)
Where: ‘b’ is a rigid type variable bound by
           the inferred type of x :: D b b

Which seems to me to be nonsense as f :: (Int, Int) -> (b, b) is clearly not going to work here.

Upvotes: 5

Views: 112

Answers (2)

dfeuer
dfeuer

Reputation: 48581

Taking things to extremes of generality, we want a type that looks like

apply :: tf -> D a b -> D c d

where tf represents the type of f. In order to apply f to (a,b) and get (c,d), we need

tf ~ (a,b) -> (c,d)

In order to apply f to (b,a) to get (d,c), we need

tf ~ (b,a) -> (d,c)

If we turn on TypeFamilies (or GADTs) we get the magic constraint we need to express that:

{-# LANGUAGE TypeFamilies #-}

apply :: (((a,b) -> (c,d)) ~ tf,
          ((b,a) -> (d,c)) ~ tf) =>
         tf -> D a b -> D c d

I suspect this is one of the most general types available. Unfortunately, it's pretty wild; working through whether a particular application will pass the type checker is not always so easy. Note also that for reasons I don't personally understand, you can't reliably define specializations using

apply' :: ...
apply' = apply

Instead, you sometimes must use

apply' f = apply f

Upvotes: 0

András Kovács
András Kovács

Reputation: 30103

Multiple types fit apply, but the inferred ((t, t) -> (b, b)) -> D t t -> D b b is the most sensible and usable one. The alternatives are going to be higher-rank, so let's enable that language extension:

{-# LANGUAGE RankNTypes #-}

First, we can make apply id work:

apply :: (forall a. a -> a) -> D a b -> D a b
apply f (D x y) = D (f x) (f y)

However, now id is the only function with which apply works (all total functions of type forall a. a -> a are equal to id).

Here's another type:

apply :: (forall a. a -> (c, c)) -> D a b -> D c c
apply f (D x y) = D (f x) (f y)

But this too comes at a price. Now the f-s can only be constant functions that ignore the previous fields of D. So apply (const (0, 0)) works, but we have no way to inspect the argument of f.

In contrast, the inferred type is pretty useful. We can express transformations with it that look at the actual data contained in D.

At this point, we might ask: why does GHC infer what it infers? After all, some functions work with the alternative types, but don't work with the default type. Could it be better to sometimes infer higher-ranked types? Well, such types are often extremely useful, but inferring them is unfeasible.

Type inference for rank-2 types is rather complicated, and not very practical either, because it's not possible to infer most general types. With rank-1 inference, we can infer a type that is more general than all other valid types for the same expression. There's no such guarantee with rank-2 types. And inference for rank-3 and above types is just undecidable.

For these reasons, GHC sticks to rank-1 inference, so it never infers types with forall-s inside function arguments.

Upvotes: 8

Related Questions