Re: [Toss-devel] Speagram and typed terms in Toss

[Lukasz K. <luk...@gm...>]

Hi!

> (1) For terms and term rewriting systems, besides the presentation
> based on (extending) the textbook presentation of them, we should
> provide presentation-translation into structures and "Toss systems",
> even if at no point the translation is performed.

I have absolutely no problem with that - in fact I even wanted to
replace term rewriting with structure rewriting in code, but it seems
to be more hassle than it is worth. But I *did* change old speagram
semantics and now require all rewriting rules to be left-linear, with
equality being a special function now. In this way term rewriting is very
similar to structure rewriting - up to copying subterms on the right side.

> (2) Types should be parts of terms. I.e. in the translation to
> structures, when a node corresponds to an instance of a root of a
> term, the node is connected via a "type" edge to a (representation of
> a) term that is its type. The hierarchy ends with a "Type" term whose
> translation has the "type" edge connected to itself ("Type : Type").
> In the textbook presentation, we might require that the arity is >= 1
> and the first argument is always a type, or just extend the standard
> terms to type-carrying terms with a handy syntax like "f(t1 :
> ty_1,...,tn : ty_n) : ty".
>
> (2a) The corollary is that term rewriting rules will match against
> types, where the types come primarily from parsing and possibly from
> some type coercion syntax.

What you are writing here suggests one interesting idea to me:
how about making an experiment and implementing type arc parsing
(i.e. speagram-style parsing) as a Toss game? The only harder part
would be type unification, and for basic types it is not that hard, right?
Maybe I'll take some time and have a shot at this - it looks really very
interesting to me. Especially when you think about one weak point of
the current term system (i.e. old speagram): that disambiguation happens
only after full parse. This both makes the disambiguation rules hard to
understand, and makes the whole system far slower than it should be.
If we have it as a game - and different parses correspond to different
possible moves during the play - then maybe we can use payoffs or some
other mechanism to exclude stupid parses before generating all of them?
I'm not sure that is what you meant - and it might be much harder to do
more complex types and their unification as a toss game - but maybe it
really is worth a try? Write what you think! :)

Lukasz