Induction, Co-induction, and Types in Slate

[Massimo Dentico]

"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