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
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
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
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.
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 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
participants (3)
-
Ryan Ingram -
Vladimir Reshetnikov -
Wouter Swierstra