Mateusz Kowalczyk
About two weeks ago we got an email (at ghc-users) mentioning that comparing to 7.6, 7.7.x snapshot would contain (amongst other things), type level natural numbers.
I believe the package used is at [1].
Can someone explain what use is such package in Haskell? I understand uses in a language such as Agda where we can provide proofs about a type and then use that to perform computations using the type system (such as guaranteeing that concatenating two vectors together will give a new one with the length of the two initial vectors combine) however as far as I can tell, this is not the case in Haskell (although I don't want to say ?impossible? and have Oleg jump me).
It most certainly will be possible to do type level arithmetic. For one use-case, see Linear.V from the linear library [1]. The DataKinds work is already available in 7.6, allowing one to use type level naturals, but the type checker is unable to unify arithmetic operations. Cheers, - Ben [1] http://hackage.haskell.org/packages/archive/linear/1.1.1/doc/html/Linear-V.h...