Cat type system error (failure with some cases of nested polymorphism)

23 views
Skip to first unread message

Christopher Diggins

unread,
Apr 23, 2008, 12:16:00 PM4/23/08
to catla...@googlegroups.com
Thanks to John Nowak, for identifying this problem: the Cat type
system does not yet handle nested polymorphism correctly.

In Cat the type system is supposed to be compositional. For example:

define fg { f g }
define gh { g h }

The type of "f gh" should be the same as "fg h". Unfortunately this is
not always the case.

A good example is:

define dd { dup dip }
define f { [id] dup dip }
define g { [id] dd }

The type of f is

f : (A b -> A b (C d -> C d))

However the type of g is

g : (A b -> A b (A b -> A b))

What has happened is that the unification process failed to properly
deal with polymorphic type variables.

Consider the following types (which are correct)

[id] : (A -> A (B c -> B c))
dd : (D (D -> E) -> E (D -> E))

To be perfectly clear I need to add explicit universal quantification operators:

[id] : forall.A.(A -> A forall.B.c.(B c -> B c))
dd : forall.D.E.(D (D -> E) -> E (D -> E))

When I compose these, I get the result:

(A -> E (D -> E))

And I also generate the equality:

A forall.B.c.(B c -> B c) = D (D -> E)

Which in turn generates the equalities:

D = B c
E = B c
A = B c

So the end product is:

(B c -> B c (B c -> B c))

Well this is where the problem occurs: A = B c, but we have already
identified that B c is polymorphic (generic) relative to the function
on the stack.
We are implicitly constraining a polymorphic type variables, where we
don't want to.
At first it is tempting to rename all polymorphic type variables, but
we would get garbage:

(F g -> H i (J k -> L m))

This eliminates the important constraint that J k = L m, and F g = H i.

So the problem seems to be that we need to make polymorphic type
variables retain the forall quanitification at the correct level.

This might be achievable by using a kind of renaming system based on
which function the variable occurs in. For example we can look at dd
as having the following type:

(D0 (D1 -> E1) -> E0 (D2 -> E2))

So D0, E0 are one level and D1,E1 are another and D2->E2 are another.

At this point, I am not sure how to best handle the situiation. It
appears that as humans we have an ability to deduce where to place the
forall quantifiers, and I just need to express this.

It may be helpful to look at a function signature like this:

(D (D -> E) -> E (D -> E))

and consider it to be something like:

(D0 (D1 -> E1) -> E0 (D2 -> E2))

with the followign constraints:

(D0 = D1, E0 = E1, D2 = D0, E2 = E0)

So a more complete and correct polymorphic type system for Cat will
probably require consideration of the binding order of arguments to
values, and a more sophisticated renaming algorithm.

Well that's it for now, hopefully someone will find these thoughts useful.

- Christopher

John Nowak

unread,
Apr 23, 2008, 1:12:24 PM4/23/08
to catla...@googlegroups.com

On Apr 23, 2008, at 12:16 PM, Christopher Diggins wrote:

> At this point, I am not sure how to best handle the situiation. It
> appears that as humans we have an ability to deduce where to place the
> forall quantifiers, and I just need to express this.

The problem is that, in many cases, there's no best place to put the
quantifiers. As such, the programmer needs to step in and say what's
important for a particular use case.

