Induction, Co-induction, and Types in Slate

[Brian T. Rice]

At 09:15 PM 3/29/00 +0200, Massimo Dentico wrote:
>"Brian T. Rice" wrote:
>> 
>> 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. :)
>> 
>> [...]
>
>Just for checking my understanding:
>
>1) you re-introduce the concept of class in terms of objects (prototypes);

Yes, I'm using the namespace idea to act as "birthplace" for objects, and
coercing objects made there to be of a certain type and specified by
external information like equation. Actual values would simply be objects
whose state is specified by completely solved equations.

>2) a class "produces" its instances through invocation of slots;

Well, it produces them through a kind of cloning of objects that provide
the desired slot-behavior. Whether that's done by the enclosing namespace
or a kernel of objects doesn't matter too much.

Actually, if it's possible, it'd be nice to somehow separate the namespace
enclosing the objects of a certain type from the object acting as the
class, but I don't see an immediately obvious way to do this that doesn't
seem like a hack. My objection (to my own idea :) is that in order to say
"(Naturals new)" to get a new natural number, you have to have a slot in
the Naturals named "new" which isn't a natural number. However, I suppose
it's not having equational expressions reference it means it has no "value"
as other Naturals would.

>2) you blur the distinction between expression languages for values and
types;

Yes, that sums it up. The whole idea is to place types at the first-order
level, which constitutes real linguistic reflection (as done in Napier88
and possibly other languages(?)). The objects produced by this method
aren't quite "self-describing" in the usual sense, but the only part of
their definition that's not encapsulated is the equational part and its
semantics, which are provided by the enclosing namespace structure. I don't
think that this is too bad a trade-off.

>3) you introduce the possibility of denoting (I'm not sure about this term)
>   non-computable functions through co-inductive types.

That term works fine. Consider "clone" to be the kernel of the co-inductive
typing possibilities in Slate, since it allows you to re-create an object
many times and consider each clone (which is just a reference to the
original object with odd meta-behavior) as a new object with value
discovered only by inspecting equations referencing it within the namespace.
 
>> Now, to the example:
>[snipped Peano's definition of natural numbers in Slate]
>> Of course, the natural numbers as I've discussed are hardly useful except
>> for counting or generalization to a grammar or syntax.
>I Agree.

>> 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.
>
>For example, in the case of (a sub-set of) integers is possible to use
directly
>machine instructions; so you intend to annotate the "classes" (or, better,
the
>slots) with these primitives. Shortly: equations for proofs, symbolic
manipulations,
>and primitives for efficient evaluations. Is it correct?

Absolutely. I'd like full mathematical generality in the type system and
the primitives to act as annotations of a sort. I'm not positive about the
way these annotations could be cleanly inserted into the system, so any
suggestions from Tunesers along these lines (with explanation of the
details) would be quite welcome. :)

>> 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.
>
>The classical representation with integers pairs.

Well, it's not just that I'm saying that rationals are objects with two
integers as state. Those two integers actually mean something about that
integer in this typing system I propose.

To illustrate, say I have "x=3/4". In my current system, "x" would be
cloned as a new object with *no* state in the Rationals space to produce a
result for the equation "x*4=3". The way this would get allocated is as
follows: we represent the equation in usual object-oriented parsing terms
as an eqnExpression which references the integers "3" and the
productExpression of "x" and "4". Looking at this example, we see that the
integers are used as a kernel for the rationals without actually coercing
them to be rationals. The expression types are ambiguous, since such an
equation could be either an integer or rational, or some restricted subtype
like positive rational or integer. However this is handled, the fact
remains that such a system of types can be specified equationally, rather
than strictly by implementation.

>> 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,
>> ~
>
>I like your approach that aims to minimize and unify concepts but still
>I'm not convinced by your semantic/syntactic framework. However, I'm
>following your work with interest.

Well, if I can manage to pin down how the meta-behavior system works, upon
which a lot of this hinges, then it should become much more clear how the
system will work in an efficient and semantically-solid way.

>Best regards.
>
>-- 
>Massimo Dentico

~