[m-dev.] documenting typed insts

[Zoltan Somogyi]

2020-01-07 20:39 GMT+11:00 Julien Fischer<jfischer at opturion.com>:
>     :- type tm ---> walking ; cycling ; car.
>     :- type fruit ---> lemon ; orange ;  apple.
>     :- inst citrus for fruit/0 ---> lemon ; walking.
> 
> I get an error about the inst defintion.
> 
>    foo.m:010: Error: inst `citrus'/0 is declared to be for type `foo.fruit'/0, but
>    foo.m:010:   its top level function symbol `walking'/0 is not a function symbol
>    foo.m:010:   of that type.
> 
> Or is the commit message referring to something else?

It is referring to something else.

If you have

:- type t1 ---> f1(...) ; f2.
:- type t2 ---> f1(...) ; f2. % in a different module, of course
:- inst i1 for t1/0 ---> f1(ground, ..., ground).

the inst i1 is valid, so you don't get the above error message. That's good.
What is not good is that you *also* don't get an error message if one
of your predicates has an argument of type t2 which is declared to have
a mode such as "in(i1)". In this case, the programmer has declared
that i1 is for use on values of type t1, but it is being used on a value
of type t2. The code to detect this kind of problem has not been
written yet, mostly because it requires the mode checker to handle
a sixth task along with its current five, and the interactions can be
very complex. (For example, one would want to detect this error
even when it occurs in a subterm of an argument of a higher order
value.)

However, specifying what type an inst is *meant* for is useful
documentation even without its implicit assertion (that it is not used
on values of any other type) being enforced, which is why it can be
documented now anyway.

Zoltan.