3 Apr 21:42 2013

## Type level natural numbers

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

2013-04-03 19:42:16 GMT

2013-04-03 19:42:16 GMT

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). -- -- Mateusz K.