Induction, Co-induction, and Types in Slate

[Brian T. Rice]

Dear Tunesers,
What follows are some ideas I had concerning the specification of literal
types (integers, rationals, text, logic) within Slate, helpful towards
reflection. These ideas aren't incredibly well polished, but then that's
why I'm looking for input in the first place. :)

I've figured the simplest way to describe datatypes in slate would be to
use the object-as-set (as well as namespace) metaphor to have containers
for the datatypes, and have them interact within those namespaces. As an
example, I'd like to model the integers operationally using induction and
addition, with subtraction by inversion. A rough sketch of what I mean
starts with an object in Slate called Integers which acted as a container
namespace for the integer object type. Within this namespace, one would
have an object Zero which would have slots for addition, subtraction, etc.
When these slots are invoked, new objects get created that behaviorally
satisfy everything one would expect from a full formal description of the
integer. This description is too vague for real purposes, of course. I'll
describe how this should work below.

I originally came up with this idea to deal with the oddities of
co-inductive types, such as streams of values or even the rational number
system. Both of these ideas don't admit to a numeration via the natural
number system, and in programming languages are naturally
lazily-implemented. However, a robust general method (using equational
expressions) exists for specifying these types beyond simple algorithms.
However, I'm still working out the mechanics of this type of framework in
Slate, and I invite your comments.

The basic idea of using container objects as sets(classes) of all instances
of a datatype, I found that it also works fine for inductive datatypes. In
fact, it seems that the system won't be able to superficially tell them
apart, which is a Good Thing, in that we won't have some conceptual rift
between types like formal language values and, say, the rational numbers.

Now, to the example:
The simplest example possible is to describe induction itself. We start of
course by defining the natural number system. So we construct this object
called Naturals, and we know (somehow) that 'zero' is in it, the particular
kernel of this system's values. However, zero isn't some world-wide common
concept, it's just a selector in that namespace. Because of this, we have
to deal with the object as a formal model of the zero of the natural numbers.

Now, an object means nothing without its behavior. Our object 'zero' must
have one slot in the formal model of natural numbers. We'll call it
'successor', which just gives us the next natural number. (We'll leave
addition out of this model for simplicity's sake.)

Every time you call 'successor', you want the result to also belong to
Naturals, and you want the result to have the same behavior as 'zero'. So
if we take the single-quote to represent successor, we have 1=0', 2=0'',
3=0''', etc.

We *could* make 1, 2, 3, and its kin permanent residents of Naturals by
defining all clones of 0' (as well as 0' itself) to be denoted by 1, for
example. This is a slight stretch of the meta-behavior idea of Slate, in
that we can definitely show that removing the 'clone' slot of 1 helps in
avoiding new denotations of the same concept that we want 1 to denote, but
it's harder to accept the idea that all invocations of the 0' expression
return 1 simply because we said so. :) There's another approach where you
leave all the instances in Naturals besides 'zero' annonymous and handle
the naming issue through explicit denotations like using sequences of
digits as a decimal representation. This means that the object in the
Natural namespaces should be the reified expression of applying 'successor'
to 'zero'. This promotes an interesting course of action, where even
algebraic symbols are implemented as slots in the namespace whose type they
are dynamically using. If we do this, then our means of specification will
have to enumerate the number of 'successor' applications made to obtain the
desired number, which is a simple act of lambda-abstraction.

Of course, the natural numbers as I've discussed are hardly useful except
for counting or generalization to a grammar or syntax. The really
interesting examples include the Integers and Rationals, where the
specifying equations are everything. Primitives could of course supply
evaluation of the expressions in that case, without losing the generality
of a full symbolic algebra system. However, within co-inductive types like
Rationals, there would be no kernel values, and everything would be
specified by equations and embeddings into the integers.

This is all preliminary, and slightly rambling, but it gets across the
intent of what I'm working on right now. Tomorrow I'll describe how most of
this uses meta-behavior of all of the different objects involved in order
to implement the idea. I'd also like to discuss how this relates to
primitives, as well as the detailed object structure of the expressions and
equations that matter in a system like this.

Thanks,
~