Re: [Haskell-cafe] Question on rank-N polymorphism

Well, I don't really recommend programming in dependently typed languages right now :) But if you must, Agda has been getting a lot of attention recently. Also, the theorem prover Coq is based on the dependently-typed lambda calculus. In Haskell, giving a function an intersection type is generally done with typeclasses. You can write, for example: class Fs a where type FsResult a fs :: a -> FsResult a data Fmap = Fmap instance Fs Fmap where type FsResult a = forall f a b. Functor f => (f (a,b) -> f a, f (a,b) -> f b) fs Fmap = (fmap fst, fmap snd) (although this seems unusable to me!) You can also use Template Haskell to copy the argument: -- I may have the syntax wrong here fs :: a -> Q Exp fs a = [e| ($a fst, $a snd) ] test :: (Int, String) test = $(fs (`id` (1,"2")) -- ryan On Sun, Jun 7, 2009 at 2:28 AM, Vladimir Reshetnikov wrote:

Hi Ryan,

Thanks for your explanation. What language with dependent types would you recommend me to look at?

Now I am studying rank-N polymorphism in Haskell and trying to generalize some combinators in my libraries to multitypes. This is how I came to this question.

Thanks, Vladimir

On 6/7/09, Ryan Ingram wrote:

...

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 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@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe