[Haskell-cafe] Why is type level (+) not commutative?

27 Nov 2014


      I have a type signature (for an extended Kalman filter as it happens thought that is not relevant)
...
outer ::  forall m n p q .
          (KnownNat m, KnownNat n, KnownNat p, KnownNat q,
           (1 <=? n) ~ 'True, (1 <=? m) ~ 'True,
           (1 <=? p) ~ 'True, (n + q) ~ p) =>
          R n -> Sq n ->
          L m n -> Sq m ->
          (R p -> R n) -> (R n -> Sq n) -> Sq n ->
          [R m] -> [R q] ->
          [(R n, Sq n)]
and my function compiles. If I change (n+ q) ~ p to (q + n) ~ p then I get a type error
...
Could not deduce (p ~ (n + q))
    from the context (KnownNat m,
                      KnownNat n,
                      KnownNat p,
                      KnownNat q,
                      (1 <=? n) ~ 'True,
                      (1 <=? m) ~ 'True,
                      (1 <=? p) ~ 'True,
                      (q + n) ~ p)
Is expressing commutativity not possible?

Dominic Steinitz
dominic@steinitz.org
http://idontgetoutmuch.wordpress.com