Friday, May 09, 2008

N-ary infix predicates

In languages with operator overloading, it's possible to define binary infix predicates such as (using Haskell here):
infix <:
(<:) :: Ty -> Ty -> Bool
x <: y = x `subtype` y -- for some auxiliary subtype function
With arithmetic operators that continue to return elements of the same type (does this make their types endofunctors? I'm no category theorist), so as long as you declare an associativity, the n-ary case is easy to parse. Predicates aren't closed over their input type, though, so in Haskell I can't take the above definition and write:
t1 <: t2 <: t3
But in math, we overload binary predicates to the n-ary case by assuming an implicit "and" between each pair. It would just take a little kludge (but one with the full weight of historical precedent) to let the operator overloading and type system conspire to determine that any binary predicate (i.e., with result type Bool) can be extended to the n-ary case using &&.

(You could maybe also extend this to any type Monad m => m a using >>= instead of &&?)

1 comment:

Anonymous said...

But in math, we overload binary predicates to the n-ary case by assuming an implicit "and" between each pair. It would just take a little kludge...

In Perl 6, this is called "chain" associativity, and could be written
sub infix:«<:» (Ty $x, Ty $y -->Bool) is assoc<chain> { subtype($x,$y) }

Synopsis 6: Subroutines / traits