Induction, Co-induction, and Types in Slate
Massimo Dentico
m.dentico@teseo.it
Wed, 29 Mar 2000 21:15:50 +0200
"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);
2) a class "produces" its instances through invocation of slots;
2) you blur the distinction between expression languages for values and types;
3) you introduce the possibility of denoting (I'm not sure about this term)
non-computable functions through co-inductive types.
> 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?
> 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.
> 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.
Best regards.
--
Massimo Dentico