<div dir="ltr"><div class="gmail_default" style="font-family:verdana,sans-serif">Where is [1]?</div></div><div class="gmail_extra"><br><br><div class="gmail_quote">On Wed, Apr 3, 2013 at 3:42 PM, Mateusz Kowalczyk <span dir="ltr"><<a href="mailto:fuuzetsu@fuuzetsu.co.uk" target="_blank">fuuzetsu@fuuzetsu.co.uk</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">-----BEGIN PGP SIGNED MESSAGE-----<br>
Hash: SHA1<br>
<br>
About two weeks ago we got an email (at ghc-users) mentioning that<br>
comparing to 7.6, 7.7.x snapshot would contain (amongst other things),<br>
type level natural numbers.<br>
<br>
I believe the package used is at [1].<br>
<br>
Can someone explain what use is such package in Haskell? I understand<br>
uses in a language such as Agda where we can provide proofs about a<br>
type and then use that to perform computations using the type system<br>
(such as guaranteeing that concatenating two vectors together will<br>
give a new one with the length of the two initial vectors combine)<br>
however as far as I can tell, this is not the case in Haskell<br>
(although I don't want to say ?impossible? and have Oleg jump me).<br>
<br>
- --<br>
Mateusz K.<br>
-----BEGIN PGP SIGNATURE-----<br>
Version: GnuPG v2.0.19 (GNU/Linux)<br>
<br>
iQIcBAEBAgAGBQJRXIYYAAoJEM1mucMq2pqXT00P/imTf/Wd7UZ0T0ZPUbM6i3Nj<br>
P5ffEUvUGf5V1jmXub/ibVFv6QHkTigsF/K9VPo13ChtA7u4qnxH7pd+zbTCp6c4<br>
+A4dgKLVvlB+tGSvKzmsJxEtRh/rtv0UMP2RtvKoB7DH2mMv99EDkKmndWaxOI2z<br>
VjAvYFqdi//3O0P9bN9/93KZNUZviHh/5IP8f6HcpCWVDu+Z5CKbzUM6roxsBNM1<br>
a1y6RjQp2SnUFMlJnKbWepRbn2p12dzmMrXzF2UINkTkDTytP+ZIK1ZpS8/qh6i6<br>
q44GUBa2doHxhX9H+Vo3Vims3S0otyVmTQX/b2J1R7FoBl6fsPa+XUeE8RJwfSzm<br>
0Ho75AX39rynO9AJ+/hZQdk6G6VkED/JszWBSnfC56VNB0vdYI4e2mBGny4uL9MU<br>
PnVb+fYk0xuSw7wAqLnVo2ZQqyvN79uNDT4x0uf/6zvkQ8LoSzMr99YwjWI5jo2X<br>
8dqphjPPArX9MV0xCPdkpU6wPHSvEK4fOxJcqDq104+ssJdNr8PXbhtIifa/KE/C<br>
B2jhmwRllbtbg1HGXQ8zWlY+VbE+sc5O2AvhrV14fKF8xkNtLRzvhAWR/cOTXLZ0<br>
hA7r6Jjf4mzQnUBgb/BW8pH6N+UnjkV/JgJ45WHB3PSADU3JspyuG7uJUOCod75e<br>
D/849dOCHHrkYsYEPdJq<br>
=JCfK<br>
-----END PGP SIGNATURE-----<br>
<br>
_______________________________________________<br>
Haskell-Cafe mailing list<br>
<a href="mailto:Haskell-Cafe@haskell.org">Haskell-Cafe@haskell.org</a><br>
<a href="http://www.haskell.org/mailman/listinfo/haskell-cafe" target="_blank">http://www.haskell.org/mailman/listinfo/haskell-cafe</a><br>
</blockquote></div><br></div>