[Haskell-cafe] Type level natural numbers

[Mateusz Kowalczyk]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

On 03/04/13 20:42, Mateusz Kowalczyk wrote:
> 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).
> 
> 
> _______________________________________________ Haskell-Cafe
> mailing list Haskell-Cafe at haskell.org 
> http://www.haskell.org/mailman/listinfo/haskell-cafe
> 
Forgot package link -
http://hackage.haskell.org/packages/archive/type-level-natural-number/1.1.1/doc/html/TypeLevel-NaturalNumber.html
- -- 
Mateusz K.
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v2.0.19 (GNU/Linux)

iQIcBAEBAgAGBQJRXIcPAAoJEM1mucMq2pqXRX4QAILITsFLspe6Fd95uV8HUbSv
rwoCalPkaUaYBsJ2tAC27dlBPjmom25u6ISIaiiDI+XHyoQiMza+hQostIny6pR3
vjlhxuBFZQYHxJHJd90hUdDQ4+OXt+aPJbMvgwbA72yJsb95Kv1CVagF3U3wGb3X
VPSAAgbAf0NXNbVeOF7n73g1iCCfdf4QylKc64WsJInVgqBOc7XKHLGwXuhtJ+IF
1UAoS0AOYoKe7LCoDRjkKOQYqbUs6nY8GdgDNEsDdcev7GWQ3zFafGXAfVPYoe1u
I1Af5puQEJFsyvVF/AwDPR5INiVGPR6bTYAJ/oW3/3tpEswK8+tvJsqYjsPWzY8Y
7R39oYcglFe4QoixtpDtoNB9up6rT4hWbUF1TQml20IceNIvbi3+DIyZEIwgUfXg
d+CpBe1AAyCZQreF1LpQbrJc1by7pHS9+LYq4od+VClXFZJPjQLUR3qZjS6PgH4m
n5zpPzvatKY/HfMcApxW8v25ZKfOLLJGUFZ6tl8Z5go8CN9i9ptkeyrJYTyRs6FQ
K66RBQlghNFaCYTJnC6+TtNRUdKAwm0+kGMjHGrp0MGY6yasHddhD7NZ177iIKwV
MOmqXsWrFPcEuhq08OzUZd0lQL+KgQF5XEnf3mTXo1Bj1lQPoUY2ERCvtfZl6B/V
6XkP7asJSYUKXYhAp/cJ
=fw3P
-----END PGP SIGNATURE-----