[Toss-devel] Hierarchical Terms and Parametric Polymorphism

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

I brutally realized that "Typed Feature Structures" do not have
parametric polymorphism, not a trace of it. Heck, haven't I kept
repeating that the proposal is not a type system. I still think that
it is a promising language for spelling-out hypergraphs/structures
(with the direct translation I described). There are some options.

The current specification already "oscillates" a bit beyond Typed
Feature Structures in how it uses variables. At present it is somewhat
inconsistent and I planned to bring it consistently back to TFSes by
syntactically forbidding variables in place of supertypes. But now
that I realize you are unlikely to give up parametric polymorphism...

Consider the parametric declaration:

'If' boolean 'then' ?X 'else' ?X as ?X.

What restrictions does it place on how it is used? If it was a TFS, it
would mean that 'then' and 'else' branches are unified: either they
are equal, or there is a common subtype that contains both branches
(but the package is still shared by both positions). So you see, not
at all the parametric type interpretation.

With parametric types as we had them in "Middle Speagram", ?X would
become the common supertype of both branches. With a top type (like
the "type" in the proposal), using 'if-then-else' could never fail in
"Middle Speagram", it would just assume more and more general type.

There is a way to get parametric polymorphism back but going much
beyond Typed Feature Structures:

- add the restriction that two classes can have at most one Least
Upper Bound, this is the part that restricts expressiveness :-(

- add algo for computing Least Upper Bound

- remove the "top" type so that only somehow-related types have LUB

- add a different kind of variables, untyped LUB-variables. They would
not stand for the GLB of what they match with, but the LUB of what
they match with. So the TFS-like GLB-variables would be "sharing
variables", and the LUB-variables would be "type variables".

- Only the LUB-variables would be allowed in place of supertypes.
Their specification would be like the one before my recent fixing,
i.e. ISA would be defined without them and extended to terms with them
by existence of a substitution.

I implemented GLB yesterday, not compiled/tested yet, and it's really
simple. So I think the above is doable.

What do you think?