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.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 >> Reshetnikov<v.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
