[Haskell-cafe] Aren't type system extensions fun?
Andrew Coppin
understand very well.
GHC provides a vast zoo of strange and perplexing type system
extensions, which I don't understand at all. (Well, some of it is simple
enough - e.g., multiparameter type classes. But GADTs? FDs? ATs? Hmm...)
Anyway, it seems there is a large set of such type system extensions
that involve writing "forall" all over the place. I have by now more or
less managed to comprehend the fact that
data Thing = forall x. Thing x
allows a type variable to appear on the RHS that is *not* present on the
LHS, thus "hiding" the type of something inside the structure. And for
some reason, they call this "existential quantification" [which I can't
spell never mind pronounce].
Today I was reading a potentially interesting paper, and I stumbled
across something referred to as a "rank-2 type". Specifically,
class Typable x => Term x where
gmapT :: (forall y. Term y => y -> y) -> x -> x
At this point, I am at a complete loss as to how this is any different from
gmapT :: Term y => (y -> y) -> x -> x
Can anybody enlighten me?
This is probably the first real use I've ever seen of so-called rank-2
types, and I'm curios to know why people think they need to exist.
[Obviously when somebody vastly more intelligent than me says something
is necessary, they probably know something I don't...]
At this point, I don't think I even wanna *know* what the hell a rank-N
type is... o_O
_______________________________________________
Haskell-Cafe mailing list
Haskel...@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Don Stewart
>
> Today I was reading a potentially interesting paper, and I stumbled
> across something referred to as a "rank-2 type". Specifically,
>
> class Typable x => Term x where
> gmapT :: (forall y. Term y => y -> y) -> x -> x
>
> At this point, I am at a complete loss as to how this is any different from
>
> gmapT :: Term y => (y -> y) -> x -> x
>
> Can anybody enlighten me?
If in doubt, consult the fine user's guide:
Section 8.7.4. Arbitrary-rank polymorphism
http://www.haskell.org/ghc/docs/latest/html/users_guide/other-type-extensions.html#universal-quantification
-- Don
Thomas Davie
This is perhaps best explained with an example of something that can
be typed with rank-2 types, but can't be typed otherwise:
main = f id 4
f g n = (g g) n
We note that the same instance of id must be made to have both the
type (Int -> Int) and ((Int -> Int) -> (Int -> Int)) at the same
time. Rank 2 types allows us to do this.
Bob
Miguel Mitrofanov
> gmapT :: (forall y. Term y => y -> y) -> x -> x
In "gmapT f x" the function f must be of type "forall y. Termy => y ->
y". That means that for EACH type y which is an instance of "Term"
class, f maps y to y. You can't do something like "gmapT (+ 1) x",
since (+ 1) is not general enough.
However, if, say, Term class provides a method
class Term a where
...
pnt :: a
...
then you CAN do, for example, "gmapT (const pnt) x", since the type of
"const pnt" is general enough (and even more general).
> At this point, I am at a complete loss as to how this is any
> different from
>
> gmapT :: Term y => (y -> y) -> x -> x
Here you CAN do "gmapT (+ 1) x", assuming that, say, Int is an
instance of Term class.
Andrew Coppin
> This is perhaps best explained with an example of something that can
> be typed with rank-2 types, but can't be typed otherwise:
>
> main = f id 4
>
> f g n = (g g) n
>
> We note that the same instance of id must be made to have both the
> type (Int -> Int) and ((Int -> Int) -> (Int -> Int)) at the same
> time. Rank 2 types allows us to do this.
What a perplexing example! :-}
Well anyway, I was under the impression that id :: x -> x, so I'm not
really sure why this wouldn't work without Rank-2 types...
Bulat Ziganshin
Tuesday, May 27, 2008, 1:02:06 AM, you wrote:
> Today I was reading a potentially interesting paper, and I stumbled
> across something referred to as a "rank-2 type". Specifically,
existentials and polymorphic values are complement each other.
existential contains *some* type of given class. polymorphic function
can deal with *any* value of given class. so the only thing you can do
with existential value is to apply polymorphic function to it
f :: Class x => x -> Int
is [order-1] polymorphic function which may be applied to any type of
given class. higher-order function that receives order-n polymorphic
function as its argument called polymorphic function of order n+1:
ff :: (Class x => x -> Int) -> Int
its first argument is a *function*. polymorphic function. so you need
to call it with polymorphic function which is able to deal with *any*
value of given class. it's very different to polymorphic function:
g :: Class x => x -> Int -> Int
which accepts any value of given class. in the last case you have
polymorphic function that you can use with any value, in the first case
you need to provide yourself polymorphic function as argument
look at http://haskell.org/haskellwiki/GADTs_for_dummies
it should be helpful to understand type extensions machinery
--
Best regards,
Bulat mailto:Bulat.Z...@gmail.com
Philippa Cowderoy
> Thomas Davie wrote:
> > This is perhaps best explained with an example of something that can be
> > typed with rank-2 types, but can't be typed otherwise:
> >
> > main = f id 4
> >
> > f g n = (g g) n
> >
> > We note that the same instance of id must be made to have both the type (Int
> > -> Int) and ((Int -> Int) -> (Int -> Int)) at the same time. Rank 2 types
> > allows us to do this.
>
> What a perplexing example! :-}
>
> Well anyway, I was under the impression that id :: x -> x, so I'm not really
> sure why this wouldn't work without Rank-2 types...
>
Because f's type can't be written as a rank-1 type - its parameter g must
be polymorphic (forall x. x->x). With rank-1 types, all the instantiation
is done by the caller - the function can't require that it receive
polymorphic parameters.
Sometimes you gotta fight fire with fire. Most
of the time you just get burnt worse though.
Eric Stansifer
> sure why this wouldn't work without Rank-2 types...
The matter at hand is the type of the function /f/, not of the
function /id/. I'll address the question of applying /f/ to /id/ at
the end, but the interesting question is how to assign a type to /f/
at all.
In Bob's example,
f g x = (g g) x
let us try to give /f/ a type.
The rank-1 type we might first attempt is:
f :: (a -> a) -> a -> a
(which is the same thing as /f :: forall a. (a -> a) -> a -> a/). But
under this type, we would have /g :: a -> a/, and then the expression
/g g/ is illegal.
If we try again,
f :: ((a -> a) -> (a -> a)) -> a -> a
we again find that the expression /g g/ is illegal. Experimenting
further along this line will quickly convince you of the difficulty of
typing /f/.
However, it can be done using rank-2 types:
> f :: (forall a. a -> a) -> b -> b
> f g x = (g g) x
In the expression /g g/, both /g/s have the same rank-1 type /forall
a. a -> a/ (which is the same as the type /a -> a/); in the second
usage of /g/, we assign /b/ to the type variable /a/, and in the first
usage of /g/, we assign /b -> b/ to the type variable /a/. (Thus, the
second usage of /g/ has type /a -> a/, and the first usage has type
/(a -> a) -> (a -> a)/.) This is the essential point of the /forall
a/ -- it allows the type variable /a/ to be instantiated differently
as /g/ is used in different places. In other words, it is
polymorphic.
Going back to /id/, recall that
id :: a -> a
which is the same thing as
id :: forall a. a -> a
(i.e., /id/ is a polymorphic function). Since the type of /id/
unifies with the first argument of /f/, the function application /f
id/ is well-typed.
Note that we could "simplify" Bob's example down to:
f2 g = g g
although the type of this /f2/ is less pleasant:
f2 :: (forall a. a -> a) -> (forall a. a -> a)
Say, wouldn't a syntax like "(forall a => a -> a)" or "(a => a -> a)"
or something similar to that be more consistent with syntax for
contexts, e.g. "(Ord a => a -> a)"?
Eric
Derek Elkins
> Say, wouldn't a syntax like "(forall a => a -> a)" or "(a => a -> a)"
> or something similar to that be more consistent with syntax for
> contexts, e.g. "(Ord a => a -> a)"?
It's not remotely the same thing as a class constraint so why would we
want it to be "consistent" with it?
Eric Stansifer
>> or something similar to that be more consistent with syntax for
>> contexts, e.g. "(Ord a => a -> a)"?
>
> It's not remotely the same thing as a class constraint so why would we
> want it to be "consistent" with it?
Well, true; the idea come from when I read just now in the ghc manual
that the following are equivalent:
> data T = MkT (Ord a => a -> a)
> data U = MkU (forall a. Ord a => a -> a)
In other words, the context "Ord a" in the /T/ definition is
implicitly carrying a "forall a" around with it. In a sense, one can
think of "forall a" as a class constraint for /a/ that offers no
constraints at all; i.e., "forall a" is satisfied by any type /a/,
whereas "Ord a", for example, is satisfied by any type /a/ which has
an instance for /Ord/.
To be exact, here is the analogy I'm making.
Suppose we have:
> class F a => C1 a
> class C2 a
Then:
((F a, C1 a) => a -> a) is to (C1 a => a -> a)
as
(forall a. C2 a => a -> a) is to (C2 a => a -> a)
That is, /forall a/ acts like a constraint that always succeeds (and
is thus usually implicit -- e.g., in the line "class C2 a").
The analogy, of course, breaks down the moment one writes:
> -- t :: (Ord a => a -> a) -> T
> -- t = MkT
>
> u :: (forall a. Ord a => a -> a) -> U
> u = MkU
where for very good reasons the type signatures written for /t/ and
/u/ above mean entirely different things.
So, the similarity is rather tenuous, and is further diminished
because the "forall a" construct and the "Ord a" construct are used
for entirely different things in practice, regardless of some nice,
abstract connection that I see between them. But I hope you see why I
feel that "forall a" is in some ways closely related to "Ord a".
[Incidentally, I also don't like introducing new syntax (though
introducing new syntax is better than abusing existing syntax).]
On another note: the ghc 6.6.1 manual says (as does the latest
manual, but I have version 6.6.1, so that's what matters here) in
section 7.4.8.1 that the following are equivalent:
> data T a = MkT (Either a b) (b -> b)
> data T a = MkT (forall b. Either a b) (forall b. b -> b)
but for me, the first line does not compile with -fglasgow-exts (I
get: "Not in scope: type variable `b'"), but the second line does
compile. Am I missing something here?
Eric
Derek Elkins
> >> Say, wouldn't a syntax like "(forall a => a -> a)" or "(a => a -> a)"
> >> or something similar to that be more consistent with syntax for
> >> contexts, e.g. "(Ord a => a -> a)"?
> >
> > It's not remotely the same thing as a class constraint so why would we
> > want it to be "consistent" with it?
>
> Well, true; the idea come from when I read just now in the ghc manual
> that the following are equivalent:
>
> > data T = MkT (Ord a => a -> a)
> > data U = MkU (forall a. Ord a => a -> a)
>
> In other words, the context "Ord a" in the /T/ definition is
> implicitly carrying a "forall a" around with it. In a sense, one can
> think of "forall a" as a class constraint for /a/ that offers no
> constraints at all; i.e., "forall a" is satisfied by any type /a/,
> whereas "Ord a", for example, is satisfied by any type /a/ which has
> an instance for /Ord/.
It's not "carrying a forall" around with it. The fact that 'a' is
otherwise unbound leads GHC to insert a 'forall a'. That's another way
in which forall and class constraints aren't remotely the same. forall
is a binding construct that introduces a new type variable, a class
constraint is not a binding construct.
Doesn't work for me either which kind of relieves me as I don't
particularly like that interpretation.
Gleb Alexeyev
> What a perplexing example! :-}
For a bit less mind-boggling example, try meditating about the next two
functions. It may be instructive to comment out type signatures and see
what happens.
{-# OPTIONS -fglasgow-exts #-}
foo :: (forall a . a -> a) -> (Bool, String)
foo g = (g True, g "bzzt")
bar :: (forall a . Num a => a) -> (Integer, Float)
bar x = (x `div` 3, x / 3)
In a nutshell, rank-N typing is simple. Rank-1 polymorphism allows us to
type functions like map, foldr etc we all know and love. Rank-1
polymorphic types contain type variables that may be instantiated with
any monomorphic type (e.g., Int, String, etc). Rank-2 polymorphic
functions accept rank-1 polymorphic values as argument. Rank-N
polymorphic functions accept rank-(N-1) polymorphic values as argument.
As a practical example of the need for higher-rank polymorphism you may
want to read about ST monad.
Chris Smith
> This is perhaps best explained with an example of something that can be
> typed with rank-2 types, but can't be typed otherwise:
>
> main = f id 4
>
> f g n = (g g) n
That's certainly interesting. Here's another interesting example. In an
old blog post of mine...
http://cdsmith.wordpress.com/2007/11/29/some-playing-with-derivatives/
I was doing my first playing around with automatic differentiation. It
turns out that the type that's inferred for the AD function diff there
can sometimes lead to incorrect behavior. Barak Pearlmutter pointed out
such a case in the comments:
diff (\x -> (diff (x*) 2)) 1
This mixes several variables on which one is performing a derivative, and
leads to confusion between the various derivatives. The result is a
wrong answer. The version with rank 2 types, which are the types you
really want here, catches this error at compile time. (Granted, it would
be nice to get the correct answer; but an error is infinitely superior to
the wrong answer!)
As I mentioned in the article, though, rank 2 types have their own
problems, in that one needs many versions of the function: one for each
subclass of Num.
--
Chris
Andrew Coppin
> foo :: (forall a . a -> a) -> (Bool, String)
> foo g = (g True, g "bzzt")
So, after an entire day of boggling my mind over this, I have brought it
down to one simple example:
(id 'J', id True) -- Works perfectly.
\f -> (f 'J', f True) -- Fails miserably.
Both expressions are obviously perfectly type-safe, and yet the type
checker stubbornly rejects the second example. Clearly this is a flaw in
the type checker.
So what is the type of that second expression? You would think that
(x -> x) -> (Char, Bool)
as a valid type for it. But alas, this is not correct. The CALLER is
allowed to choose ANY type for x - and most of possible choices wouldn't
be type-safe. So that's no good at all!
In a nutshell, the function being passed MAY accept any type - but we
want a function that MUST accept any type. This excusiatingly subtle
distinction appears to be the source of all the trouble.
Interestingly, if you throw in the undocumented "forall" keyword,
everything magically works:
(forall x. x -> x) -> (Char, Bool)
Obviously, the syntax is fairly untidy. And the program is now not valid
Haskell according to the written standard. And best of all, the compiler
seems unable to deduce this type automatically either.
At this point, I still haven't worked out exactly why this hack works.
Indeed, I've spent all day puzzling over this, to the point that my head
hurts! I have gone through several theories, all of which turned out to
be self-contradictory. So far, the only really plausible theory I have
been able to come up with is this:
- A function starts out with a polymorphic type, such as 'x -> x'.
- Each time the function is called, all the type variables have to be
locked down to real types such as 'Int' or 'Either (Maybe (IO Int))
String' or something.
- By the above, any function passed to a high-order function has to have
all its type variables locked down, yielding a completely monomorphic
function.
- In the exotic case above, we specifically WANT a polymorphic function,
hence the problem.
- The "forall" hack somehow convinces the type checker to not lock down
some of the type variables. In this way, the type variables relating to
a function can remain unlocked until we reach each of the call sites.
This allows the variables to be locked to different types at each site
[exactly as they would be if the function were top-level rather than an
argument].
This is a plausible hypothesis for what this language feature actually
does. [It is of course frustrating that I have to hypothesise rather
than read a definition.] However, this still leaves a large number of
questions unanswered...
- Why are top-level variables and function arguments treated differently
by the type system?
- Why do I have to manually tell the type checker something that should
be self-evident?
- Why do all type variables need to be locked down at each call site in
the first place?
- Why is this virtually never a problem in real Haskell programs?
- Is there ever a situation where the unhacked type system behaviour is
actually desirably?
- Why can't the type system automatically detect where polymorphism is
required?
- Does the existence of these anomolies indicate that Haskell's entire
type system is fundamentally flawed and needs to be radically altered -
or completely redesigned?
Unfortunately, the GHC manual doesn't have a lot to say on the matter.
Reading section 8.7.4 ("Arbitrary-rank polymorphism"), we find the
following:
- "The type 'x -> x' is equivilent to 'forall x. x -> x'." [Um... OK,
that's nice?]
- "GHC also allows you to do things like 'forall x. x -> (forall y. y ->
y)'." [Fascinating, but what does that MEAN?]
- "The forall makes explicit the universal quantification that is
implicitly added by Haskell." [Wuh??]
- "You can control this feature using the following language options..."
[Useful to know, but I still don't get what this feature IS.]
The examples don't help much either, because (for reasons I haven't
figured out yet) you apparently only need this feature in fairly obscure
cases.
The key problem seems to be that the GHC manual assumes that anybody
reading it will know what "universal quantification" actually means.
Unfortunately, neither I nor any other human being I'm aware of has the
slightest clue what that means. A quick search on that infallable
reference [sic] Wikipedia yields several articles full of dense logic
theory. Trying to learn brand new concepts from an encyclopedia is more
or less doomed from the start. As far as I can comprehend it, we have
existential quantification = "this is true for SOMETHING"
universal quantification = "this is true for EVERYTHING"
Quite how that is relevant to the current discussion eludes me.
I have complete confidence that whoever wrote the GHC manual knew
exactly what they meant. I am also fairly confident that this was the
same person who implemented and even designed this particular feature.
And that they probably have an advanced degree in type system theory. I,
however, do not. So if in future the GHC manual could explain this in
less opaque language, that would be most appreciated. :-}
For example, the above statements indicate that '(x -> x) -> (Char,
Bool)' is equivilent to 'forall x. (x -> x) -> (Char, Bool)', and we
already know that this is NOT the same as '(forall x. x -> x) -> (Char,
Bool)'. So clearly my theory above is incomplete, because it fails to
explain why this difference exists. My head hurts...
(Of course, I could just sit back and pretend that rank-N types don't
exist. But I'd prefer to comprehend them if possible...)
Don Stewart
> Gleb Alexeyev wrote:
> >foo :: (forall a . a -> a) -> (Bool, String)
> >foo g = (g True, g "bzzt")
>
> So, after an entire day of boggling my mind over this, I have brought it
> down to one simple example:
>
> (id 'J', id True) -- Works perfectly.
>
> \f -> (f 'J', f True) -- Fails miserably.
>
> Both expressions are obviously perfectly type-safe, and yet the type
> checker stubbornly rejects the second example. Clearly this is a flaw in
> the type checker.
I'm sorry you are still confused, Andrew.
This is documented rather nicely in section 8.7.4.2 of
the GHC user's guide. In particularly, you'll want to not ethat
arbitrary rank type inference is undecidable, so GHC imposes a
simple rule requiring you to annotate those polymorphic parameters
of higher rank you want.
See here
http://www.haskell.org/ghc/docs/latest/html/users_guide/other-type-extensions.html#id408394
Read this carefully, and then read the references.
> Interestingly, if you throw in the undocumented "forall" keyword,
> everything magically works:
>
> (forall x. x -> x) -> (Char, Bool)
>
> Obviously, the syntax is fairly untidy. And the program is now not valid
> Haskell according to the written standard. And best of all, the compiler
> seems unable to deduce this type automatically either.
Please read the above link. In particular, pay attention to the word
"undecidable". Reading and comprehending Odersky and Laufer's paper, "Putting
type annotations to work", will explain precisely why you're butting
your head up against deciability.
-- Don
Chaddaï Fouché
> Gleb Alexeyev wrote:
>>
>> foo :: (forall a . a -> a) -> (Bool, String)
>> foo g = (g True, g "bzzt")
>
> So, after an entire day of boggling my mind over this, I have brought it
> down to one simple example:
>
> (id 'J', id True) -- Works perfectly.
>
> \f -> (f 'J', f True) -- Fails miserably.
>
> Both expressions are obviously perfectly type-safe, and yet the type checker
> stubbornly rejects the second example. Clearly this is a flaw in the type
> checker.
No, this is a flaw in the type inferencer, but simply adding the
Rank-N type to our type system makes type inference undecidable.
I would argue against the "obviously perfectly type-safe" too since
most type system don't even allow for the second case.
> So what is the type of that second expression? You would think that
>
> (x -> x) -> (Char, Bool)
>
> as a valid type for it. But alas, this is not correct. The CALLER is allowed
> to choose ANY type for x - and most of possible choices wouldn't be
> type-safe. So that's no good at all!
None of the possible choice would be type-safe. This type means :
whatever the type a, function of type (a -> a) to a pair (Char, Bool)
But the type a is unique while in the body of your function, a would
need to be two different types.
> Interestingly, if you throw in the undocumented "forall" keyword, everything
> magically works:
>
> (forall x. x -> x) -> (Char, Bool)
>
> Obviously, the syntax is fairly untidy. And the program is now not valid
> Haskell according to the written standard. And best of all, the compiler
> seems unable to deduce this type automatically either.
As I said, the compiler can't deduce this type automatically because
it would make type inference undecidable.
> At this point, I still haven't worked out exactly why this hack works.
> Indeed, I've spent all day puzzling over this, to the point that my head
> hurts! I have gone through several theories, all of which turned out to be
> self-contradictory. So far, the only really plausible theory I have been
> able to come up with is this:
Rank-N type aren't a "hack", they're perfectly understood and fit
nicely into the type system, their only problem is type inference.
> yada yada, complicated theory... cut
What you don't seem to understand is that "(x -> x) -> (Char, Bool)"
and "(forall x. x -> x) -> (Char, Bool)" are two very different
beasts, they aren't the same type at all !
Taking a real world situation to illustrate the difference :
Imagine you have different kind of automatic washer, some can wash
only wool while others can wash only cotton and finally some can wash
every kind of fabric...
You want to do business in the washing field but you don't have a
washer so you publish an announce :
If your announce say "whatever the type of fabric x, give me a machine
that can wash x and all you clothes and I'll give you back all your
clothes washed", the customer won't be happy when you will give him
back his wool clothes that the cotton washing machine he gave you torn
to shreds...
What you really want to say is "give me a machine that can wash any
type of fabric and your clothes and I'll give you back your clothes
washed".
The first announce correspond to "(x -> x) -> (Char, Bool)", the
second to "(forall x. x -> x) -> (Char, Bool)"
> - Why are top-level variables and function arguments treated differently by
> the type system?
They aren't (except if you're speaking about the monomorphism
restriction and that's another subject entirely).
> - Why do I have to manually tell the type checker something that should be
> self-evident?
Because it isn't in all cases to a machine, keep in mind you're an
human and we don't have real IA just yet.
> - Why is this virtually never a problem in real Haskell programs?
Because we seldom needs Rank-2 polymorphism.
> - Is there ever a situation where the unhacked type system behaviour is
> actually desirably?
Almost everytime. Taking a simple example : map
If the type of map was "(forall x. x -> x) -> [a] -> [a]", you could
only pass it "id" as argument, if it was "(forall x y. x -> y) -> [a]
-> [b]", you couldn't find a function to pass to it... (No function
has the type "a -> b")
> - Why can't the type system automatically detect where polymorphism is
> required?
It can and does, it can't detect Rank-N (N > 1) polymorphism because
it would be undecidable but it is fine with Rank-1 polymorphism (which
is what most people call polymorphism).
> - Does the existence of these anomolies indicate that Haskell's entire type
> system is fundamentally flawed and needs to be radically altered - or
> completely redesigned?
Maybe this should suggest to you that it is rather your understanding
of the question that is flawed... Haskell's type system is a fine
meshed mechanism that is soundly grounded in logic and mathematics, it
is rather unlikely that nobody would have noted the problem if it was
so important...
--
Jedaď
Kim-Ee Yeoh
Andrew Coppin wrote:
>
> So, after an entire day of boggling my mind over this, I have brought it
> down to one simple example:
>
> (id 'J', id True) -- Works perfectly.
> \f -> (f 'J', f True) -- Fails miserably.
>
> Both expressions are obviously perfectly type-safe, and yet the type
> checker stubbornly rejects the second example. Clearly this is a flaw in
> the type checker.
>
> So what is the type of that second expression? You would think that
> (x -> x) -> (Char, Bool)
> as a valid type for it. But alas, this is not correct. The CALLER is
> allowed to choose ANY type for x - and most of possible choices wouldn't
> be type-safe. So that's no good at all!
>
> In a nutshell, the function being passed MAY accept any type - but we
> want a function that MUST accept any type. This excusiatingly subtle
> distinction appears to be the source of all the trouble.
>
Let's fill in the type variable: (x -> x) -> (Char, Bool) ==>
forall x. (x -> x) -> (Char, Bool) ==> x_t -> (x -> x) -> (Char, Bool),
where x_t is the hidden type-variable, not unlike the reader monad.
As you've pointed out, callER chooses x_t, say Int when
passing in (+1) :: Int -> Int, which obviously would break
\f -> (f 'J', f True).
What we want is the callEE to choose x_t since callEE needs to
instantiate x_t to Char and Bool. What we want is
(x_t -> x -> x) -> (Char, Bool).
But that's just
(forall x. x -> x) -> (Char, Bool).
For completeness' sake, let me just state that if universal
quantification is like (x_t -> ...), then existential quantification
is like (x_t, ...).
Andrew Coppin wrote:
>
> At this point, I still haven't worked out exactly why this hack works.
> Indeed, I've spent all day puzzling over this, to the point that my head
> hurts! I have gone through several theories, all of which turned out to
> be self-contradictory.
>
My sympathies. You may find the haskell-cafe archive to be
as useful as I have (search Ben Rudiak-Gould or Dan Licata).
Having said that, I think you've done pretty well on your own.
Andrew Coppin wrote:
>
> - Why can't the type system automatically detect where polymorphism is
> required?
> - Does the existence of these anomolies indicate that Haskell's entire
> type system is fundamentally flawed and needs to be radically altered -
> or completely redesigned?
>
Well, give it a try! I'm sure I'm not the only one interested in
your type inference experiments. Warning: they're addictive
and may lead to advanced degrees and other undesirable
side-effects.
-- Kim-Ee
--
View this message in context: http://www.nabble.com/Aren%27t-type-system-extensions-fun--tp17479349p17498362.html
Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com.
Darrin Thompson
> Let's fill in the type variable: (x -> x) -> (Char, Bool) ==>
> forall x. (x -> x) -> (Char, Bool) ==> x_t -> (x -> x) -> (Char, Bool),
> where x_t is the hidden type-variable, not unlike the reader monad.
>
> As you've pointed out, callER chooses x_t, say Int when
> passing in (+1) :: Int -> Int, which obviously would break
> \f -> (f 'J', f True).
>
> What we want is the callEE to choose x_t since callEE needs to
> instantiate x_t to Char and Bool. What we want is
> (x_t -> x -> x) -> (Char, Bool).
> But that's just
> (forall x. x -> x) -> (Char, Bool).
>
Nice. That's the first time any of this really made sense to me. Is it
possible to construct valid argument for that function?
--
Darrin
Isaac Dupree
>> - Why are top-level variables and function arguments treated differently by
>> the type system?
>
> They aren't
In a sense, they are.
id :: (forall a. a -> a)
useId :: (forall a. a -> a) -> (Int,Bool)
brokenUseId :: (forall a. (a -> a) -> (Int,Bool))
brokenUseId :: (a -> a) -> (Int,Bool)
Note that polymorphic variables in function argument types scope over
the function results too by default. And that's a good thing. Otherwise,
id :: a -> a
would be understood as
brokenId :: (forall a. a) -> (forall a. a)
which is not at all intended ("id" specialized to _|_ values only).
Basically, you only want higher-rank types in Haskell when you know what
you're doing: due to parametric polymorphism it is less often useful to
apply an argument function to, e.g., both Int and Bool than you might
find in Python, for example. In Haskell, more often you would just take
two functions as arguments e.g.
useFunctions :: (Int -> Int) -> (Bool -> Bool) -> (Int,Bool)
or more interestingly, let's make the caller be able to choose any kind
of number:
useFunctions2 :: (Num a) => (a -> a) -> (Bool -> Bool) -> (a,Bool)
a.k.a.
useFunctions2 :: forall a. (Num a) => (a -> a) -> (Bool -> Bool) -> (a,Bool)
-Isaac
Isaac Dupree
> On Tue, May 27, 2008 at 3:40 PM, Kim-Ee Yeoh <a.biu...@asuhan.com> wrote:
>> Let's fill in the type variable: (x -> x) -> (Char, Bool) ==>
>> forall x. (x -> x) -> (Char, Bool) ==> x_t -> (x -> x) -> (Char, Bool),
>> where x_t is the hidden type-variable, not unlike the reader monad.
>>
>> As you've pointed out, callER chooses x_t, say Int when
>> passing in (+1) :: Int -> Int, which obviously would break
>> \f -> (f 'J', f True).
>>
>> What we want is the callEE to choose x_t since callEE needs to
>> instantiate x_t to Char and Bool. What we want is
>> (x_t -> x -> x) -> (Char, Bool).
>> But that's just
>> (forall x. x -> x) -> (Char, Bool).
>>
>
> Nice. That's the first time any of this really made sense to me. Is it
> possible to construct valid argument for that function?
agree, the types-are-arguments-too makes thinking about how it works A
LOT clearer... and it's actually what GHC's intermediate Core language
does. It's too bad there's no way in the language syntax to make that
interpretation clearer. (That's a subset of explicit dependent types --
explicitness is opposite type inference, not static vs. dependentness.)
-Isaac
Tillmann Rendel
> So, after an entire day of boggling my mind over this, I have brought it
> down to one simple example:
>
> (id 'J', id True) -- Works perfectly.
>
> \f -> (f 'J', f True) -- Fails miserably.
>
> Both expressions are obviously perfectly type-safe, and yet the type
> checker stubbornly rejects the second example. Clearly this is a flaw in
> the type checker.
>
> So what is the type of that second expression? You would think that
>
> (x -> x) -> (Char, Bool)
>
> as a valid type for it. But alas, this is not correct. The CALLER is
> allowed to choose ANY type for x - and most of possible choices wouldn't
> be type-safe. So that's no good at all!
All possible choices wouldn't be type-safe, so its even worse.
> In a nutshell, the function being passed MAY accept any type - but we
> want a function that MUST accept any type. This excusiatingly subtle
> distinction appears to be the source of all the trouble.
>
> Interestingly, if you throw in the undocumented "forall" keyword,
> everything magically works:
>
> (forall x. x -> x) -> (Char, Bool)
But you have to do it right.
forall x . (x -> x) -> (Char, Bool)
is equivalent to the version without forall, and does you no good. (Note
the parentheses to see why these two types are different). So there lies
no magic in mentioning forall, but art in putting it in the correct
position.
> The key problem seems to be that the GHC manual assumes that anybody
> reading it will know what "universal quantification" actually means.
> Unfortunately, neither I nor any other human being I'm aware of has the
> slightest clue what that means. A quick search on that infallable
> reference [sic] Wikipedia yields several articles full of dense logic
> theory. Trying to learn brand new concepts from an encyclopedia is more
> or less doomed from the start. As far as I can comprehend it, we have
>
> existential quantification = "this is true for SOMETHING"
> universal quantification = "this is true for EVERYTHING"
>
> Quite how that is relevant to the current discussion eludes me.
Your "MUST accept any type" is related to universal quantification, and
your "MAY accept any type" is related to existential quantification:
This works for EVERYTHING, so it MUST accept any type.
This works for SOMETHING, so it accepts some unknown type.
Quantification is the logic word for "abstracting by introducing a name
to filled with content later". For example, in your above paragraph you
wanted to tell us that no human being you are aware of has the slightest
clue what "universal quantification" means. You could have done so by
enumerating all human beings you are aware of. Instead, you used
universal quantification:
for all HUMAN BEING, HUMAN BEING has no clue.
(shortened to not overcomplicate things, HUMAN BEING is the name here).
Tillmann
Philippa Cowderoy
and a significant part of the innards of Hindley-Milner typing in order to
answer your questions. Expect to bang your head a little!
On Tue, 27 May 2008, Andrew Coppin wrote:
> - A function starts out with a polymorphic type, such as 'x -> x'.
>
Which is the same as "forall x. x -> x".
> - Each time the function is called, all the type variables have to be locked
> down to real types such as 'Int' or 'Either (Maybe (IO Int)) String' or
> something.
>
Yep, in fact in the explicitly-typed calculus commonly used as a model for
rank-n polymorphism (System F) there are explicit type lambdas and type
applications that do exactly this. Using /\ for a type lambda and [term
type] for type applications, id might be written thus:
id = /\t.(\x::t->x)
and called thus:
[id Int] 1
> - By the above, any function passed to a high-order function has to have all
> its type variables locked down, yielding a completely monomorphic function.
>
Yep.
> - The "forall" hack somehow convinces the type checker to not lock down some
> of the type variables. In this way, the type variables relating to a function
> can remain unlocked until we reach each of the call sites. This allows the
> variables to be locked to different types at each site [exactly as they would
> be if the function were top-level rather than an argument].
>
Not a hack. If there is a hack, it's in /not/ including a forall for
rank-1 types. Foralls correspond to type lambdas in the same way that ->s
correspond to ordinary lambdas.
> - Why are top-level variables and function arguments treated differently by
> the type system?
The big difference is between lambdas and binding groups (as in let,
top-level etc). With the binding group, any constraints on a value's type
will be found within its scope - so the type can be 'generalised' there,
putting a forall around it. The same isn't true of lambdas, and so their
parameters can only be polymorphic given an appropriate type annotation.
For extra confusion, type variables are themselves monomorphic[1].
> - Why do I have to manually tell the type checker something that should be
> self-evident?
It isn't - the general case is in fact undecidable.
> - Why do all type variables need to be locked down at each call site in the
> first place?
Find an alternative model for parametric polymorphism that works!
Note that 'not locking down' is equivalent to locking down to parameters
you took from elsewhere. As such, if you stick to rank-1 types you never
actually notice the difference - whereas it makes the type system an awful
lot easier to understand.
> - Why is this virtually never a problem in real Haskell programs?
I wouldn't go so far as to say virtually never, I've run into it a fair
few times - but normally until you're trying to do pretty generalised
stuff it's just not necessary.
> - Is there ever a situation where the unhacked type system behaviour is
> actually desirably?
There are plenty of situations where a rank-1 type is the correct type. If
you give id a rank-2 type, it's more specific - just as if you typed it
Int->Int.
> - Why can't the type system automatically detect where polymorphism is
> required?
Because there's often more than one possible type for a term, without a
'most general' type.
> - Does the existence of these anomolies indicate that Haskell's entire type
> system is fundamentally flawed and needs to be radically altered - or
> completely redesigned?
>
About as much as the undecidability of the halting problem and the
incompleteness theory suggest our understanding of computation and logic
is fundamentally flawed - which is to say, not at all.
> The key problem seems to be that the GHC manual assumes that anybody reading
> it will know what "universal quantification" actually means. Unfortunately,
> neither I nor any other human being I'm aware of has the slightest clue what
> that means.
Guess nobody on this list's human, huh?
It's really not the GHC manual's job to teach you the language extensions
from scratch any more than it should teach Haskell 98 from scratch. I
guess the real question is where the relevant community documentation is,
something I have to admit to not having needed to check.
> existential quantification = "this is true for SOMETHING"
> universal quantification = "this is true for EVERYTHING"
>
The type "forall x. x -> x" is "for all types x, x -> x". As in, "for all
types x, (\y -> y) :: x -> x".
[1] Actually this is no longer quite true since GHC now supports
impredicative polymorphism in which type variables can be instantiated
with polymorphic types. But please ignore that for now?
'In Ankh-Morpork even the shit have a street to itself...
Truly this is a land of opportunity.' - Detritus, Men at Arms
Ryan Ingram
> On Tue, May 27, 2008 at 3:40 PM, Kim-Ee Yeoh <a.biu...@asuhan.com> wrote:
> > What we want is the callEE to choose x_t since callEE needs to
> > instantiate x_t to Char and Bool. What we want is
> > (x_t -> x -> x) -> (Char, Bool).
> > But that's just
> > (forall x. x -> x) -> (Char, Bool).
> Nice. That's the first time any of this really made sense to me. Is it
> possible to construct valid argument for that function?
Yes, it's easy, especially since there is only one total function of
that type: id
-- ryan
Ryan Ingram
> This is probably the first real use I've ever seen of so-called rank-2
> types, and I'm curios to know why people think they need to exist.
> [Obviously when somebody vastly more intelligent than me says something is
> necessary, they probably know something I don't...]
The usual example I've seen for "beauty in rank-2 types" is the ST monad.
ST lets you define 'stateful' imperative algorithms with destructive
update, but be able to call them safely from pure-functional code.
This is made safe by a "phantom" type variable and the rank-2 type of runST:
> runST :: forall a. (forall s. ST s a) -> a
The "s" in ST logically represents the "initial state" used by the
imperative computation it represents; it tracks any allocations and
updates that need to be made before the computation can run. By
requiring that the passed in computation works for *any* initial
state, you guarantee that it can't reference any external store or
return data from within the store; for example, consider this:
> newSTRef :: forall s a. a -> ST s (STRef s a)
> mkZero :: forall s. ST s (STRef s Int)
> mkZero = newSTRef 0
Now consider trying to type "runST mkZero"; first we generate a new
type variable "s1" for the "s" in mkZero, then use it to instantiate
the result type, "a":
runST :: (forall s. ST s (STRef s1 a)) -> STRef s1 a
Now we need to unify s1 with s to match mkZero's type for the first
argument. But we can't do that, because then "s" escapes its forall
scope. So we can statically guarantee that no references escape from
runST!
---
Another example that I personally am attached to is Prompt:
http://hackage.haskell.org/cgi-bin/hackage-scripts/package/MonadPrompt
(There's no Haddock documentation on that site, but the source code is
well-commented and there's a module of examples).
The function I want to talk about is "runPrompt"
> prompt :: forall p a. p a -> Prompt p a
> runPrompt :: forall p r. (forall a. p a -> a) -> Prompt p r -> r
Lets instantiate p and r to simplify things; I'll use [] for p and Int for r.
> test1 :: Prompt [] Int
> test1 = prompt [1,2,3]
> test2 :: Prompt [] Int
> test2 = do
> x <- prompt ['A', 'B', 'C']
> return (ord x) -- ord :: Char -> Int
Now, the type of runPrompt specialized for these examples is
> runPrompt :: (forall a. [a] -> a) -> Prompt [] Int -> Int
Notice that we need to pass in a function that can take -any- list and
return an element. One simple example is "head":
> head :: forall a. [a] -> a
> head (x:xs) = x
So, putting it together:
ghci> runPrompt head test1
1
ghci> runPrompt head test2
65 -- ascii code for 'A'.
Now, this isn't that great on its own; wouldn't it be useful to be
able to get some information about the type of result needed when
writing your prompt-handler function? Then you could do something
different in each case.
That's a question for another topic, but to get you started, start
looking around for information on GADTs.
-- ryan
Luke Palmer
<andrew...@btinternet.com> wrote:
> Gleb Alexeyev wrote:
>>
>> foo :: (forall a . a -> a) -> (Bool, String)
>> foo g = (g True, g "bzzt")
>
> So, after an entire day of boggling my mind over this, I have brought it
> down to one simple example:
>
> (id 'J', id True) -- Works perfectly.
>
> \f -> (f 'J', f True) -- Fails miserably.
>
> Both expressions are obviously perfectly type-safe, and yet the type checker
> stubbornly rejects the second example. Clearly this is a flaw in the type
> checker.
>
> So what is the type of that second expression? You would think that
>
> (x -> x) -> (Char, Bool)
When you're reasoning about this, I think it would help you greatly to
explicitly put in *all* the foralls. In haskell, when you write, say:
map :: (a -> b) -> [a] -> [b]
All the free variables are *implicitly* quantified at the top level.
That is, when you write the above, the compiler sees:
map :: forall a b. (a -> b) -> [a] -> [b]
(forall has low precedence, so this is the same as:
map :: forall a b. ((a -> b) -> [a] -> [b])
)
And the type you mention above for the strange expression is:
forall x. (x -> x) -> (Char, Bool)
Which indicates that the caller gets to choose. That is, if a caller
sees a 'forall' at the top level, it is allowed to instantiate it with
whatever type it likes. Whereas the type you want has the forall in
a different place than the implicit quantifiaction:
(forall x. x -> x) -> (Char, Bool)
Here the caller does not have a forall at the top level, it is hidden
inside a function type so the caller cannot instantiate the type.
However, when implementing this function, the argument will now have
type
forall x. x -> x
And the implementation can instantiate x to be whatever type it likes.
But my strongest advice is, when you're thinking through this, remember that:
x -> x
Is not by itself a type, because x is meaningless. Instead it is
Haskell shorthand for
forall x. x -> x
Luke
Ketil Malde
> So, after an entire day of boggling my mind over this, I have brought
> it down to one simple example:
>
> (id 'J', id True) -- Works perfectly.
>
> \f -> (f 'J', f True) -- Fails miserably.
>
> Both expressions are obviously perfectly type-safe, and yet the type
> checker stubbornly rejects the second example. Clearly this is a flaw
> in the type checker.
>
> So what is the type of that second expression? You would think that
>
> (x -> x) -> (Char, Bool)
A bit late in the fray, but have you considered this simpler
expression:
\f -> f 'J'
I think you'll agree this does not have type
(x->x) -> Char
but rather
(Char -> a) -> a
right? Yet you can use 'id' as an argument (for f), since it has type
forall a . a -> a
where you are free to substitute Char for a and get (Char -> Char).
An expression like:
\f -> (f 'J', f True)
requires an f that is both (Char -> a) and (Bool -> a) *at the same
time*. A type like (a -> a) -> (Char,Bool) means that the expression
is polymorphic in its argument, but here you need to specify that the
function argument must be polymorphic itself.
E.g. (forall a. a -> a) -> (Char,Bool).
(Disclaimer: I hope I got it right :-)
-k
--
If I haven't seen further, it is by standing in the footprints of giants
Roberto Zunino
> (id 'J', id True) -- Works perfectly.
>
> \f -> (f 'J', f True) -- Fails miserably.
>
> Both expressions are obviously perfectly type-safe, and yet the type
> checker stubbornly rejects the second example. Clearly this is a flaw in
> the type checker.
When you type some expression such as
\x -> x
you have to choose among an infinite number of valid types for it:
Int -> Int
Char -> Char
forall a . a -> a
forall a b . (a,b) -> (a,b)
...
Yet the type inference is smart enough to choose the "best" one:
forall a. a -> a
because this is the "most general" type.
Alas, for code like yours:
foo = \f -> (f 'J', f True)
there are infinite valid types too:
(forall a. a -> Int) -> (Int, Int)
(forall a. a -> Char)-> (Char, Char)
(forall a. a -> (a,a)) -> ((Char,Char),(Bool,Bool))
...
and it is much less clear if a "best", most general type exists at all.
You might have a preference to type it so that
foo :: (forall a . a->a) -> (Char,Bool)
foo id ==> ('J',True) :: (Char,Bool)
but one could also require the following, similarly reasonable code to work:
foo :: (forall a. a -> (a,a)) -> ((Char,Char),(Bool,Bool))
foo (\y -> (y,y)) ==> (('J','J'),(True,True))
:: ((Char,Char),(Bool,Bool))
And devising a type inference system allowing both seems to be quite
hard. Requiring a type annotation for these not-so-common code snippets
seems to be a fair compromise, at least to me.
Regards,
Zun.
Andrew Coppin
> When you're reasoning about this, I think it would help you greatly to
> explicitly put in *all* the foralls. In haskell, when you write, say:
>
> map :: (a -> b) -> [a] -> [b]
>
> All the free variables are *implicitly* quantified at the top level.
> That is, when you write the above, the compiler sees:
>
> map :: forall a b. (a -> b) -> [a] -> [b]
>
>
> forall x. (x -> x) -> (Char, Bool)
>
> Which indicates that the caller gets to choose. That is, if a caller
> sees a 'forall' at the top level, it is allowed to instantiate it with
> whatever type it likes. Whereas the type you want has the forall in
> a different place than the implicit quantifiaction:
>
> (forall x. x -> x) -> (Char, Bool)
>
> Here the caller does not have a forall at the top level, it is hidden
> inside a function type so the caller cannot instantiate the type.
> However, when implementing this function, the argument will now have
> type
>
> forall x. x -> x
>
> And the implementation can instantiate x to be whatever type it likes.
>
Hmm. Right. So you're saying that the exact position of the "forall"
indicates the exact time when the variable(s) get specific types
assigned to them?
So... the deeper you nest the foralls, the longer those variables stay
unbound? [And the higher the "rank" of the type?]
Finally, that seems to make actual sense. I have one final question though:
forall x, y. x -> y -> Z
forall x. x -> (forall y. y -> Z)
Are these two types the same or different? [Ignoring for a moment the
obvious fact that you'll have one hell of a job writing a total function
with such a type!] After all, ignoring the quantification, we have
x -> y -> Z
x -> (y -> Z)
which are both the same type. So does that mean you can move the forall
to the left but not to the right? Or are the types actually different?
Andrew Coppin
> When you type some expression such as
>
> \x -> x
>
> you have to choose among an infinite number of valid types for it:
>
> Int -> Int
> Char -> Char
> forall a . a -> a
> forall a b . (a,b) -> (a,b)
> ...
>
> Yet the type inference is smart enough to choose the "best" one:
> forall a. a -> a
> because this is the "most general" type.
>
> Alas, for code like yours:
>
> foo = \f -> (f 'J', f True)
>
> there are infinite valid types too:
>
> (forall a. a -> Int) -> (Int, Int)
> (forall a. a -> Char)-> (Char, Char)
> (forall a. a -> (a,a)) -> ((Char,Char),(Bool,Bool))
> ...
>
> and it is much less clear if a "best", most general type exists at all.
> Requiring a type annotation for these not-so-common code snippets
> seems to be a fair compromise, at least to me.
Thank you for coming up with a clear and comprehensible answer.
Isaac Dupree
> Finally, that seems to make actual sense. I have one final question though:
>
> forall x, y. x -> y -> Z
> forall x. x -> (forall y. y -> Z)
>
> Are these two types the same or different? [Ignoring for a moment the
> obvious fact that you'll have one hell of a job writing a total function
> with such a type!]
they're the same type: foralls in function *results* can be moved to the
outside with no change in meaning. They don't make it a higher rank
type. (though some definitions in typically-uncurried languages like to
call it higher rank, that's not relevant to us). (modulo GHC issues
with impredicative polymorphism, which ideally shouldn't even come into
the picture here, because you're only using/exploring RankNTypes)
-Isaac
Lennart Augustsson
(which Haskell isn't).
Phillippa mentioned it in an earlier post, but here it is again.
First the old stuff, if you have a term of type (S->T) then the
(normal form of) term must be (\ x -> e), where x has type S and e has
type T.
When using a function it's the caller that decided the actual value of
the x, and the callee decides the value to return.
OK, now forall. If a term is of type (forall a . T) then the (normal
form of) term must be (/\ a -> e), where /\ is a capital lambda, and
it means it's a function that takes a type as the argument instead of
a term. For type application I'll write f@T, meaning that f is /\
function and we give it type argument T.
Let's try it on some functions. What's the real type id? It's
id :: forall a . a-> a
since the type is a forall, the body of the function must start with a /\
id = /\ b -> \ x -> x
(or if you want to be explicit about types id= /\ b -> \ (x::b) -> x)
It's quite clear that the caller gets to pick both the type argument
and the value argument, and the id function only gets to pick the
return value,
e.g., (id@Int 5) or (id@Bool True).
Another example
const :: forall a . forall b . a -> b -> a
const = /\ a -> /\ b -> \ x -> \ y -> x
or, alternatively
const' :: forall a . a -> forall b . b -> a
const' = /\ a -> \ x -> /\ b -> \ y -> x
It's obvious that the caller gets to pick both types and both values.
The placement of the foralls only affect the type application order
(const@Int@Bool 5 True) resp (const'@Int 5 @Bool True).
All right, so let's do rank 2.
f :: (forall a . a -> a) -> (Int, Bool)
What's the body of the function? The top level type is -> so it must
start with a \, e.g., \ g ->
When using g it must be used correctly. The type of g starts with a
forall, so using it must start with a type application followed by a
normal application.
f = \ g -> (g@Int 5, g@Bool True)
So it's again clear the the caller of f doesn't get to pick the type
a, it must be supplied by the callee. The caller of f must supply a
value of type (forall a . a->a), i.e., (f id).
So you can see that depending on the forall's position with respect to
the -> the role of it changes from a type being picked by the caller
or callee.
(If it's under an odd number of arrows the callee picks.)
If you remove all the explicit type abstractions and applications
above then you have Haskell (+ RankN).
As other have pointed out, you can't remove the nested foralls because
in general they cannot be inferred.
Hope this helps.
-- Lennart
Ryan Ingram
> Andrew Coppin wrote:
> > Finally, that seems to make actual sense. I have one final question
> though:
> >
> > forall x, y. x -> y -> Z
> > forall x. x -> (forall y. y -> Z)
> >
> > Are these two types the same or different? [Ignoring for a moment the
> obvious fact that you'll have one hell of a job writing a total function
> with such a type!]
> >
>
> they're the same type: foralls in function *results* can be moved to the
> outside with no change in meaning. They don't make it a higher rank type.
> (though some definitions in typically-uncurried languages like to call it
> higher rank, that's not relevant to us). (modulo GHC issues with
> impredicative polymorphism, which ideally shouldn't even come into the
> picture here, because you're only using/exploring RankNTypes)
To be clear, these types are different but it doesn't matter because
we are also given a "type-abstraction" rule which allows us to convert
between the two trivially.
For example, given:
> const :: forall a b. a -> b -> a
> const2 :: forall a. a -> (forall b. b -> a)
When you partially apply const, you need to specify a type for the
second argument (see the previous person talking about "locking down"
type variables at the call site).
However, you don't know what type to lock down "b" to, so you can let
your caller choose! Here's an example...
> test = const (1 :: Int)
What is the type of test? First we need to "lock down" the types for
const; part of that involves generating a type variable for the "a"
and "b" arguments for const; while the "a" argument unifies with Int,
it turns out the "b" type variable is never used, so we allow the user
to choose it, ending up with the result:
> test :: forall b. b -> Int
The reason why you can always move a "forall" to the left of a
function arrow is very simple; given a type A (that may have some type
variables, but no "b"s.), and a type B (that may have some type
variables, including "b"), consider these two types:
type t1 = forall b. (A -> B)
type t2 = A -> (forall b. B)
To convert from t1 to t2, since A has no mention of the type variable
"b", we just delay the decision of what "b" should be. In system F
notation, given an expression e1 of type t1, we can convert it to t2
in the following way:
] e2 :: t2
] e2 = \(a :: A) -> /\ b -> e1 @b a
Similarily, given an expression e2 of type t2, we can convert to t1:
] e1 :: t1
] e1 = /\ b -> \(a :: A) -> e2 a b
However, if we have a higher ranked type:
type t3 = (forall b. B) -> A
type t4 = forall b. (B -> A)
this conversion no longer works! This is because expressions of type
t3 may call their arguments at many instances of b. We can, however,
convert an expression e4 of type t4 into the higher-ranked type t3:
] e3 :: t3
] e3 = \(x :: forall b. B) -> e4 @Int (x @Int)
Notice that we had to choose some arbitrary type (I picked Int) to
instantiate x at when calling e4; this shows that the rank-2 type is
definitely different than the rank-1 type; it leaves more choices up
to the callee!
-- ryan
Kim-Ee Yeoh
Roberto Zunino-2 wrote:
>
> Alas, for code like yours:
> foo = \f -> (f 'J', f True)
>
> there are infinite valid types too:
> (forall a. a -> Int) -> (Int, Int)
> (forall a. a -> Char)-> (Char, Char)
> (forall a. a -> (a,a)) -> ((Char,Char),(Bool,Bool))
> ...
>
> and it is much less clear if a "best", most general type exists at all.
>
How about
foo :: (exists. m :: * -> *. forall a. a -> m a) -> (m Char, m Bool)
Not quite Haskell, but seems to cover all of the examples you gave.
-- Kim-Ee
--
View this message in context: http://www.nabble.com/Aren%27t-type-system-extensions-fun--tp17479349p17531238.html
Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com.
_______________________________________________
Luke Palmer
> Roberto Zunino-2 wrote:
>>
>> Alas, for code like yours:
>> foo = \f -> (f 'J', f True)
>>
>> there are infinite valid types too:
>> (forall a. a -> Int) -> (Int, Int)
>> (forall a. a -> Char)-> (Char, Char)
>> (forall a. a -> (a,a)) -> ((Char,Char),(Bool,Bool))
>> ...
>>
>> and it is much less clear if a "best", most general type exists at all.
>>
>
> How about
> foo :: (exists. m :: * -> *. forall a. a -> m a) -> (m Char, m Bool)
>
> Not quite Haskell, but seems to cover all of the examples you gave.
You have now introduced a first-class type function a la dependent
types, which I believe makes the type system turing complete. This
does not help the decidability of inference :-)
Luke
Roberto Zunino
>
> How about
> foo :: (exists. m :: * -> *. forall a. a -> m a) -> (m Char, m Bool)
Thank you: I had actually thought about something like that.
First, the exists above should actually span over the whole type, so it
becomes a forall because (->) is contravariant on its 1st argument:
foo :: forall m :: * -> * . (forall a. a -> m a) -> (m Char, m Bool)
This seems to be Haskell+extensions, but note that m above is meant to
be an arbitrary type-level function, and not a type constructor (in
general). So, I am not surprised if undecidability issues arise in type
checking/inference. :-)
Another valid type for foo can be done AFAICS with intersection types:
foo :: (Char -> a /\ Bool -> b) -> (a,b)
But I can not comment about their inference, or usefulness in practice.
Regards,
Zun.
Edsko de Vries
> Kim-Ee Yeoh wrote:
> >
> >How about
> > foo :: (exists. m :: * -> *. forall a. a -> m a) -> (m Char, m Bool)
>
> Thank you: I had actually thought about something like that.
>
> First, the exists above should actually span over the whole type, so it
> becomes a forall because (->) is contravariant on its 1st argument:
>
> foo :: forall m :: * -> * . (forall a. a -> m a) -> (m Char, m Bool)
>
> This seems to be Haskell+extensions, but note that m above is meant to
> be an arbitrary type-level function, and not a type constructor (in
> general). So, I am not surprised if undecidability issues arise in type
> checking/inference. :-)
Type *checking* is still decidable (System Fw is sufficiently powerful
to model these types) but type inference now needs higher order
unification, which indeed is undecidable.
> Another valid type for foo can be done AFAICS with intersection types:
>
> foo :: (Char -> a /\ Bool -> b) -> (a,b)
>
> But I can not comment about their inference, or usefulness in practice.
Again, undecidable :) In fact, I believe that an inference algorithm for
intersection types is equivalent to solving the halting problem. Type
checking however is decidable, but expensive.
Edsko
Kim-Ee Yeoh
Luke Palmer-2 wrote:
>
> You have now introduced a first-class type function a la dependent
> types, which I believe makes the type system turing complete. This
> does not help the decidability of inference :-)
>
God does not care about our computational difficulties. He infers
types emp^H^H^H ... uh, as He pleases.
Anyway, the original point of it was semantic. Let's first
explore the meaning of "the most general type." Type functions
give one answer, intersection types another.
-- Kim-Ee (yeoh at cs dot wisc dot edu)
--
View this message in context: http://www.nabble.com/Aren%27t-type-system-extensions-fun--tp17479349p17534701.html
Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com.
_______________________________________________
Achim Schneider
>
>
> Luke Palmer-2 wrote:
> >
> > You have now introduced a first-class type function a la dependent
> > types, which I believe makes the type system turing complete. This
> > does not help the decidability of inference :-)
> >
>
> God does not care about our computational difficulties. He infers
> types emp^H^H^H ... uh, as He pleases.
>
This begs the question: Can God come up with a type He doesn't
understand?
The answer, it seems, is Mu.
--
(c) this sig last receiving data processing entity. Inspect headers for
past copyright information. All rights reserved. Unauthorised copying,
hiring, renting, public performance and/or broadcasting of this
signature prohibited.
Isaac Dupree
>>
>> foo :: (Char -> a /\ Bool -> b) -> (a,b)
>>
>> But I can not comment about their inference, or usefulness in practice.
>
> Again, undecidable :) In fact, I believe that an inference algorithm for
> intersection types is equivalent to solving the halting problem. Type
> checking however is decidable, but expensive.
a.k.a. find some value that matches both Char->a and Bool->b for some a
and b. Could use type-classes to do it.
But why, when we can just use standard tuples instead?
foo :: (Char -> a , Bool -> b) -> (a,b)
Admittedly this function is isomorphic to type (Char,Bool)... but that's
a different issue, with the arbitrariness of our choice of example function.
-Isaac
Roberto Zunino
>>> foo :: (Char -> a /\ Bool -> b) -> (a,b)
>
> and b. Could use type-classes to do it.
Uhmm... you mean something like (neglecting TC-related issues here)
class C a b where
fromChar :: Char -> a
fromBool :: Bool -> b
or some more clever thing?
If this can be encoded with method-less classes, I would be quite
interested in knowing how.
> But why, when we can just use standard tuples instead?
> foo :: (Char -> a , Bool -> b) -> (a,b)
This makes the class dictionary explicit.
Alas, IIUC we lost type erasure (does that still hold with intersection
types?) in this "implementation".
Zun.
Roberto Zunino
> Uhmm... you mean something like (neglecting TC-related issues here)
>
> class C a b where
> fromChar :: Char -> a
> fromBool :: Bool -> b
Oops: i meant something like
class C x a b | x -> a,b where
fromChar :: x -> Char -> a
fromBool :: x -> Bool -> b
Isaac Dupree
>>>
>>> a.k.a. find some value that matches both Char->a and Bool->b for some a and b. Could use type-classes to do it.
>> Uhmm... you mean something like (neglecting TC-related issues here)
>>
>> class C a b where
>> fromChar :: Char -> a
>> fromBool :: Bool -> b
>
> Oops: i meant something like
>
> class C x a b | x -> a,b where
> fromChar :: x -> Char -> a
> fromBool :: x -> Bool -> b
no... let me figure out what I meant. Just somehow to have a single
function that takes an argument of two different types without
completely ignoring it.
class Arg a where
whatYouPass :: a -> Something
instance Arg Char where
whatYouPass = ...
instance Arg Bool where
whatYouPass = ...
Then (foo whatYouPass) :: (Something, Something).
Or if it was
class Arg a where
whatYouPass :: a -> a
then (foo whatYouPass) :: (Char, Bool).
And I'm sure there are ways to make the return type different if you
want to think about FDs etc.
Simon Peyton-Jones
| I have complete confidence that whoever wrote the GHC manual knew
| exactly what they meant. I am also fairly confident that this was the
| same person who implemented and even designed this particular feature.
| And that they probably have an advanced degree in type system theory. I,
| however, do not. So if in future the GHC manual could explain this in
| less opaque language, that would be most appreciated. :-}
As the person who wrote the offending section of the GHC user manual (albeit lacking a qualification of any sort in type theory), I am painfully aware of its shortcomings. Much of the manual is imprecise, and explains things only by examples. The wonder is that it apparently serves the purpose for many people.
Nevertheless, the fact is that it didn't do the job for Andrew, at least not first time around.
After some useful replies to his email, he wrote
| Thank you for coming up with a clear and comprehensible answer.
I would very much welcome anyone who felt able to improve on the text in the manual, even if it's only a paragraph or two. If you stub your toe on the manual, once you find the solution, take a few minutes to write the words you wish you had read to begin with, and send them to me.
Meanwhile, Andrew, I recommend the paper "Practical type inference for arbitrary rank types", which is, compared to the user manual at least, rather carefully written.
Simon