[Prev][Next][Index]

Parameterized sorts for LSL!?

   Date: Wed, 17 Nov 93 09:48:07 -0800
   From: horning@src.dec.com
   X-Mts: smtp

   Gary,

   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.

Yes, that sounds reasonable.

   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.

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.

	Gary
Reference(s):