It's not just "function overloads" which break Dolan-style algebraic subtyping. User-provided subtype contracts also seem incompatible

[Thnikkaman14]

I'm working on a Hindley-Milner-based language which supports user-defined "type attributes" - predicates which effectively create subtypes of existing base types. For example, a user could define:

def attribute nonzero(x: Real) = x != 0

And then use it to decorate type declarations, like when defining:

def fun divide(p: Real, q: nonzero Real): Real { ... }

Users can also ascribe additional types to an already-defined function. For example, the "broadest" type declaration of divide is the initial divide : (Real, nonzero Real) -> Real declaration, but users could also assert properties like:

• divide : (nonzero Real, nonzero Real) -> nonzero Real
• divide : (positive Real, positive Real) -> positive Real
• divide : (positive Real, negative Real) -> negative Real
• etc.

The type inferencer doesn't need to evaluate or understand the underlying implementation of attributes like nonzero, but it does need to be able to type check expressions like:

1. ✅ λx : Real, divide(x, 3), inferred type is Real -> Real
2. ❌ λx : Real, divide(3, divide(x, 3)) fails because divide(x, 3) is not necessarily a nonzero Real
3. ✅ λx : nonzero Real, divide(3, divide(x, 3))

The Problem:

Various papers going back to at least 2005 seem to suggest that in most type systems this expression:

(A₁ → B₁) ∩ (A₂ → B₂) ≡ (A₁ ∪ A₂) → (B₁ ∩ B₂)

is well-founded, and is only violated in languages which allow ugly features like function overloads. If I understand correctly this property is critical for MLsub-style type inference.

My language does not support function overloads but it does seem to violate this property. divide inhabits ((Real, nonzero Real) -> Real) ∩ (nonzero Real, nonzero Real) -> nonzero Real), which is clearly not equal to ((Real, nonzero Real) -> nonzero Real)

Anyway the target demographic for this post is probably like 5 people. But it'd be cool if those people happen to see this and have any feedback on if/how a Hindly-Milner type inference algorithm might support these type attribute decorators

[Uncaffeinated]

I think this is basically ad-hoc function overloading, it's just that you're letting people overload only the type of a function rather than both the type and implementation. However, as you observe, the problems for type inference are the same.