It's worth considering that concatenative languages without explicit
recursive definitions (either because they're disallowed or because
they're desugared to use 'm') can be fully expanded down to
primitives. Doing so would allow quite a few more things to type
check, although you'd no longer be able to talk about the type of a
single function. Still, certain errors could be deduced to never be
avoidable even after definitions are expanded, so perhaps you could
still give local type errors even if you couldn't (always) display the
type.

If you're interested in retaining local type inference with higher
rank types, you might want to look into intersection types. This paper
shows that intersection types enable higher rank polymorphism to be
inferred for any rank, although each rank is exponentially more
difficult to infer:

http://citeseer.ist.psu.edu/466200.html

- John

Christopher Diggins

unread,
Apr 23, 2008, 1:26:13 PM4/23/08
to catla...@googlegroups.com
On Wed, Apr 23, 2008 at 1:12 PM, John Nowak <jo...@johnnowak.com> wrote:
>
>
> On Apr 23, 2008, at 12:16 PM, Christopher Diggins wrote:
>
> > At this point, I am not sure how to best handle the situiation. It
> > appears that as humans we have an ability to deduce where to place the
> > forall quantifiers, and I just need to express this.
>
> The problem is that, in many cases, there's no best place to put the
> quantifiers. As such, the programmer needs to step in and say what's
> important for a particular use case.

I am still not convinced that this is neccessariy the case in a
concatenative language. Given the infinite number of type systems
possible, I see no reason to believe that no consistent system for
deducing the best place to put a quanitifer exists, simply based on
the fact that modern researchers haven't yet found one.

> It's worth considering that concatenative languages without explicit
> recursive definitions (either because they're disallowed or because
> they're desugared to use 'm') can be fully expanded down to
> primitives.

That is a very good point!

> Doing so would allow quite a few more things to type
> check, although you'd no longer be able to talk about the type of a
> single function.

Which I suppose is completely fine.

> Still, certain errors could be deduced to never be
> avoidable even after definitions are expanded, so perhaps you could
> still give local type errors even if you couldn't (always) display the
> type.

Cool.

> If you're interested in retaining local type inference with higher
> rank types, you might want to look into intersection types. This paper
> shows that intersection types enable higher rank polymorphism to be
> inferred for any rank, although each rank is exponentially more
> difficult to infer:

Hmmm.... I like your solution a lot.

Thanks a lot for your thoughts and contributions!

- Christopher

John Nowak

unread,
Apr 23, 2008, 1:41:13 PM4/23/08
to catla...@googlegroups.com

On Apr 23, 2008, at 1:26 PM, Christopher Diggins wrote:


>> The problem is that, in many cases, there's no best place to put the
>> quantifiers. As such, the programmer needs to step in and say what's
>> important for a particular use case.
>
> I am still not convinced that this is neccessariy the case in a
> concatenative language. Given the infinite number of type systems
> possible, I see no reason to believe that no consistent system for
> deducing the best place to put a quanitifer exists, simply based on
> the fact that modern researchers haven't yet found one.

Well it's a bit more than that not having found one yet; higher rank
type inference has been proven undecidable for ranks higher than two
in systems with universal quantification. I don't see any reason to
that believe concatenative languages could get around this.

- John

Christopher Diggins

unread,
Apr 23, 2008, 3:10:30 PM4/23/08
to catla...@googlegroups.com
On Wed, Apr 23, 2008 at 1:41 PM, John Nowak <jo...@johnnowak.com> wrote:
> On Apr 23, 2008, at 1:26 PM, Christopher Diggins wrote:
> >> The problem is that, in many cases, there's no best place to put the
> >> quantifiers. As such, the programmer needs to step in and say what's
> >> important for a particular use case.
> >
> > I am still not convinced that this is neccessariy the case in a
> > concatenative language. Given the infinite number of type systems
> > possible, I see no reason to believe that no consistent system for
> > deducing the best place to put a quanitifer exists, simply based on
> > the fact that modern researchers haven't yet found one.
>
> Well it's a bit more than that not having found one yet; higher rank
> type inference has been proven undecidable for ranks higher than two
> in systems with universal quantification.

I assume you are referring to higher-rank type inference for System F
(http://citeseer.ist.psu.edu/wells98typability.html)? This is only one
particular group of calculi.
It is naive to assume that there are no constraints that we can place
on a type system to allow decidable inference of higher-order
universal quantification.

- Christopher

John Nowak

unread,
Apr 23, 2008, 10:45:33 PM4/23/08
to catla...@googlegroups.com

Indeed, this seems sensible. I was assuming too much.

- John

John Nowak

unread,
Apr 23, 2008, 10:54:24 PM4/23/08
to catla...@googlegroups.com

On Apr 23, 2008, at 1:12 PM, John Nowak wrote:

> http://citeseer.ist.psu.edu/466200.html

Ack. That is not the paper I meant to send. This is:

http://www.church-project.org/reports/Kfo+Wel:TCSB-2004-
v311n1-3.html

- John

Reply all
Reply to author
Forward
0 new messages