23 views

Skip to first unread message

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.

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

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

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.

>

>

> 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

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

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.

> 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

Apr 23, 2008, 10:45:33 PM4/23/08

to catla...@googlegroups.com

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

- John

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

Search

Clear search

Close search

Google apps

Main menu