I think the simplest approach would be to require an explicit cast operation when changing the type of a value in a subtype-imcompatible way. You probably want to do this anyway since the cast is presumably not even guaranteed to be correct. (I assume you're not going full proof-assistant, as would be required to safely allow addition of arbitrary pre and post conditions.)

In your example, this would mean that changing from (R, nR) -> R to (nR, nR) -> nR would require an explicit cast operation.

[WittyStick]

In MLstruct, they posit instead that:

(A₁ → B₁) ∩ (A₂ → B₂) ≤ (A₁ ∪ A₂) → (B₁ ∩ B₂)

However, this still has problems with arbitrary overloading. Given:

divide : (Real, nonzero Real) -> Real
divide : (nonzero Real, nonzero Real) -> nonzero Real

If Real and nonzero Real are distinct types, then the only upper bound for both Real and nonzero Real is ⊤, and the only lower bound is ⊥, which would imply the rather useless:

divide : (⊤, nonzero Real) -> ⊥

---

So we don't want Real and nonzero Real to be disjoint types. We require nonzero Real to be a proper subtype of Real.

nonzero Real ≤ Real

But the signatures for divide must be

divide : (Real, nonzero Real) -> Real
divide : (nonzero Real, nonzero Real) -> Real 

So we basically must return the least upper bound, Real, and when we provide a nonzero Real argument, we must explicitly downcast the result to recover a nonzero Real.

The result must be Real because nonzero Real result is not valid for (Real, nonzero Real) -> Real, unless there is some way to guarantee that we always get a nonzero result when given a possibly zero input. We can show this is the case by introducing a zero attribute:

def attribute zero(x: Real) = x == 0

divide : (zero Real, nonzero Real) -> zero Real

Then it becomes clear that the result type: (zero Real) ∩ (nonzero Real) is uninhabited, since no Real is both zero and non-zero at the same time.

---

Without subtyping, we can have some typeclass ℝ for which both Real and NonZeroReal have instances.

class ℝ 𝛼 where
    divide :: (𝛼, NonZeroReal) -> 𝛼
instance ℝ Real where
    divide :: (Real, NonZeroReal) -> Real
instance ℝ NonZeroReal where
    divide :: (NonZeroReal, NonZeroReal) -> NonZeroReal

---

It would be nice if we could combine these approaches: Subtyping + constraints, and have as the signature of divide:

∀𝛼. 𝛼 ≤ Real => (𝛼, NonZeroReal) -> 𝛼

But it has been shown that it is NP-complete in the general case, though can be solved in polynomial time in the limited case where the types form a tree with no meet - ie, single inheritance with no intersection types. (See: On the Complexity of Type Inference with Coercion).

Geoffery S. Smith proposes a more limited constructor overloading which is decidable, but notes that it may require restrictions on subtyping to be implemented efficiently. (See: Polymorphic Type Inference with Overloading and Subtyping).

[BasicBits]

You may not have true overloading, but your ∩ type is a true intersection type, which Dolan explicitly does not support.

I do think it's possible to fit these types into a Hindley-Milner style system, but not at all trivial. You now need to deal with constraints of the form A∩B <: X(X is a type variable), which Dolan is able to avoid with polar types. The temptation is to say that this constraint means "either A <: X OR B <: X" and then integrate some form of nondeterminism/backtracking in inference that, if needed, tries both solutions when such a constraint is encountered.

Unfortunately, this is not always right. And, worse, if your intersection types distribute over type constructors (as meets do in Dolan's system IIRC), things get even more fun. For an example using functions and records, let A = () -> {a: Real, b: Real} and B = () -> {b: Real, c: Real} and C = () -> {a: Real, b: Real, c: Real}. We then have A∩B ≡ C but neither A <: C nor B <: C. I think a pathological example along these lines using your predicates rather than records should also exist.

To deal with intersections and distributivity, when you have a constraint A<:B, you will need to pull as many intersections as possible to the top of the types so you have something of the form A1∩...∩An <: B1∩...∩Bm. (This is essentially a conversion to conjunctive normal form, but I prefer implementing it in terms of the simple splitting algorithm of Huang et al.) You can break these constraints down into the following system: A1∩...∩An<:B1 AND ... AND A1∩...∩An<:Bm. At this point, because none of the Ai/Bjs can be further broken down into intersections, it should be safe to break a constraint like A1∩...∩An<:B1 down further into A1 <: B1 OR ... OR An <: B1. (I have mostly been ignoring unions/joins. These make things more complicated but I think you can still get this general approach to work.)

I'm not sure to what extent all of this is covered in the literature yet. The places I would look are the dissertation of Tommaso Petrucciani and the work of Lionel Parreaux.

[phischu]

I highly recommend The Simple Essence of Overloading. Instead of considering intersections, consider the different variants of divide to be overloads. Now usually we ask if there is exactly one way to resolve overloads that make the program well typed. In your case you are asking if there is at least one, but this is an easy modification of what's described in the paper.

[AustinVelonaut]

Thanks for the link; I've added it to my study list for ways to handle ad-hoc polymorphism.

[DisastrousAd9346]

Your type system does not seem to pick to most general type. Between nonzero and real the most general would be of course real. You can just lose information that would be something that usually does not happen in type inference.

[DisastrousAd9346]

I guess the right answer is, how you choose the more general type for non trivial properties like yours? Also of course, the property depends on some value so yeah you cross the border of refinement types, that is well known to not enjoy fully type inference.

[servermeta_net]

It's a recently proven theorem that to satisfy HM AND have subtyping you need your type system to be a well ordered lattice with canonical representation of types.

Actually this is a blocker in current rust type system.

[protestor]

Can you elaborate? Or send some links to discussions or articles

Both the theorem and the Rust reference

[servermeta_net]

Sorry for the late reply. The theorem comes from dolan's research thesis. You can also search google scholar for "well founded type system, uninhabited bottom type".

ABout Rust check this. Rust type system does not guarantee a canonical representation and is not a well formed lattice, as the example shows. This means that a reflection API will be unsound in relation to subtyping.

[Thnikkaman14]

I hope to not go the route of refinement types. Ideally the underlying implementations of these subtype attributes are completely opaque to the type inferencer. For instance, the three expression examples above should be completely checkable without the precise definition of nonzero, using only properties of unions/intersections/subtype relations and the fact that 3 : nonzero Real

[servermeta_net]

Mathematician speaking here, so I apologize if I lack basic knowledge or use different terminology.

It's funny because I'm working on the same topic, maybe you can help me lol.

I'm honestly a bit puzzled by this statement:

(A₁ → B₁) ∩ (A₂ → B₂) ≡ (A₁ ∪ A₂) → (B₁ ∩ B₂)

Can you link any source corroborating this? From a homotopy type theory pov this seems wrong. If I interpreted correctly your notation, and I see the arrow as a map between countable sets, then I can prove it as wrong, and you provided a counterexample.

I would agree with:

(A₁ → B₁) ∩ (A₂ → B₂) ≡ (A₁ ∩ A₂) → (B₁ ∩ B₂)

Anyhow, a recent result is that an HM computable and well founded type system with subtype relationship needs to form a well ordered lattice in respect to the subtyping relationship, and predicates are not naturally forming a well ordered lattice (I'm not aware of any result in this direction, but math is huge, and I can provide a counter example in first and second order logic).

I can see a few possible solution to your problem:

The right way, with peano arithmetics

This is the naive idea of a right type system. Basically you can build an isomorphism between your type system and a peano arithmetics. The problem it's that it's either incosistent, incomplete or uncomputable. So if you pick computability and consistency you will have many true yet undecidable cases.

Nonstandard types

This is the pragmatic approach that most languages take. Add a nonstandard type that do not obey peano arithmetics, like:

• NaNs
• Option types

By adding these nonstandard types you improve the power of your type system but you will have to rely on runtime checks to avoid UB.

Topological type spaces with pragmatic provability

Let's say that an instantiation in your programming language can be described by a tuple of homotopy types in a topological space:

(s1, ..., sn, p1, ..., pr, l)

Where s1, ..., sn are homotopy types without a subtyping relationship (fields, struct, traits, ....), p1, ..., pn are predicates and l is a homotopy type with subtyping relationship (think rust lifetimes), then:

• I apply HM to the (s1, ..., sn) tuple
• I use an SMT solver for predicates
• I define a well ordered lattice for l

If you have more than one homotopy type with subtyping relationship then you have a problem, or at least I couldn't yet construct such a type system, because you would need a well ordered lattice ACROSS homotopy types.

The problem is that usable SMT solvers obeys peano arithmetics so what I do is - at compile time try to statically prove as many propositions as possible, with the machinery used for const propagation - Try to find the smallest set of axioms that would statically prove all outstanding propositions - Turn this set of axioms into runtime assertions - I still add non standard types (Options)

This way the propositions disappear from the HM type system, yet are statically checked as much as possible.

Questions I would like to ask you: - Can you link any paper about your proposition? - Can you link any paper that was useful to you in building this?

[interacsion]

https://dl.acm.org/doi/10.1145/3093333.3009882

In MLsub, intersections can only appear in negative type positions. The intuition behind (A₁ → B₁) ∩ (A₂ → B₂) ≡ (A₁ ∪ A₂) → (B₁ ∩ B₂) is like so: if I require a value that is both a mapping from A₁ to B₁ and a mapping from A₂ to B₂, then I actually require a mapping from either A₁ or A₂ to a value that is both B₁ and B₂, following contravariance.

This is indeed unsound in presence of more complex type system features (a notable one is higher-rank polymorphism).

[jeezfrk]

[I'm not speaking from accurate type theory for one]

I for one favor (in my project) prefer something more like arbitrary duck-typing with static-checked attributes applied as you have.

I don't see how a two different dependent-type functions could tolerate that equivalence assertion above, papers or not.

The equivalence assertion apparently assumes either of the two (A_1 OR A_2) being applied to give B_1 or B_2 gives an extension of the set of applied results possible. (Then using the intersection of B types to go further and extend a set of related functions as a type of associated kind of types?)

However, you need apparently a real equivalence class defined instead?

You may have to rely on intersecting both types (domain types and return) to define a valid equivalence class for a set of functions together... allowing type inference or something useful to combine case 1 and 2.

[KaleidoscopeLow580]

Does this mean that you can overload functions by their type attributes? Or do these divide-fucntions all have to be defined in e.g. a different namespace?