-----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@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/... - -- 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-----