Sunday, September 16, 2012

Category of Stacks

In the usual category of types as objects with morphisms the terms of some language, the types are the usual base types and all types constructable from a set of type constructors. It seems that we would need a different kind of category for a concatenative language- one where the types are stacks with basics types, perhaps polymorphic types, and always ending in "Stack variables" indicating a "rest of the stack". This seems to be the usual way to consider type systems for these language, but I've never seem an investigation of the category this would form. Unfortunately, since I understand only the basics of even elementary category theory, all I can do is make some basic observations.

First off- The stack consisting of only a stack variable is terminal. It is terminal because you can always pop off anything from the defined part of a stack until you get to its stack variable. At first I thought it was initial too, because you can always add to the empty stack to get to a given type, but what would you add? At the least there is no unique term, and with polymorphic stack elements there is nothing reasonable to add at all. I don't believe that there is an initial object, unless there is some sense in which we can bind the "rest of the stack" to a given type, instantiating at any type we want. I'm not sure if this really makes sense, however.

Secondly- a stack with the elements of two stacks, the first stacks elements followed by the seconds elements, seems to form a product. We can always drop the elements of one of the two stacks to get the other one, which form the projections. Just as with regular type products there is an arbitrary order and an isomorphism swapping that order. Note that the terminal stack does seem to be the identity of the product, so that encouraging.

Thirdly- sums are a bit tricky. The only reasonable way I can think to form a sum is to take two stacks and push them as a single element of a sum type of stacks. This makes it a stack of stacks. Otherwise you would need to somehow "tag" parts of a stack that may be different lengths, and I don't seem how this would work. Its not a big deal to make this a stack of stacks, and I believe that has been done before, but it is interesting that if we don't do it that way then there are no sum types that I can think of. If we do allow this, it also seems like a similar product of stacks exists, But then we need a separate unit type as its identity as the empty stack would become the identity of the sum and the zero of the product.

A similar situation appears to occur with pushout and pullbacks, and limits and colimits. I can't make any of this rigorous, but it does seems to behave differently then regular categories of types, and is perhaps worth some study.

No comments:

Post a Comment