• Andrei Paskevich's avatar
    Mlw: overloaded symbols · 1aa6a8b1
    Andrei Paskevich authored
    This is a prototype version that requires no additional annotation.
    In addition to the existing rules of scoping:
      - it is forbidden to declare two symbols with the same name
        in the same scope ("everything can be unambiguously named"),
      - it is allowed to shadow an earlier declaration with a newer one,
        if they belong to different scopes (e.g., via import),
    we define one new rule:
      - when an rsymbol rs_new would normally shadow an rsymbol rs_old,
        but (1) both of them are either
          - binary relations: t -> t -> bool,
          - binary operators: t -> t -> t, or
          - unary operators:  t -> t
        and (2) their argument types are not the same,
        then rs_old remains visible in the current scope.
        Both symbols should take non-ghost arguments and
        return non-ghost results, but effects are allowed.
        The name itself is not taken into account, hence
        it is possible to overload "div", "mod", or "fact".
    Clause (1) allows us to perform type inference for a family of rsymbols,
    using an appropriate generalized signature.
    Clause (2) removes guaranteed ambiguities: we treat this case as
    the user's intention to redefine the symbol for a given type.
    Type inference failures are still possible: either due to
    polymorphism (['a -> 'a] combines with [int -> int] and
    will fail with the "ambiguous notation" error), or due
    to inability to infer the precise types of arguments.
    Explicit type annotations and/or use of qualified names
    for disambiguation should always allow to bypass the errors.
    Binary operations on Booleans are treated as relations, not as
    operators. Thus, (+) on bool will not combine with (+) on int.
    This overloading only concerns programs: in logic, the added rule
    does not apply, and the old symbols get shadowed by the new ones.
    In this setting, modules never export families of overloaded symbols:
    it is impossible to "use import" a single module, and have access to
    several rsymbols for (=) or (+).
    The new "overloading" rule prefers to silently discard the previous
    binding when it cannot be combined with the new one. This allows us
    to be mostly backward compatible with existing programs (except for
    the cases where type inference fails, as discussed above).
    This rule should be enough to have several equalities for different
    program types or overloaded arithmetic operations for bounded integers.
    These rsymbols should not be defined as let-functions: in fact, it is
    forbidden now to redefine equality in logic, and the bounded integers
    should be all coerced into mathematical integers anyway.
    I would like to be able to overload mixfix operators too, but
    there is no reasonable generalized signature for them: compare
    "([]) : map 'a 'b -> 'a -> 'b" with "([]) : array 'a -> int -> 'a"
    with "([]) : monomap -> key -> elt". If we restrict the overloading
    to symbols with specific names, we might go with "'a -> 'b -> 'c" for
    type inference (and even "'a -> 'b" for some prefix operators, such
    as "!" or "?"). To discuss.
pmodule.ml 45.1 KB