Home

Number-Parameterized Types by Oleg Kiselyov

Number-Parameterized Types by Oleg Kiselyov

from the abstract:

This paper describes practical programming with types parameterized by numbers: e.g., an array type parameterized by the array's size or a modular group type Zn parameterized by the modulus. An attempt to add, for example, two integers of different moduli should result in a compile-time error with a clear error message. Number-parameterized types let the programmer capture more invariants through types and eliminate some run-time checks.

Oleg shows several approaches towards encoding numbers into types and using those numbers to check list length, matching sizes for matrices or vectors. Oleg also points out connections to dependent types, phantom types, and shape-invariant programming.

By shapr at 2005-10-03 13:18 | Implementation | Type Theory | other blogs | 9422 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

C++?

Has had this capability to some extent for quite a while, hasn't it? For instance, Boost.Array will only let you swap() and perform comparisons on arrays of the same size. Also, Boost.MultiArray limits most of its interface to dealing with same-dimension arrays. It seems the more generic concept is to have *value*-parameterized types. Unfortunately, C++ only allows builtin types to be compile-time values, although I think Java is more flexible in this area. I don't think Java allows value parameters for generics, though.

By David B. Held at Mon, 2005-10-03 13:51 | login or register to post comments

Yes, mentioned in the related section.

From the abstract:

Section related compares our approach with the phantom type programming in SML by Matthias Blume, with a practical dependent-type system of Hongwei Xi, with statically-sized and generic arrays in Pascal and C, with the shape inference in array-oriented languages, and with C++ template meta-programming.

By shapr at Mon, 2005-10-03 14:54 | login or register to post comments

As an aside, it is very readable

I'm (clearly) not very up on PLT, let alone Haskell, and yet I found this paper not hard to follow (maybe my eyes glazed over starting at section 3.4); kind Oleg was perhaps a little more verbose than other readers needed, but it helped keep me clued in.

By raould at Wed, 2005-10-05 21:34 | login or register to post comments

PDF Version?

Hi there,

Did I miss the link to the PDF version? If so, would you mind posting it?

thanks!

By jimdesu at Wed, 2005-10-05 23:14 | login or register to post comments

link

The link is on the comments page. Unfortunately, the link to the comment page is broken. You can grab the PDF here: http://pobox.com/~oleg/ftp/papers/number-parameterized-types.pdf.

By Greg Buchholz at Wed, 2005-10-05 23:24 | login or register to post comments