### More commutative operators

3 Aug 2013 01:24 am### The final API for (<κ)-commutative operators

Last time I talked about generalizing the notion of quasi-unordered pairs to the notion of quasi-unordered multisets. The final API from last time was:type Confusion :: * → *
isSingleton :: Confusion a → Maybe a
size :: Confusion a → Cardinal
observe :: Ord r ⇒ (a → r) → Confusion a → [(r, Either (Confusion a) a)]

Now, every function of type `Confusion a → b`

is guaranteed to be a (<κ)-commutative operator, where κ is implicitly given by the definition of `Confusion`

. However, we have no way to construct the arguments to those functions! We need to add a function ** confuse :: ∀λ. 0<λ<κ ⇒ Vector a λ → Confusion a** so that we can construct arguments for our (<κ)-commutative operators. Of course, rather than using bounded quantification and the

`Vector`

type, it'd be a lot easier to just define a type which incorporates this quantification directly:
data BoundedList (a::*) :: Nat → * where
BLNil :: BoundedList a n
BLCons :: a → BoundedList a n → BoundedList a (1+n)
data NonEmptyBoundedList (a::*) :: Nat → * where
NEBLSingleton :: a → NonEmptyBoundedList a 1
NEBLCons :: a → NonEmptyBoundedList a n → NonEmptyBoundedList a (1+n)

Now we have:
confuse :: NonEmptyBoundedList a κ → Confusion a
type Commutative a b = Confusion a → b
runCommutative :: Commutative a b → NonEmptyBoundedList a κ → b
runCommutative f xs = f (confuse xs)

Ideally, we'd like to take this a step further and have a version of `runCommutative`

which returns a variadic function of type `a → ... a → b`

for the appropriate number of arguments. This way we'd be able to call them like regular curried functions rather than needing to call them as uncurried functions. There are a number of ways to do variadic functions in Haskell, but discussing them would take us too far afield. Naturally, implementing them will amount to taking advantage of the 4-tuple for folding over multisets, which was defined last time.

### Handling κ-commutative operators

Continuing the theme, suppose we really want to handle the case of κ-commutative operators rather than (<κ)-commutative operators. For simplicity, let's restrict ourselves to finite κ, and let's pretend that Haskell has full dependent types. If so, then we can use the following API:

type Confusion :: * → Nat → *
extractSingleton :: Confusion a 1 → a
size :: Confusion a n → Nat
size _ = n
data ConfusionList (r, a :: *) :: Nat → * where
CLNil :: ConfusionList r a 0
CLCons :: r → Confusion a n → ConfusionList r a m → ConfusionList r a (n+m)
observe :: Ord r ⇒ (a → r) → Confusion a n → ConfusionList r a n
confuse :: Vector a (1+n) → Confusion a (1+n)
type Commutative a n b = Confusion a n → b
runCommutative :: Commutative a n b → Vector a n → b
runCommutative f xs = f (confuse xs)