Apologies for the double-reply...
Your mail prompted me to finally get around to adding a mono/polytype system
to an interpreter I've been working on for pure type systems, to see what a
GHC-alike type system would look like. Here's what I came up with.
Constants are: *m, []m, *p and []p
On Sun, Dec 6, 2009 at 8:39 AM, Dan Doel dan.d...@gmail.com wrote:
Apologies for the double-reply...
Your mail prompted me to finally get around to adding a mono/polytype system
to an interpreter I've been working on for pure type systems, to see what a
GHC-alike type system would look like.
Hello.
Consider the type: (forall a . a) - String.
On one hand, it is rank-2 polymorphic, because it abstracts over a
rank-1 polymorphic type.
On the other hand, it is monomorphic because it isn't actually
quantified itself: in my intuitive view, a parametrically polymorphic
type has infinitely
Eugene Kirpichov wrote:
Hello.
Consider the type: (forall a . a) - String.
On one hand, it is rank-2 polymorphic, because it abstracts over a
rank-1 polymorphic type.
On the other hand, it is monomorphic because it isn't actually
quantified itself: in my intuitive view, a parametrically
Eugene,
Consider the type: (forall a . a) - String.
It's of rank 2.
What is the definition of rank of a polymorphic type?
The minimal rank of a type is given by
rank (forall a. t) = 1 `max` rank t
rank (t - u) = (if rank t == 0 then 0 else rank t + 1) `max`
rank u
rank _
2009/12/5 Stefan Holdermans ste...@cs.uu.nl:
Eugene,
Consider the type: (forall a . a) - String.
It's of rank 2.
What is the definition of rank of a polymorphic type?
The minimal rank of a type is given by
rank (forall a. t) = 1 `max` rank t
rank (t - u) = (if rank t == 0 then 0
Eugene,
1) Does there exist an authoritative source saying the same? Not that
I'm doubting, just supposing that the source would have other
interesting information, too :)
You may want to have a look at the already mentioned JFP-article by
Peyton Jones et al. and perhaps the work of Kfoury
2009/12/6 Stefan Holdermans ste...@cs.uu.nl:
Eugene,
1) Does there exist an authoritative source saying the same? Not that
I'm doubting, just supposing that the source would have other
interesting information, too :)
You may want to have a look at the already mentioned JFP-article by Peyton
On Sunday 06 December 2009 1:42:34 am Eugene Kirpichov wrote:
OK, thanks.
However, isn't the type (forall a . a) - String impredicative because
it instantiates a type variable of the type constructor (-) p q with
p = forall a . a?
There's probably no clear cut answer to this independent of
