[m-dev.] proposed syntax for typed insts

[Zoltan Somogyi]

I am proposing a syntax for typed insts, which we have
long agreed are a good idea.

Currently, inst declarations look like either this:

:- inst Instname(InstArgs) == ...

or like this:

:- inst InstName(InstArgs) ---> ...

I propose that "for TypeName/TypeArity" be added
between the InstName(InstArgs) and the "==" or "---->",
so that they look like this:

:- inst InstName(InstArgs) for TypeName/TypeArity == ...

This can be achieved by adding "for" as a new xfx operator
with a priority that is lower than the priority of either --->,
which is 1179, and of "==", which is 700. (In a perversity
inherited from Prolog, lower priorities bind more *tightly*.)
That way, the part of the term that we read in for an inst
definition with have InstName(InstArgs) for TypeName/TypeArity
in the slot that used to have just InstName(InstArgs)
(the slot being the left argument term of ---> or ==), and
everything else will remain the same as far as parsing
the inst definition is concerned. ("inst" is prefix op with
priority 1199, so it binds loosest of all these operators.)

I am attaching a program that reads in terms and prints them
showing the priorities of the relevant ops, two inst definitions
from tree234.m (one with ---> and one with ==), both in their
current untyped form and in the proposed typed form, and the
output of the program on these inst definitions as terms after
"for" is added as an xfx op with priority 500.

What do people think about the proposal? Should the keyword
be something other than "for"? Should we require typed insts
to use :- typed_inst instead of just :- inst? Should the syntax
structure be completely different?

As an aside, is show_ops.m worth adding to extras?

Zoltan.

[Peter Wang]

Post by Zoltan Somogyi
I am proposing a syntax for typed insts, which we have
long agreed are a good idea.
:- inst Instname(InstArgs) == ...
:- inst InstName(InstArgs) ---> ...
I propose that "for TypeName/TypeArity" be added
between the InstName(InstArgs) and the "==" or "---->",
:- inst InstName(InstArgs) for TypeName/TypeArity == ...

It looks okay to me.

Previously I had imagined the same syntax but with ":" instead of "for".
Too bad ":" would bind tighter than the "/" in TypeName/TypeArity.

Peter

[Julien Fischer]

Hi,

Post by Zoltan Somogyi
I am proposing a syntax for typed insts, which we have
long agreed are a good idea.
:- inst Instname(InstArgs) == ...
:- inst InstName(InstArgs) ---> ...
I propose that "for TypeName/TypeArity" be added
between the InstName(InstArgs) and the "==" or "---->",
:- inst InstName(InstArgs) for TypeName/TypeArity == ...
This can be achieved by adding "for" as a new xfx operator
with a priority that is lower than the priority of either --->,
which is 1179, and of "==", which is 700. (In a perversity
inherited from Prolog, lower priorities bind more *tightly*.)
That way, the part of the term that we read in for an inst
definition with have InstName(InstArgs) for TypeName/TypeArity
in the slot that used to have just InstName(InstArgs)
(the slot being the left argument term of ---> or ==), and
everything else will remain the same as far as parsing
the inst definition is concerned. ("inst" is prefix op with
priority 1199, so it binds loosest of all these operators.)

I have no objection to adding "for" as the new operator.

Post by Zoltan Somogyi
I am attaching a program that reads in terms and prints them
showing the priorities of the relevant ops, two inst definitions
from tree234.m (one with ---> and one with ==), both in their
current untyped form and in the proposed typed form, and the
output of the program on these inst definitions as terms after
"for" is added as an xfx op with priority 500.
What do people think about the proposal? Should the keyword
be something other than "for"? Should we require typed insts
to use :- typed_inst instead of just :- inst? Should the syntax
structure be completely different?

At this stage I would say no, but it depends a bit on the
details of how typed insts are going to fit into the language.
(For example, in their presence will we eventually restrict what
untyped insts are allowed?)

Post by Zoltan Somogyi
As an aside, is show_ops.m worth adding to extras?

Sure.

Julien.

[Zoltan Somogyi]

Post by Julien Fischer
At this stage I would say no, but it depends a bit on the
details of how typed insts are going to fit into the language.
(For example, in their presence will we eventually restrict what
untyped insts are allowed?)

The obvious first step is simply to record the type with the inst's definition,
and insist on *that* type matching the inst, not just *some* accessible type,
as we do now.

For this, we need to decide *what* type information we allow to be specified
for an inst.

I expect that 99% of defined insts involve function symbols from only one
type constructor. The list_skel and uniq_tree234 insts are both like that.
However, I can see that in some cases, one would want to define not just
insts like this:

:- inst at_most_one_key(K, V) for tree234(TK, TV) ==
bound((
empty
;
two(K, V, uniq_tree234(K, V), uniq_tree234(K, V))
)).

but also insts like this:

:- inst at_most_one_yes_key(EK, V) for tree234(maybe(TEK), TV) ==
bound((
empty
;
two(yes(EK), V, uniq_tree234(K, V), uniq_tree234(K, V))
)).

(The more realistic application I am thinking of is insts
that represent patterns involving more than one node type
in abstract syntax trees, but I didn't want to invent an AST
just for this post :-()

A type constructor applied to a list of unique type variables
can be represented by just its name and arity (as my original
proposal showed), but this shorthand doesn't work if the type
constructor's arguments are not variables (or aren't *distinct*
variables).

One could define at_most_one_yes_key in terms of at_most_one_key,
by providing the appropriate inst (bound(yes(EK)) for K, so this is
a tradeoff between simplicity of implementation and ease of use.

The second step would be modifying the mode checker to require
that defined inst that *do* specify what type or type template,
as above) they are supposed to apply to *are* only applied to
that type or type template.

At that point, we could (third step) announce the new capability,
and (fourth step, after waiting while everyone installs a new compiler)
we could start using it ourselves.

Fifth step, we could eventually generate warnings for inst definitions
that do not specify a type template. After the next release with that
warning, we could (sixth step) generate errors for such insts,
effectively deleting them from the language.

I expect that the second step would be by far the hardest to code,
especially if we decide to allow nontrivial type templates.
The longest would be the waiting periods (at least a few months,
probably a year) on both sides of step five.

Anyone see any flaws in the above? Would anyone want to keep
untyped insts around forever?

BTW, I added show_ops.m to extras, after documenting it a bit.

Zoltan.