[Haskell-cafe] Question on rank-N polymorphism

[Ryan Ingram]

This is a really interesting question.

So, fs is well-typed in Haskell:
   fs :: (((a,a) -> a) -> t) -> (t,t)
i.e.
   fs id :: ((a,a) -> a, (a,a) -> a)

However, I believe what you are asking is for fs to be equivalent to
the following:
> fs2 f g = (f fst, g snd)

which has the type
fs2 :: (((a, b) -> a) -> t) -> (((a1, b1) -> b1) -> t1) -> (t, t1)

except with the argument broadcast polymorphically to both positions.

This means the argument must have the multitype

g :: ((a,b) -> a) -> t  /\  ((a1,b1) -> b1) -> t1

for some t and t1 which are functions of a,b and a1,b1.

Unfortunately I don't believe it is possible to encode this type in
System F or System F(c), the underlying lambda-calculus used by GHC,
so Haskell isn't going to be able to solve this problem.  But there
are statically typed languages which can solve this problem.

You can take the big hammer of dependent types, and write fs something
like this (not Haskell; this is a dependently-typed language):

typeof_g :: (Type -> Type -> Type -> Type) -> Type
typeof_g res_type = (a :: Type) -> (b :: Type) -> (c :: Type) ->
((a,b) -> c) -> res_type a b c

fs :: (res_type :: Type -> Type -> Type -> Type) -> (g :: typeof_g res_type)
  -> (a :: Type) -> (b :: Type) -> (res_type a b a, res_type a b b)
fs _ g a b = (g a b a fst, g a b b snd)

So, you'd write fs id like this:
> fs (\a b c. (a,b) -> c) (\a b c. id ((a,b) -> c))

This is a fascinating problem, though.  What put you on this path?

  -- ryan

On Sat, Jun 6, 2009 at 3:06 PM, Vladimir
Reshetnikov<v.reshetnikov at gmail.com> wrote:
> Hi,
>
> I have the following code:
>
> --------------------------------------------------------------------------------
> fs g = (g fst, g snd)
> examples = (fs fmap, fs liftA, fs liftM, fs id, fs ($(1,"2")), fs
> ((,)id), fs (:[]), fs repeat)
> --------------------------------------------------------------------------------
>
> The idea is that fs accepts a polymorphic function as its argument.
> What type signature can I specify for f in order to compile this code?
> If it is not possible in Haskell, is there another language with
> static typing which allows this?
>
> Thanks,
> Vladimir
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>