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

[Dominic Steinitz]

Thanks for this and I apologise for not being clear. I really wanted to know why the type checker couldn’t figure this out for itself.

It seems one has to write e.g. (which is really equivalent to your synonym)

> (n+ q) ~ p, (q + n) ~ p

in the type signature if one wants commutativity.

Another thing I noticed was

> *Main> :t outer muPrior sigmaPrior bigH bigSigmaY
> outer muPrior sigmaPrior bigH bigSigmaY
>   :: (KnownNat (2 + q), KnownNat q, (1 <=? (2 + q)) ~ 'True) =>
>      (R (2 + q) -> R 2)
>      -> (R 2 -> Sq 2) -> Sq 2 -> [R 1] -> [R q] -> [(R 2, Sq 2)]

So the type checker seems unable to discharge the constraint KnownNat q, (1 <=? (2 + q)) ~ ‘True) even though that *must* be true. Also if q is a KnowNat then surely q + 2 must be a KnownNat so that constraint can also be discharged.

Anyway my (extended Kalman) filter is working now and the type system made sure I didn’t make some of the mistakes that one can make in other languages.

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

On 27 Nov 2014, at 17:22, adam vogt <vogt.adam at gmail.com> wrote:

> Hi Dominic,
> 
> On Thu, Nov 27, 2014 at 3:22 AM, Dominic Steinitz <dominic at steinitz.org> wrote:
>> Is expressing commutativity not possible?
> 
> I think the best we can do is:
> 
> type PlusEqv x y xy = ( (x + y) ~ xy, (y + x) ~ xy )
> 
> And then use "(n `PlusEqv` q) p" instead of "(n + q) ~ p"
> 
> Regards,
> Adam