[m-dev.] documenting typed insts

[Julien Fischer]

On Tue, 7 Jan 2020, Zoltan Somogyi wrote:

> 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.)

Ok, I see.

> 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.

Yes.

Julien.