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

2009-06-07 Thread Vladimir Reshetnikov 
Hi Zsolt,

fs :: (((a, a) - a) - t) - (t, t)
fs g = (g fst, g snd)
examples = (fs fmap, fs liftA, fs liftM, fs id, fs ($(1,2)), fs
((,)id), fs (:[]), fs repeat)

No instance for (Num [Char])
  arising from the literal `1' at M.hs:6:54
Possible fix: add an instance declaration for (Num [Char])
In the expression: 1
In the second argument of `($)', namely `(1, 2)'
In the first argument of `fs', namely `($ (1, 2))'

Anyways, this signature is not what intended. I want it to work for
all tuples, regardless of their element types.

Thanks
Vladimir

On 6/7/09, Zsolt Dollenstein zsol.z...@gmail.com wrote:
 On Sun, Jun 7, 2009 at 9:17 AM, Vladimir
 Reshetnikovv.reshetni...@gmail.com wrote:
 Hi Zsolt,

 It does not compiles with GHC without type annotations.

 It does with mine: The Glorious Glasgow Haskell Compilation System, version
 6.10.2

 Anyway, try this: fs :: (((a, a) - a) - t) - (t, t)


 Thanks,
 Vladimir

 On 6/7/09, Zsolt Dollenstein zsol.z...@gmail.com wrote:
 Hi Vladimir,

 On Sun, Jun 7, 2009 at 12:06 AM, Vladimir
 Reshetnikovv.reshetni...@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?

 Have you tried putting the above into ghci for example, then asking for
 :t
 fs?
 Or am I misunderstanding your point?

 Cheers,
 Zsolt

 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





___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

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

2009-06-07 Thread 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
Reshetnikovv.reshetni...@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@haskell.org
 http://www.haskell.org/mailman/listinfo/haskell-cafe

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

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

2009-06-07 Thread 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
Reshetnikovv.reshetni...@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.s...@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
 Reshetnikovv.reshetni...@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@haskell.org
 http://www.haskell.org/mailman/listinfo/haskell-cafe



___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

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

2009-06-07 Thread Wouter Swierstra 

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?


As you said yourself, you need to add a type signature to fs:


{-# LANGUAGE RankNTypes #-}




fs :: ((forall a . ((a, a) - a)) - t) - (t, t)
fs g = (g fst, g snd)

examples = (fs id, fs repeat, fs (\x - [x]), fs ((,)id))



Hope this helps,

  Wouter


This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

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

2009-06-07 Thread Ryan Ingram 
The most interesting example is

fs ($ (1, 2))

Which I haven't been able to make typecheck.

Here's some well-typed code:

 fs2 f g = (f fst, g snd)
 ab f = f ('a', b)
 test = fs2 ab ab
 -- test2 = fs ab

The question is, is it possible to write fs such that your examples
typecheck and test2 also typechecks?

I find this example interesting because it's the smallest example I've
seen of a well-typed program which would just work in Scheme or
Lisp, but which we can't assign a type to in Haskell.

  -- ryan

On Sun, Jun 7, 2009 at 9:20 AM, Wouter Swierstraw...@cs.nott.ac.uk wrote:
 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?

 As you said yourself, you need to add a type signature to fs:

 {-# LANGUAGE RankNTypes #-}


 fs :: ((forall a . ((a, a) - a)) - t) - (t, t)
 fs g = (g fst, g snd)

 examples = (fs id, fs repeat, fs (\x - [x]), fs ((,)id))


 Hope this helps,

  Wouter


 This message has been checked for viruses but the contents of an attachment
 may still contain software viruses, which could damage your computer system:
 you are advised to perform your own checks. Email communications with the
 University of Nottingham may be monitored as permitted by UK legislation.

 ___
 Haskell-Cafe mailing list
 Haskell-Cafe@haskell.org
 http://www.haskell.org/mailman/listinfo/haskell-cafe

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Haskell-cafe] Question on rank-N polymorphism

2009-06-06 Thread Vladimir Reshetnikov 
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