[m-rev.] for review: restrict some typeclass definitions in .int{, 3} files to be abstract

[Zoltan Somogyi]

On 2023-08-02 05:24 +02:00 CEST, "Peter Wang" <novalazy at gmail.com> wrote:
> I think where this problem will arise most in practice is when you try
> to print out a term:
> 
>     print([1, 2, 3], !IO)
> 
> Is that a list(int) or non_empty_list(int)? The end result is the same,
> but the compiler doesn't know that.

In virtually all cases, a predicate that normally takes as input
a value of whose type is the supertype, when given a value that can
also be described with the subtype, will do exactly the same thing.
After all, the subtype is similar to an inst on the supertype, and it can
restrict the set of paths that execution can take through the body of
the predicate, but on each path that in that restricted set, it wil execute
exactly the same code.

This means that the only possible source of differences between

- treating print([1,2,3], !IO) as being list(int) and
- treating print([1,2,3], !IO) as being non_empty_list(int)

is an explicit type test in either print, or in some predicates/functions
in its call tree. So in this case, the reason "the compiler doesn't know that"
is that the compiler does not know whether print or its call tree
contain explicit type tests.

We could make the point moot by imposing a rule that when there is
an ambiguity between subtype and supertype, the compiler must choose
the subtype. In this example, that would mean treating [1,2,3] as non_empty_list.

That would still leave ambiguities between two different subtypes.
For example type pair(list, list) could have two subtypes pair(empty_list, list)
and pair(list, empty_list), and [] - [] would belong to both subtypes.
We could document that any such ambiguities could be resolved by the user
by defining a subtype that imposes the constraints imposed by both subtypes.
This subtype would be pair(empty_list, empty_list) in this case. The point
is that if the supertype and all its subtypes form a complete lattice,
then every term has a unique types that best describes it.
 
> These ambiguities can be resolved, but the compiler warns about the
> predicate using a lot of overloaded symbols. Maybe we should raise the
> default value of --typecheck-ambiguity-warn-limit.

Due to the exponential nature of the memory and CPU time cost
of ambiguity, I don't think that will work in general. It may help in a few cases,
but it will still be overwhelmed in a significant number of cases.

>> > Perhaps we can point out which lines the terms with ambiguous types
>> > occur on.
>> 
>> As shown above, this already happens. (Though if e.g. [] occurs
>> more than once on a line, you get just one message for that line.)
>> 
> 
> In term_conversion.m, it took me some trial and error to find the
> location where I should place the type qualifiers.

I am not surprised; it is not that trivial a problem. But you did know
which line to modify. We can't do better than that until we expand
contexts to include either column information, or some other info
(such as byte offsets in the source file) that can be converted
to column information.

>> If yes, then I want to keep the definitions of empy_list and non_empty_list
>> commented out, but with the comment updated to reflect this diagnosis.
>> The reason for that is that I don't like the idea of either us, or other Mercury
>> programmers, having to go around adding explicit type qualifications to lots
>> of nils and cons just to get the number of type assignments in the type checker
>> below the ambiguity threshold.

The attached diff does this.

Zoltan.
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Log.enel
Type: application/octet-stream
Size: 491 bytes
Desc: not available
URL: <http://lists.mercurylang.org/archives/reviews/attachments/20230802/c91f84f7/attachment.obj>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: DIFF.enel
Type: application/octet-stream
Size: 4411 bytes
Desc: not available
URL: <http://lists.mercurylang.org/archives/reviews/attachments/20230802/c91f84f7/attachment-0001.obj>