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:infix <:
(<:) :: Ty -> Ty -> Bool
x <: y = x `subtype` y -- for some auxiliary subtype function
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 &&.t1 <: t2 <: t3
(You could maybe also extend this to any type Monad m => m a using >>= instead of &&?)
1 comment:
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
Post a Comment