Mateusz Kowalczyk | 3 Apr 21:42 2013
Picon

Type level natural numbers


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.
Mateusz Kowalczyk | 3 Apr 21:46 2013
Picon

Re: Type level natural numbers


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.
Clark Gaebel | 3 Apr 21:47 2013
Picon
Picon

Re: Type level natural numbers

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

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Ben Gamari | 4 Apr 15:18 2013
Picon

Re: Type level natural numbers

Mateusz Kowalczyk <fuuzetsu <at> fuuzetsu.co.uk> writes:

> 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.html

Gmane