[Haskell-cafe] Type level natural numbers

[Clark Gaebel]

Where is [1]?


On Wed, Apr 3, 2013 at 3:42 PM, Mateusz Kowalczyk
<fuuzetsu at fuuzetsu.co.uk>wrote:

> -----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 at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20130403/a1cce805/attachment.htm>