[Haskell-cafe] Question on rank-N polymorphism

[Ryan Ingram]

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<v.reshetnikov at gmail.com> 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 <ryani.spam at gmail.com> 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<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
>>>
>>
>