[Prev][Next][Index]
Parameterized sorts for LSL!
I've heard from Jim Horning about parameterized sorts.
He says:
Yes, LSL needs parameterized sorts. No, I don't know of anyone who has
committed time to design them. A year or so I designed a "poor man's
version," in which names could have components separated by $, and
components could be substituted separately. The Achilles Heel of this
proposal is non-confluence (the same sequence of components could come from
two very different sequences of substitutions). So I concluded that, at a
minimum, there has to be some sort of bracketing, Set[T], rather than
Set$T. But that's as far as it went at that time, I think.
He also asked about me remark:
In case anybody wants to do this, it would also be convenient to
have parameterized trait function names as well; for example equalAs[T].
It may help to quote his question:
I didn't understand your remark about parameterized function names: Since
they already contain a full signature (which can often be elided), they are
parameterized by all the types in the signature. Or were you simply
suggesting that parameterized types be allowed in signatures? I agree that
the latter would be essential to any useful design for parameterized sorts.
My reply was as follows.
No, in Larch/C++ we treat = in assertions as a call to a trait function
named \equal_as_T. For each type there is a point-of-view of equality for
that type. For example, consider pairs of intergers, IntPair, and triples
of integers, IntTriple. If we want IntTriple to be a subtype of IntPair,
then we will need to define \equal_as_IntPair for combinations of IntTriple
and IntPair arguments. We would also define \equal_as_IntTriple for IntTriple
arguments. Now suppose we've defined a trait like this, but in C++ the name
of the type is PairInt instead of IntPair. I need to rename IntPair to
be PairInt
uses IntPairTrait(PairInt for IntPair)
but that won't change the name \equal_as_IntPair to be \equal_as_PairInt.
I have to write...
uses IntPairTrait(PairInt for IntPair,
\equal_as_PairInt for \equal_as_IntPair)
instead. So having trait function names that are parameterized would solve
this problem too. Does that make sense?
Perhaps we could solve this problem in Larch/C++ some other way, but I don't
see how. The problem is that we need both
\equal_as_IntPair : IntTriple, IntTriple -> Bool
and
\equal_as_IntTriple : IntTriple, IntTriple -> Bool
so the signature overloading doesn't help here.
Jim agreed that this was a problem and added a new insight that makes this
kind of thing less specific to Larch/C++.
A very similar problem
shows up if you want to rename "fields" in any of the LSL shorthands. The
shorthands were put in the language to reduce the amount of duplicate
boilerplate; unfortunately, they do so only at the base level, not when
traits are referenced.
That is, you'd like to be able to rename the field foo to bar and have both
__.foo and set_foo be renamed.
This would be possible if you could have their names be something like:
__.[foo] and set_[foo]
Admittedly this isn't the most pleasant syntax.
But it does indicate the (practical) utility of such a mechanism.
Does anyone have a student interested in working on such extensions to LSL
and LP? It seems like OBJ3 would be a place to get some guidance as to how
to proceed. If no one else is doing this, I'm willing to work on it sometime.
Gary
Reference(s):