Orthologic type systems argue for union, intersection, negation — but not distributivity

burny_tech · x · 2026-07-23

A paper on orthologic type systems argues for a type system with union, intersection, negation, variance, and explicit subtype assumptions, but without distributivity.

The core claim is that dropping distributivity is the right choice: A × (B + C) should not be treated as the same type as (A × B) + (A × C). They may be isomorphic, but the paper argues that distributivity conflates extensional equivalence with representational identity.

Original post →

More from Research

Research channel →