Type level natural numbers
-----BEGIN PGP SIGNED MESSAGE----- Hash: SHA1 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. -----BEGIN PGP SIGNATURE----- Version: GnuPG v2.0.19 (GNU/Linux) iQIcBAEBAgAGBQJRXIYYAAoJEM1mucMq2pqXT00P/imTf/Wd7UZ0T0ZPUbM6i3Nj P5ffEUvUGf5V1jmXub/ibVFv6QHkTigsF/K9VPo13ChtA7u4qnxH7pd+zbTCp6c4 +A4dgKLVvlB+tGSvKzmsJxEtRh/rtv0UMP2RtvKoB7DH2mMv99EDkKmndWaxOI2z VjAvYFqdi//3O0P9bN9/93KZNUZviHh/5IP8f6HcpCWVDu+Z5CKbzUM6roxsBNM1 a1y6RjQp2SnUFMlJnKbWepRbn2p12dzmMrXzF2UINkTkDTytP+ZIK1ZpS8/qh6i6 q44GUBa2doHxhX9H+Vo3Vims3S0otyVmTQX/b2J1R7FoBl6fsPa+XUeE8RJwfSzm 0Ho75AX39rynO9AJ+/hZQdk6G6VkED/JszWBSnfC56VNB0vdYI4e2mBGny4uL9MU PnVb+fYk0xuSw7wAqLnVo2ZQqyvN79uNDT4x0uf/6zvkQ8LoSzMr99YwjWI5jo2X 8dqphjPPArX9MV0xCPdkpU6wPHSvEK4fOxJcqDq104+ssJdNr8PXbhtIifa/KE/C B2jhmwRllbtbg1HGXQ8zWlY+VbE+sc5O2AvhrV14fKF8xkNtLRzvhAWR/cOTXLZ0 hA7r6Jjf4mzQnUBgb/BW8pH6N+UnjkV/JgJ45WHB3PSADU3JspyuG7uJUOCod75e D/849dOCHHrkYsYEPdJq =JCfK -----END PGP SIGNATURE-----
-----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-----
Where is [1]?
On Wed, Apr 3, 2013 at 3:42 PM, Mateusz Kowalczyk
-----BEGIN PGP SIGNED MESSAGE----- Hash: SHA1
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. -----BEGIN PGP SIGNATURE----- Version: GnuPG v2.0.19 (GNU/Linux)
iQIcBAEBAgAGBQJRXIYYAAoJEM1mucMq2pqXT00P/imTf/Wd7UZ0T0ZPUbM6i3Nj P5ffEUvUGf5V1jmXub/ibVFv6QHkTigsF/K9VPo13ChtA7u4qnxH7pd+zbTCp6c4 +A4dgKLVvlB+tGSvKzmsJxEtRh/rtv0UMP2RtvKoB7DH2mMv99EDkKmndWaxOI2z VjAvYFqdi//3O0P9bN9/93KZNUZviHh/5IP8f6HcpCWVDu+Z5CKbzUM6roxsBNM1 a1y6RjQp2SnUFMlJnKbWepRbn2p12dzmMrXzF2UINkTkDTytP+ZIK1ZpS8/qh6i6 q44GUBa2doHxhX9H+Vo3Vims3S0otyVmTQX/b2J1R7FoBl6fsPa+XUeE8RJwfSzm 0Ho75AX39rynO9AJ+/hZQdk6G6VkED/JszWBSnfC56VNB0vdYI4e2mBGny4uL9MU PnVb+fYk0xuSw7wAqLnVo2ZQqyvN79uNDT4x0uf/6zvkQ8LoSzMr99YwjWI5jo2X 8dqphjPPArX9MV0xCPdkpU6wPHSvEK4fOxJcqDq104+ssJdNr8PXbhtIifa/KE/C B2jhmwRllbtbg1HGXQ8zWlY+VbE+sc5O2AvhrV14fKF8xkNtLRzvhAWR/cOTXLZ0 hA7r6Jjf4mzQnUBgb/BW8pH6N+UnjkV/JgJ45WHB3PSADU3JspyuG7uJUOCod75e D/849dOCHHrkYsYEPdJq =JCfK -----END PGP SIGNATURE-----
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Mateusz Kowalczyk
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.h...
participants (3)
-
Ben Gamari -
Clark Gaebel -
Mateusz Kowalczyk