[Haskell-cafe] Type level natural numbers
bgamari.foss at gmail.com
Thu Apr 4 15:18:28 CEST 2013
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 .
> 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 . 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
More information about the Haskell-Cafe