Limit the type family restriction to “a couple”,

Question

Consider the following, where I am trying to say: " ais a couple":

type family F t a :: Constraint
type instance F Int a = (a ~ (a1, a2))

It does not work, because both a1, and a2are not included in the scope, but is there a way to express it?

Of course, in the signature function I can write the type of restrictions (a ~ (a1, a2)), even if a1and a2not mentioned elsewhere, but I need to put it in the signature copy function, which, of course, is determined by the class. And ain this case is not an option for most instance, a copy function, the same as Functoris fas a class option instead aand bso I can not add further restrictions to the instance of the proposal.

Answer 1

Yes! You can do it!

Strong, somewhat built-up version

First, a few useful types of families:

type family Fst a where
  Fst (x,y) = x

type family Snd a where
  Snd (x,y) = y

Now the one you need:

type IsPair a = a ~ (Fst a, Snd a)

Here's the test:

type family Con a where
  Con (f x y) = f

test :: IsPair a => proxy a -> Con a :~: (,)
test _ = Refl

And even simpler, which checks for a stronger property:

 test1 :: IsPair a => a -> Fst a
 test1 = fst

And just to make sure he is satisfied when it should be:

data Dict c where
  Dict :: c => Dict c

test2 :: Dict (IsPair (a, b))
test2 = Dict

You can, of course, use this to define yours F:

type family F t a
type instance F Int a = IsPair a

Much simpler but much less powerful

type family Con a where
  Con (f x y) = f
type IsPair a = Con a ~ (,)

The problem with this, compared to the first approach, is that it actually does not give you glorious knowledge about that a ~ (Fst a, Snd a). Therefore, he makes an expression, but you cannot do much with him.

A little generalization

? PolyKinds , :

type family Arg1 a where Arg1 (f x) = x
type family Arg2 a where Arg2 (f y x) = y
type family Arg3 a where Arg3 (f z y x) = z
type family Arg4 a where Arg4 (f w z y x) = w

type family IsF (f :: k) (a :: *) :: Constraint
type instance IsF f a = a ~ f (Arg1 a)
type instance IsF f a = a ~ f (Arg2 a) (Arg1 a)
type instance IsF f a = a ~ f (Arg3 a) (Arg2 a) (Arg1 a)
type instance IsF f a = a ~ f (Arg4 a) (Arg3 a) (Arg2 a) (Arg1 a)

PolyKinds, IsF1, IsF2 ..

,

type IsPair a = IsF (,) a
type IsMaybe a = IsF Maybe a
...

( GHC 7.10 , ).

data Dict c where
  Dict :: c => Dict c

test1 :: Dict (IsF f (f a))
test1 = Dict

test2 :: Dict (IsF f (f a b))
test2 = Dict

test3 :: Dict (IsF f (f a b c))
test3 = Dict

test4 :: Dict (IsF f (f a b c d))
test4 = Dict