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

[Peter Wang]

On Wed, 02 Aug 2023 21:54:26 +1000 "Zoltan Somogyi" <zoltan.somogyi at runbox.com> wrote:
> 
> 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.

Right.

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

Or should the compiler choose the base type?

Say non_empty_list(T) was defined in a separate module. Then for this
piece of code:

    T = type_of([1,2,3])

the behaviour would silently depend on what modules are imported,
possibly in an ancestor module. If the compiler always chose the base type
then the behaviour would not be potentially affected by adding module
imports, as the base type must be visible for the code to compile.

In any case, I'm not too eager about having the compiler pick a type.
Maybe with a warning, like when an unbound type variable is implicitly
bound to 'void'.

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

The error for term_conversion.m only gave the line number of the
predicate (specifically of the neck), but not the locations of the
ambiguous symbols.

Peter