[Haskell-cafe] Why is type level (+) not commutative?
Dominic Steinitz
dominic at steinitz.org
Thu Nov 27 08:22:13 UTC 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 at steinitz.org
http://idontgetoutmuch.wordpress.com
More information about the Haskell-Cafe
mailing list