Mateusz Kowalczyk <fuuze...@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 _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
