[Haskell-cafe] Type level natural numbers

[Ben Gamari]

Mateusz Kowalczyk <fuuzetsu at fuuzetsu.co.uk> writes:

> 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.html