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
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) -
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
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
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
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)