The Monad.Reader/Issue5/Number Param Types
From HaskellWiki
m 
m 

Line 3:  Line 3:  
= Numberparameterized types = 
= Numberparameterized types = 

−  ''This article is also [http://pobox.com/~oleg/ftp/papers/numberparameterizedtypes.pdf available in PDF]. This Wiki page is not the master file: rather, it is the result of the {{{SXML>Wiki}}} conversion. Please comment in ["/Comments"]'' 
+  ''This article is also [http://pobox.com/~oleg/ftp/papers/numberparameterizedtypes.pdf available in PDF]. This Wiki page is not the master file: rather, it is the result of the <tt>SXML>Wiki</tt> conversion.'' 
= Abstract = 
= Abstract = 

Line 13:  Line 13:  
with a clear error message. Numberparameterized types let the 
with a clear error message. Numberparameterized types let the 

programmer capture more invariants through types and eliminate some 
programmer capture more invariants through types and eliminate some 

−  runtime checks.[[BR]] 
+  runtime checks.<br/> 
We review several encodings of the numeric 
We review several encodings of the numeric 

parameter but concentrate on the phantom type representation of a 
parameter but concentrate on the phantom type representation of a 

Line 20:  Line 20:  
messages more comprehensible. We implement arithmetic on 
messages more comprehensible. We implement arithmetic on 

decimal numberparameterized types, which lets us statically 
decimal numberparameterized types, which lets us statically 

−  typecheck operations such as array concatenation.[[BR]] 
+  typecheck operations such as array concatenation.<br/> 
Overall we demonstrate a practical 
Overall we demonstrate a practical 

dependenttypelike system that is just a Haskell library. The basics 
dependenttypelike system that is just a Haskell library. The basics 

Line 28:  Line 28:  
= Contents = 
= Contents = 

−  
−  [[TableOfContents(2)]] 

−  
−  
== Introduction == 
== Introduction == 

−  [[Anchor(sec:Introduction)]]Discussions about types parameterized by values — especially 
+  Discussions about types parameterized by values — especially 
types of arrays or finite groups parameterized by their size — 
types of arrays or finite groups parameterized by their size — 

reoccur every couple of months on functional programming languages 
reoccur every couple of months on functional programming languages 

newsgroups and mailing lists. The often expressed wish is to guarantee 
newsgroups and mailing lists. The often expressed wish is to guarantee 

that, for example, we never attempt to add two vectors of different 
that, for example, we never attempt to add two vectors of different 

−  lengths. As one poster said [#Haskelllistquote [ Haskelllistquote] ], 
+  lengths. As one [[#Haskelllistquoteposter]] said, 
−  “This {{{[}}}feature{{{]}}} would be helpful in the crypto library where I end up having 
+  “This [feature] would be helpful in the crypto library where I end up having 
to either define new length Words all the time or using lists and 
to either define new length Words all the time or using lists and 

losing the capability of ensuring I am manipulating lists of the same 
losing the capability of ensuring I am manipulating lists of the same 

Line 64:  Line 60:  
at least one). The violations of the constraints are detected at 
at least one). The violations of the constraints are detected at 

compile time. We can remove runtime tag checks in functions like 
compile time. We can remove runtime tag checks in functions like 

−  {{{vhead}}}, which are statically assured to receive a nonempty 
+  <hask>vhead</hask>, which are statically assured to receive a nonempty 
vector. 
vector. 

Line 79:  Line 75:  
number. For simplicity, all the vectors in the paper are indexed from 
number. For simplicity, all the vectors in the paper are indexed from 

zero. In addition to vector constructors and element accessors, we 
zero. In addition to vector constructors and element accessors, we 

−  define a {{{zipWith}}}like operation to map two vectors onto 
+  define a <hask>zipWith</hask>like operation to map two vectors onto 
the third, element by element. An attempt to map vectors of different 
the third, element by element. An attempt to map vectors of different 

sizes should be reported as a type error. The typechecker will also 
sizes should be reported as a type error. The typechecker will also 

guarantee that there is no attempt to allocate a vector of a negative 
guarantee that there is no attempt to allocate a vector of a negative 

−  size. In Section [#sec:arithmetic [ sec:arithmetic] ] we introduce operations {{{vhead}}}, {{{vtail}}} and {{{vappend}}} on numberparameterized vectors. 
+  size. In Section [[#Computations with decimal typessec:arithmetic]] we introduce operations <hask>vhead</hask>, <hask>vtail</hask> and <hask>vappend</hask> on numberparameterized vectors. 
The types of these operations exhibit arithmetic and inequality 
The types of these operations exhibit arithmetic and inequality 

constraints. 
constraints. 

Line 93:  Line 89:  
encoding of the size in a sequence of type constructors. The 
encoding of the size in a sequence of type constructors. The 

resulting types are phantom and impose no runtime overhead. Section 
resulting types are phantom and impose no runtime overhead. Section 

−  [#sec:unarytype [ sec:unarytype] ] describes unary encoding of numerals in type 
+  [[#Encoding the number parameter in type constructors, in unarysec:unarytype]] 
−  constructors, Sections [#sec:decimalfixed [ sec:decimalfixed] ] and 
+  describes unary encoding of numerals in type 
−  [#sec:decimalarb [ sec:decimalarb] ] discuss decimal encodings. Section 
+  constructors, Sections [[#Fixedprecision decimal typessec:decimalfixed]] and 
−  [#sec:decimalfixed [ sec:decimalfixed] ] introduces a type representation for 
+  [[#Arbitraryprecision decimal typessec:decimalarb]] discuss decimal encodings. Section 
−  fixedprecision decimal numbers. Section [#sec:decimalarb [ sec:decimalarb] ] 
+  [[#Fixedprecision decimal typessec:decimalfixed]] introduces a type representation for 
+  fixedprecision decimal numbers. Section [[#Arbitraryprecision decimal typessec:decimalarb]] 

removes the limitation on the maximal size of representable numbers, 
removes the limitation on the maximal size of representable numbers, 

at a cost of a more complex implementation and of replacing commas 
at a cost of a more complex implementation and of replacing commas 

Line 105:  Line 101:  
interesting groups. 
interesting groups. 

−  Section [#sec:arithmetic [ sec:arithmetic] ] describes the first 
+  Section [[#Computations with decimal typessec:arithmetic]] describes the first 
contribution of the paper. We develop addition and subtraction of 
contribution of the paper. We develop addition and subtraction of 

“decimal types”, i.e., of the type constructor applications 
“decimal types”, i.e., of the type constructor applications 

Line 115:  Line 111:  
numberparameterized types. 
numberparameterized types. 

−  Section [#sec:dynamic [ sec:dynamic] ] briefly describes working with 
+  Section [[#Staticallysized vectors in a dynamic contextsec:dynamic]] briefly describes working with 
numberparameterized types when the numeric parameter, and even its 
numberparameterized types when the numeric parameter, and even its 

upper bound, are not known until run time. We show one, quite simple 
upper bound, are not known until run time. We show one, quite simple 

Line 121:  Line 117:  
witnessing. The witnessing code, which must be trustworthy, is notably 
witnessing. The witnessing code, which must be trustworthy, is notably 

compact. The section uses the method of blending of static and dynamic 
compact. The section uses the method of blending of static and dynamic 

−  assurances that was first described in [#stanamictrees [ stanamictrees] ]. 
+  assurances that was first described in [[#stanamictreesstanamictrees]]. 
−  Section [#sec:related [ sec:related] ] compares our approach with the 
+  Section [[#Related worksec:related]] compares our approach with the 
phantom type programming in SML by Matthias Blume, with a practical 
phantom type programming in SML by Matthias Blume, with a practical 

dependenttype system of Hongwei Xi, with staticallysized and generic 
dependenttype system of Hongwei Xi, with staticallysized and generic 

arrays in Pascal and C, with the shape inference in arrayoriented 
arrays in Pascal and C, with the shape inference in arrayoriented 

−  languages, and with C++ template metaprogramming. Section [#sec:conclusions [ sec:conclusions] ] concludes. 
+  languages, and with C++ template metaprogramming. Section [[#Conclusionssec:conclusions]] concludes. 
== Encoding the number parameter in data constructors == 
== Encoding the number parameter in data constructors == 

−  [[Anchor(sec:Okasaki)]]The first approach to vectors parameterized by their size encodes 
+  The first approach to vectors parameterized by their size encodes 
the size as a series of data constructors. This approach has been used 
the size as a series of data constructors. This approach has been used 

−  extensively by Chris Okasaki. For example, in [#Okasaki99 [ Okasaki99] ] 
+  extensively by Chris Okasaki. For example, in [[#Okasaki99Okasaki99]] 
he describes square matrixes whose dimensions can be proved equal at 
he describes square matrixes whose dimensions can be proved equal at 

compile time. He digresses briefly to demonstrate vectors of 
compile time. He digresses briefly to demonstrate vectors of 

statically known size. A similar technique has been described by 
statically known size. A similar technique has been described by 

−  McBride [#McBride [ McBride] ]. In this section, we develop a more naive 
+  [[#McBrideMcBride]]. In this section, we develop a more naive 
encoding of the size through data constructors, for introduction and 
encoding of the size through data constructors, for introduction and 

comparison with the encoding of the size via type constructors in the 
comparison with the encoding of the size via type constructors in the 

Line 145:  Line 141:  
Our representation of vectors of a statically checked size is 
Our representation of vectors of a statically checked size is 

reminiscent of the familiar representation of lists: 
reminiscent of the familiar representation of lists: 

−  +  <haskell> 

−  
−  {{{ 

data List a = Nil  Cons a (List a) 
data List a = Nil  Cons a (List a) 

−  }}} 
+  </haskell> 
−  {{{List a}}} is a recursive datatype. Lists of different sizes 
+  <hask>List a</hask> is a recursive datatype. Lists of different sizes 
have the same recursive type. To make the types different (so that 
have the same recursive type. To make the types different (so that 

we can represent the size, too) we break the explicit recursion in the 
we can represent the size, too) we break the explicit recursion in the 

datatype declaration. We introduce two data constructors: 
datatype declaration. We introduce two data constructors: 

−  +  <haskell> 

−  
−  {{{ 

module UnaryDS where 
module UnaryDS where 

data VZero a = VZero deriving Show 
data VZero a = VZero deriving Show 

Line 158:  Line 154:  
infixr 3 :+: 
infixr 3 :+: 

data Vecp tail a = a :+: (tail a) deriving Show 
data Vecp tail a = a :+: (tail a) deriving Show 

−  }}} 
+  </haskell> 
−  The constructor {{{VZero}}} represents a vector of a zero 
+  The constructor <hask>VZero</hask> represents a vector of a zero 
−  size. A value of the type {{{Vecp tail a}}} is a nonempty vector 
+  size. A value of the type <hask>Vecp tail a</hask> is a nonempty vector 
−  formed from an element of the type {{{a}}} and (a smaller vector) 
+  formed from an element of the type <hask>a</hask> and (a smaller vector) 
−  of the type {{{tail a}}}. We place our vectors into the class 
+  of the type <hask>tail a</hask>. We place our vectors into the class 
−  {{{Show}}} for expository purposes. Thus vectors holding one 
+  <hask>Show</hask> for expository purposes. Thus vectors holding one 
−  element have the type {{{Vecp VZero a}}}, vectors with two 
+  element have the type <hask>Vecp VZero a</hask>, vectors with two 
−  elements have the type {{{Vecp (Vecp VZero) a}}}, with three elements 
+  elements have the type <hask>Vecp (Vecp VZero) a</hask>, with three elements 
−  {{{Vecp (Vecp (Vecp VZero)) a}}}, etc. We should stress the 
+  <hask>Vecp (Vecp (Vecp VZero)) a</hask>, etc. We should stress the 
−  separation of the shape type of a vector, {{{Vecp (Vecp VZero)}}} in the last example, from the type of vector elements. The shape 
+  separation of the shape type of a vector, <hask>Vecp (Vecp VZero)</hask> in the last example, from the type of vector elements. The shape 
type of a vector clearly encodes vector’s size, as repeated 
type of a vector clearly encodes vector’s size, as repeated 

−  applications of a type constructor {{{Vecp}}} to the type 
+  applications of a type constructor <hask>Vecp</hask> to the type 
−  constructor {{{VZero}}}, i.e., as a Peano numeral. We have indeed 
+  constructor <hask>VZero</hask>, i.e., as a Peano numeral. We have indeed 
designed a numberparameterized ''type''. 
designed a numberparameterized ''type''. 

To generically manipulate the family of differentlysized vectors, 
To generically manipulate the family of differentlysized vectors, 

we define a class of polymorphic functions: 
we define a class of polymorphic functions: 

−  +  <haskell> 

−  
−  {{{ 

class Vec t where 
class Vec t where 

vlength:: t a > Int 
vlength:: t a > Int 

vat:: t a > Int > a 
vat:: t a > Int > a 

vzipWith:: (a>b>c) > t a > t b > t c 
vzipWith:: (a>b>c) > t a > t b > t c 

−  }}} 
+  </haskell> 
−  The method {{{vlength}}} gives us the size of a vector; the 
+  The method <hask>vlength</hask> gives us the size of a vector; the 
−  method {{{vat}}} lets us retrieve a specific element, and the method 
+  method <hask>vat</hask> lets us retrieve a specific element, and the method 
−  {{{vzipWith}}} produces a vector by an elementbyelement 
+  <hask>vzipWith</hask> produces a vector by an elementbyelement 
−  combination of two other vectors. We can use {{{vzipWith}}} to 
+  combination of two other vectors. We can use <hask>vzipWith</hask> to 
−  add two vectors elementwise. We must emphasize the type of {{{vzipWith}}}: the two argument vectors may hold elements of different 
+  add two vectors elementwise. We must emphasize the type of <hask>vzipWith</hask>: the two argument vectors may hold elements of different 
types, but the vectors must have the same shape, i.e., size. 
types, but the vectors must have the same shape, i.e., size. 

−  The implementation of the class {{{Vec}}} has only two 
+  The implementation of the class <hask>Vec</hask> has only two 
instances: 
instances: 

−  +  <haskell> 

−  
−  {{{ 

instance Vec VZero where 
instance Vec VZero where 

vlength = const 0 
vlength = const 0 

Line 202:  Line 198:  
vzipWith f (a :+: ta) (b :+: tb) = 
vzipWith f (a :+: ta) (b :+: tb) = 

(f a b) :+: (vzipWith f ta tb) 
(f a b) :+: (vzipWith f ta tb) 

−  }}} 
+  </haskell> 
−  The second instance makes it clear that a value of a type {{{Vecp tail a}}} is a vector {{{Vec}}} if and only if 
+  The second instance makes it clear that a value of a type <hask>Vecp tail a</hask> is a vector <hask>Vec</hask> if and only if 
−  {{{tail a}}} is a vector {{{Vec}}}. Our vectors, 
+  <hask>tail a</hask> is a vector <hask>Vec</hask>. Our vectors, 
−  instances of the class {{{Vec}}}, are recursively defined too. Unlike 
+  instances of the class <hask>Vec</hask>, are recursively defined too. Unlike 
lists, our vectors reveal their sizes in their types. 
lists, our vectors reveal their sizes in their types. 

That was the complete implementation of the numberparameterized 
That was the complete implementation of the numberparameterized 

vectors. We can now define a few sample vectors: 
vectors. We can now define a few sample vectors: 

−  +  <haskell> 

−  
−  {{{ 

v3c = 'a' :+: 'b' :+: 'c' :+: VZero 
v3c = 'a' :+: 'b' :+: 'c' :+: VZero 

v3i = 1 :+: 2 :+: 3 :+: VZero 
v3i = 1 :+: 2 :+: 3 :+: VZero 

v4i = 1 :+: 2 :+: 3 :+: 4 :+: VZero 
v4i = 1 :+: 2 :+: 3 :+: 4 :+: VZero 

−  }}} 
+  </haskell> 
and a few simple tests: 
and a few simple tests: 

−  +  <haskell> 

−  
−  {{{ 

test1 = vlength v3c 
test1 = vlength v3c 

test2 = [vat v3c 0, vat v3c 1, vat v3c 2] 
test2 = [vat v3c 0, vat v3c 1, vat v3c 2] 

−  }}} 
+  </haskell> 
We can load the code into a Haskell system and run the 
We can load the code into a Haskell system and run the 

tests. Incidentally, we can ask the Haskell system to tell us the 
tests. Incidentally, we can ask the Haskell system to tell us the 

inferred type of a sample vector: 
inferred type of a sample vector: 

−  +  <haskell> 

−  
−  {{{ 

*UnaryDS> :t v3c 
*UnaryDS> :t v3c 

Vecp (Vecp (Vecp VZero)) Char 
Vecp (Vecp (Vecp VZero)) Char 

−  }}} 
+  </haskell> 
The inferred type indeed encodes the size of the vector as a 
The inferred type indeed encodes the size of the vector as a 

Peano numeral. We can try more complex tests, of elementwise 
Peano numeral. We can try more complex tests, of elementwise 

operations on two vectors: 
operations on two vectors: 

−  +  <haskell> 

−  
−  {{{ 

test3 = vzipWith (\c i > (toEnum $ fromEnum c + fromIntegral i)::Char) 
test3 = vzipWith (\c i > (toEnum $ fromEnum c + fromIntegral i)::Char) 

v3c v3i 
v3c v3i 

Line 236:  Line 232:  
*UnaryDS> test3 
*UnaryDS> test3 

'b' :+: ('d' :+: ('f' :+: VZero)) 
'b' :+: ('d' :+: ('f' :+: VZero)) 

−  }}} 
+  </haskell> 
−  In particular, {{{test3}}} demonstrates an operation on two 
+  In particular, <hask>test3</hask> demonstrates an operation on two 
vectors of the same shape but of different element types. 
vectors of the same shape but of different element types. 

An attempt to add, by mistake, two vectors of different sizes is 
An attempt to add, by mistake, two vectors of different sizes is 

revealing: 
revealing: 

−  +  <haskell> 

−  
−  {{{ 

test5 = vzipWith (+) v3i v4i 
test5 = vzipWith (+) v3i v4i 

Line 250:  Line 246:  
In the third argument of `vzipWith', namely `v4i' 
In the third argument of `vzipWith', namely `v4i' 

In the definition of `test5': vzipWith (+) v3i v4i 
In the definition of `test5': vzipWith (+) v3i v4i 

−  }}} 
+  </haskell> 
We get a type error, with a clear error message (the quoted message, 
We get a type error, with a clear error message (the quoted message, 

here and elsewhere in the paper, is by GHCi. The Hugs error message 
here and elsewhere in the paper, is by GHCi. The Hugs error message 

Line 258:  Line 254:  
For vectors described in this section, the element access 
For vectors described in this section, the element access 

−  operation, {{{vat}}}, takes {{{O(n)}}} time where 
+  operation, <hask>vat</hask>, takes <tt>O(n)</tt> time where 
−  {{{n}}} is the size of the vector. Chris Okasaki [#Okasaki99 [ Okasaki99] ] has designed more sophisticated numberparameterized 
+  <tt>n</tt> is the size of the vector. [[#Okasaki99Chris Okasaki]] has designed more sophisticated numberparameterized 
−  vectors with element access time {{{O(log n)}}}. Although this 
+  vectors with element access time <tt>O(log n)</tt>. Although this 
is an improvement, the overhead of accessing an element adds up for 
is an improvement, the overhead of accessing an element adds up for 

many operations. Furthermore, the overhead of data constructors, 
many operations. Furthermore, the overhead of data constructors, 

−  {{{:+:}}} in our example, becomes noticeable for longer 
+  <hask>:+:</hask> in our example, becomes noticeable for longer 
vectors. When we encode the size of a vector as a sequence of data 
vectors. When we encode the size of a vector as a sequence of data 

constructors, the latter overhead cannot be eliminated. 
constructors, the latter overhead cannot be eliminated. 

Line 269:  Line 265:  
Although we have achieved the separation of the shape type of a 
Although we have achieved the separation of the shape type of a 

vector from the type of its elements, we did so at the expense of a 
vector from the type of its elements, we did so at the expense of a 

−  sequence of data constructors, {{{:+:}}}, at the term 
+  sequence of data constructors, <hask>:+:</hask>, at the term 
level. These constructors add time and space overheads, which 
level. These constructors add time and space overheads, which 

increase with the vector size. In the following sections we 
increase with the vector size. In the following sections we 

Line 281:  Line 277:  
== Encoding the number parameter in type constructors, in unary == 
== Encoding the number parameter in type constructors, in unary == 

−  [[Anchor(sec:unarytype)]]To improve the efficiency of numberparameterized vectors, we 
+  To improve the efficiency of numberparameterized vectors, we 
choose a better runtime representation: Haskell arrays. The code in 
choose a better runtime representation: Haskell arrays. The code in 

the present section is in Haskell98. 
the present section is in Haskell98. 

−  +  <haskell> 

−  
−  {{{ 

module UnaryT (..elided..) where 
module UnaryT (..elided..) where 

import Data.Array 
import Data.Array 

−  }}} 
+  </haskell> 
First, we need a type structure (an infinite family of types) to 
First, we need a type structure (an infinite family of types) to 

encode nonnegative numbers. In the present section, we will use an 
encode nonnegative numbers. In the present section, we will use an 

unary encoding in the form of Peano numerals. The unary type encoding of 
unary encoding in the form of Peano numerals. The unary type encoding of 

integers belongs to programming folklore. It is also described in 
integers belongs to programming folklore. It is also described in 

−  [#Blume01 [ Blume01] ] in the context of a foreignfunction interface 
+  [[#Blume01Blume01]] in the context of a foreignfunction interface 
library of SML. 
library of SML. 

−  +  <haskell> 

−  
−  {{{ 

data Zero = Zero 
data Zero = Zero 

data Succ a = Succ a 
data Succ a = Succ a 

−  }}} 
+  </haskell> 
−  That is, the term {{{Zero}}} of the type {{{Zero}}} 
+  That is, the term <hask>Zero</hask> of the type <hask>Zero</hask> 
−  represents the number 0. The term {{{(Succ (Succ Zero))}}} of the type 
+  represents the number 0. The term <hask>(Succ (Succ Zero))</hask> of the type 
−  {{{(Succ (Succ Zero))}}} encodes the number two. We call these 
+  <hask>(Succ (Succ Zero))</hask> encodes the number two. We call these 
−  numerals Peano numerals because the number {{{n}}} is 
+  numerals Peano numerals because the number <tt>n</tt> is 
−  represented as a repeated application of {{{n}}} type (data) 
+  represented as a repeated application of <tt>n</tt> type (data) 
−  constructors {{{Succ}}} to the type (term) {{{Zero}}}. We observe a onetoone correspondence between the types of our 
+  constructors <hask>Succ</hask> to the type (term) <hask>Zero</hask>. We observe a onetoone correspondence between the types of our 
numerals and the terms. In fact, a numeral term looks precisely the 
numerals and the terms. In fact, a numeral term looks precisely the 

same as its type. This property is crucial as we shall see on many 
same as its type. This property is crucial as we shall see on many 

occasions below. It lets us “lift” number computations to the type 
occasions below. It lets us “lift” number computations to the type 

−  level. The property also makes error messages lucid. [[FootNote(We could have declared {{{Succ}}} as {{{newtype Succ a = Succ a}}} so that {{{Succ}}} is just a tag and all nonbottom Peano numerals share the same runtime representation. As we shall see however, we hardly ever use the values of our numerals.)]] 
+  level. The property also makes error messages lucid 
+  <ref>We could have declared <hask>Succ</hask> as 

+  <hask>newtype Succ a = Succ a</hask> so that <hask>Succ</hask> is just a 

+  tag and all nonbottom Peano numerals share the same runtime 

+  representation. As we shall see however, we hardly ever use the values of 

+  our numerals.</ref>. 

−  We place our Peano numerals into a class {{{Card}}}, which 
+  We place our Peano numerals into a class <hask>Card</hask>, which 
−  has a method {{{c2num}}} to convert a numeral into the 
+  has a method <hask>c2num</hask> to convert a numeral into the 
corresponding number. 
corresponding number. 

−  +  <haskell> 

−  
−  {{{ 

class Card c where 
class Card c where 

c2num:: (Num a) => c > a  convert to a number 
c2num:: (Num a) => c > a  convert to a number 

Line 323:  Line 319:  
instance (Card c) => Card (Succ c) where 
instance (Card c) => Card (Succ c) where 

c2num x = 1 + c2num (cpred x) 
c2num x = 1 + c2num (cpred x) 

−  }}} 
+  </haskell> 
−  The function {{{cpred}}} determines the predecessor for a 
+  The function <hask>cpred</hask> determines the predecessor for a 
positive Peano numeral. The definition for that function may seem 
positive Peano numeral. The definition for that function may seem 

puzzling: it is undefined. We observe that the callers do not need the value 
puzzling: it is undefined. We observe that the callers do not need the value 

returned by that function: they merely need the type of that 
returned by that function: they merely need the type of that 

−  value. Indeed, let us examine the definitions of the method {{{c2num}}} in the above two instances. In the instance {{{Card Zero}}}, we are certain that the argument of {{{c2num}}} has 
+  value. Indeed, let us examine the definitions of the method <hask>c2num</hask> in the above two instances. In the instance <hask>Card Zero</hask>, we are certain that the argument of <hask>c2num</hask> has 
−  the type {{{Zero}}}. That type, in our encoding, represents the 
+  the type <hask>Zero</hask>. That type, in our encoding, represents the 
number zero, which we return. There can be only one nonbottom value 
number zero, which we return. There can be only one nonbottom value 

−  of the type {{{Zero}}}: therefore, once we know the type, we do 
+  of the type <hask>Zero</hask>: therefore, once we know the type, we do 
not need to examine the value. Likewise, in the instance 
not need to examine the value. Likewise, in the instance 

−  {{{Card (Succ c)}}}, we know that the type of the argument of {{{c2num}}} is {{{(Succ c)}}}, where {{{c}}} is itself a 
+  <hask>Card (Succ c)</hask>, we know that the type of the argument of <hask>c2num</hask> is <hask>(Succ c)</hask>, where <hask>c</hask> is itself a 
−  {{{Card}}} numeral. If we could convert a value of the type 
+  <hask>Card</hask> numeral. If we could convert a value of the type 
−  {{{c}}} to a number, we can convert the value of the type {{{(Succ c)}}} as well. By induction we determine that {{{c2num}}} never examines the value of its argument. Indeed, not only {{{c2num (Succ (Succ Zero))}}} evaluates to 2, but so does 
+  <hask>c</hask> to a number, we can convert the value of the type <hask>(Succ c)</hask> as well. By induction we determine that <hask>c2num</hask> never examines the value of its argument. Indeed, not only <hask>c2num (Succ (Succ Zero))</hask> evaluates to 2, but so does 
−  {{{c2num (undefined::(Succ (Succ Zero)))}}}. 
+  <hask>c2num (undefined::(Succ (Succ Zero)))</hask>. 
The same correspondence between the types and the terms suggests 
The same correspondence between the types and the terms suggests 

that the numeral type alone is enough to describe the size of a 
that the numeral type alone is enough to describe the size of a 

vector. We do not need to store the value of the numeral. The shape 
vector. We do not need to store the value of the numeral. The shape 

−  type of our vectors could be ''phantom'' [#Blume01 [ Blume01] ]. 
+  type of our vectors could be ''phantom'' (as in [[#Blume01Blume01]]). 
−  +  <haskell> 

−  
−  {{{ 

newtype Vec size a = Vec (Array Int a) deriving Show 
newtype Vec size a = Vec (Array Int a) deriving Show 

−  }}} 
+  </haskell> 
−  That is, the type variable {{{size}}} does not occur on the 
+  That is, the type variable <hask>size</hask> does not occur on the 
−  righthand size of the {{{Vec}}} declaration. More importantly, 
+  righthand size of the <hask>Vec</hask> declaration. More importantly, 
−  at runtime our {{{Vec}}} is indistinguishable from an {{{Array}}}, thus incurring no additional overhead and providing 
+  at runtime our <hask>Vec</hask> is indistinguishable from an <hask>Array</hask>, thus incurring no additional overhead and providing 
constanttime element access. As we mentioned earlier, for simplicity, 
constanttime element access. As we mentioned earlier, for simplicity, 

all the vectors in the paper are indexed from zero. The data 
all the vectors in the paper are indexed from zero. The data 

−  constructor {{{Vec}}} is not exported from the module, so one 
+  constructor <hask>Vec</hask> is not exported from the module, so one 
has to use the following functions to construct vectors. 
has to use the following functions to construct vectors. 

−  +  <haskell> 

−  
−  {{{ 

listVec':: (Card size) => size > [a] > Vec size a 
listVec':: (Card size) => size > [a] > Vec size a 

listVec' size elems = Vec $ listArray (0,(c2num size)1) elems 
listVec' size elems = Vec $ listArray (0,(c2num size)1) elems 

Line 363:  Line 359:  
vec:: (Card size) => size > a > Vec size a 
vec:: (Card size) => size > a > Vec size a 

vec size elem = listVec' size $ repeat elem 
vec size elem = listVec' size $ repeat elem 

−  }}} 
+  </haskell> 
−  The private function {{{listVec{{{'}}}}}} constructs the vector 
+  The private function <hask>listVec'</hask> constructs the vector 
of the requested size initialized with the given values. The function 
of the requested size initialized with the given values. The function 

makes no check that the length of the list of the initial values 
makes no check that the length of the list of the initial values 

−  {{{elems}}} is equal to the length of the vector. We use this 
+  <hask>elems</hask> is equal to the length of the vector. We use this 
−  nonexported function internally, when we have proven that {{{elems}}} has the right length, or when truncating such a list is 
+  nonexported function internally, when we have proven that <hask>elems</hask> has the right length, or when truncating such a list is 
−  appropriate. The exported function {{{listVec}}} is a safe 
+  appropriate. The exported function <hask>listVec</hask> is a safe 
−  version of {{{listVec{{{'}}}}}}. The former assures that the 
+  version of <hask>listVec'</hask>. The former assures that the 
−  constructed vector is consistently initialized. The function {{{vec}}} initializes all elements to the same value. For example, the 
+  constructed vector is consistently initialized. The function <hask>vec</hask> initializes all elements to the same value. For example, the 
following expression creates a boolean vector of two elements with the 
following expression creates a boolean vector of two elements with the 

−  initial values {{{True}}} and {{{False}}}. 
+  initial values <hask>True</hask> and <hask>False</hask>. 
−  +  <haskell> 

−  
−  {{{ 

*UnaryT> listVec (Succ (Succ Zero)) [True,False] 
*UnaryT> listVec (Succ (Succ Zero)) [True,False] 

Vec (array (0,1) [(0,True),(1,False)]) 
Vec (array (0,1) [(0,True),(1,False)]) 

−  }}} 
+  </haskell> 
A Haskell interpreter created the requested value, and printed it 
A Haskell interpreter created the requested value, and printed it 

out. We can confirm that the inferred type of the vector encodes its 
out. We can confirm that the inferred type of the vector encodes its 

size: 
size: 

−  +  <haskell> 

−  
−  {{{ 

*UnaryT> :type listVec (Succ (Succ Zero)) [True,False] 
*UnaryT> :type listVec (Succ (Succ Zero)) [True,False] 

Vec (Succ (Succ Zero)) Bool 
Vec (Succ (Succ Zero)) Bool 

−  }}} 
+  </haskell> 
We can now introduce functions to operate on our vectors. The 
We can now introduce functions to operate on our vectors. The 

functions are similar to those in the previous section. As before, 
functions are similar to those in the previous section. As before, 

Line 390:  Line 386:  
polymorphism is expressed differently however. In the present section 
polymorphism is expressed differently however. In the present section 

we use just the parametric polymorphism rather than typeclasses. 
we use just the parametric polymorphism rather than typeclasses. 

−  +  <haskell> 

−  
−  {{{ 

vlength_t:: Vec size a > size 
vlength_t:: Vec size a > size 

vlength_t _ = undefined 
vlength_t _ = undefined 

Line 406:  Line 402:  
vzipWith f va vb = 
vzipWith f va vb = 

listVec' (vlength_t va) $ zipWith f (velems va) (velems vb) 
listVec' (vlength_t va) $ zipWith f (velems va) (velems vb) 

−  }}} 
+  </haskell> 
−  The functions {{{vlength{{{_}}}t}}} and {{{vlength}}} tell 
+  The functions <hask>vlength_t</hask> and <hask>vlength</hask> tell 
−  the size of their argument vector. The function {{{vat}}} 
+  the size of their argument vector. The function <hask>vat</hask> 
returns the element of a vector at a given zerobased index. The function 
returns the element of a vector at a given zerobased index. The function 

−  {{{velems}}}, which gives the list of vector’s elements, is the 
+  <hask>velems</hask>, which gives the list of vector’s elements, is the 
−  left inverse of {{{listVec}}}. The function 
+  left inverse of <hask>listVec</hask>. The function 
−  {{{vzipWith}}} elementwise combines two vectors into the third 
+  <hask>vzipWith</hask> elementwise combines two vectors into the third 
−  one by applying a userspecified function {{{f}}} to the 
+  one by applying a userspecified function <hask>f</hask> to the 
corresponding elements of the argument vectors. The polymorphic types 
corresponding elements of the argument vectors. The polymorphic types 

of these functions indicate that the functions generically operate on 
of these functions indicate that the functions generically operate on 

−  numberparameterized vectors of any {{{size}}}. Furthermore, 
+  numberparameterized vectors of any <hask>size</hask>. Furthermore, 
−  the type of {{{vzipWith}}} expresses the constraint that the 
+  the type of <hask>vzipWith</hask> expresses the constraint that the 
two argument vectors must have the same size. The result will be a 
two argument vectors must have the same size. The result will be a 

vector of the same size as that of the argument vectors. We rely on 
vector of the same size as that of the argument vectors. We rely on 

−  the fact that the function {{{zipWith}}}, when applied to two 
+  the fact that the function <hask>zipWith</hask>, when applied to two 
lists of the same size, gives the list of that size. This justifies our 
lists of the same size, gives the list of that size. This justifies our 

−  use of {{{listVec{{{'}}}}}}. 
+  use of <hask>listVec'</hask>. 
We have introduced two functions that yield the size of their 
We have introduced two functions that yield the size of their 

−  argument vector. One is the function {{{vlength{{{_}}}t}}}: it 
+  argument vector. One is the function <hask>vlength_t</hask>: it 
returns a value whose type represents the size of the vector. We are 
returns a value whose type represents the size of the vector. We are 

interested only in the type of the return value — which we extract 
interested only in the type of the return value — which we extract 

−  statically from the type of the argument vector. The function {{{vlength{{{_}}}t}}} is a ''compiletime'' function. Therefore, it is 
+  statically from the type of the argument vector. The function <hask>vlength_t</hask> is a ''compiletime'' function. Therefore, it is 
−  no surprise that its body is {{{undefined}}}. The type of the 
+  no surprise that its body is <hask>undefined</hask>. The type of the 
−  function ''is'' its true definition. The function {{{vlength}}} in contrast retrieves vector’s size from the runtime 
+  function ''is'' its true definition. The function <hask>vlength</hask> in contrast retrieves vector’s size from the runtime 
−  representation as an array. If we export {{{listVec}}} from the 
+  representation as an array. If we export <hask>listVec</hask> from the 
−  module {{{UnaryT}}} but do not export the constructor {{{Vec}}}, we can guarantee that {{{c2num . vlength{{{_}}}t}}} is 
+  module <hask>UnaryT</hask> but do not export the constructor <hask>Vec</hask>, we can guarantee that <hask>c2num . vlength_t</hask> is 
−  equivalent to {{{vlength}}}: our numberparameterized vector 
+  equivalent to <hask>vlength</hask>: our numberparameterized vector 
type is sound. 
type is sound. 

From the practical point of view, passing terms such as 
From the practical point of view, passing terms such as 

−  {{{(Succ (Succ Zero))}}} to the functions {{{vec}}} or {{{listVec}}} to construct vectors is inconvenient. The previous 
+  <hask>(Succ (Succ Zero))</hask> to the functions <hask>vec</hask> or <hask>listVec</hask> to construct vectors is inconvenient. The previous 
section showed a better approach. We can implement it here too: we let 
section showed a better approach. We can implement it here too: we let 

the user enumerate the values, which we accumulate into a list, 
the user enumerate the values, which we accumulate into a list, 

counting them at the same time: 
counting them at the same time: 

−  +  <haskell> 

−  
−  {{{ 

infixl 3 &+ 
infixl 3 &+ 

data VC size a = VC size [a] 
data VC size a = VC size [a] 

Line 450:  Line 446:  
vc:: (Card size) => VC size a > Vec size a 
vc:: (Card size) => VC size a > Vec size a 

vc (VC size lst) = listVec' size (reverse lst) 
vc (VC size lst) = listVec' size (reverse lst) 

−  }}} 
+  </haskell> 
The counting operation is effectively performed by a typechecker 
The counting operation is effectively performed by a typechecker 

−  at compile time. Finally, the function {{{vc}}} will allocate 
+  at compile time. Finally, the function <hask>vc</hask> will allocate 
and initialize the vector of the right size — and of the right 
and initialize the vector of the right size — and of the right 

type. Here are a few sample vectors and operations on them: 
type. Here are a few sample vectors and operations on them: 

−  +  <haskell> 

−  
−  {{{ 

v3c = vc $ vs &+ 'a' &+ 'b' &+ 'c' 
v3c = vc $ vs &+ 'a' &+ 'b' &+ 'c' 

v3i = vc $ vs &+ 1 &+ 2 &+ 3 
v3i = vc $ vs &+ 1 &+ 2 &+ 3 

Line 465:  Line 461:  
v3c v3i 
v3c v3i 

test4 = vzipWith (+) v3i v3i 
test4 = vzipWith (+) v3i v3i 

−  }}} 
+  </haskell> 
We can run the tests as follows: 
We can run the tests as follows: 

−  +  <haskell> 

−  
−  {{{ 

*UnaryT> test3 
*UnaryT> test3 

Vec (array (0,2) [(0,'b'),(1,'d'),(2,'f')]) 
Vec (array (0,2) [(0,'b'),(1,'d'),(2,'f')]) 

*UnaryT> :type test3 
*UnaryT> :type test3 

Vec (Succ (Succ (Succ Zero))) Char 
Vec (Succ (Succ (Succ Zero))) Char 

−  }}} 
+  </haskell> 
The type of the result bears the clear indication of the size of 
The type of the result bears the clear indication of the size of 

the vector. If we attempt to perform an elementwise operation on 
the vector. If we attempt to perform an elementwise operation on 

vectors of different sizes, for example: 
vectors of different sizes, for example: 

−  +  <haskell> 

−  
−  {{{ 

test5 = vzipWith (+) v3i v4i 
test5 = vzipWith (+) v3i v4i 

Couldn't match `Zero' against `Succ Zero' 
Couldn't match `Zero' against `Succ Zero' 

Line 483:  Line 479:  
In the third argument of `vzipWith', namely `v4i' 
In the third argument of `vzipWith', namely `v4i' 

In the definition of `test5': vzipWith (+) v3i v4i 
In the definition of `test5': vzipWith (+) v3i v4i 

−  }}} 
+  </haskell> 
we get a message from the typechecker that the sizes are off 
we get a message from the typechecker that the sizes are off 

by one. 
by one. 

Line 490:  Line 486:  
== Fixedprecision decimal types == 
== Fixedprecision decimal types == 

−  [[Anchor(sec:decimalfixed)]]Peano numerals adequately represent the size of a vector in vector’s 
+  Peano numerals adequately represent the size of a vector in vector’s 
type. However, they make the notation quite verbose. We want to offer 
type. However, they make the notation quite verbose. We want to offer 

a programmer a familiar, decimal notation for the terms and the types 
a programmer a familiar, decimal notation for the terms and the types 

Line 504:  Line 500:  
is the use of decimal rather than unary types to describe the sizes of 
is the use of decimal rather than unary types to describe the sizes of 

our vectors. 
our vectors. 

−  +  <haskell> 

−  
−  {{{ 

module FixedDecT (..export list elided..) where 
module FixedDecT (..export list elided..) where 

import Data.Array 
import Data.Array 

−  }}} 
+  </haskell> 
Since we will be using the decimal notation, we need the terms and 
Since we will be using the decimal notation, we need the terms and 

the types for all ten digits: 
the types for all ten digits: 

−  +  <haskell> 

−  
−  {{{ 

data D0 = D0 
data D0 = D0 

data D1 = D1 
data D1 = D1 

... 
... 

data D9 = D9 
data D9 = D9 

−  }}} 
+  </haskell> 
For clarity and to save space, we elide repetitive code 
For clarity and to save space, we elide repetitive code 

−  fragments. The full code is available from [#CodeForPaper [ CodeForPaper] ]. To manipulate the digits uniformly (e.g., to find out the 
+  fragments. The [[#CodeForPaperfull code]] is available. To manipulate the digits uniformly (e.g., to find out the 
−  corresponding integer), we put them into a class {{{Digit}}}. We also introduce a class for nonzero digits. The latter has no 
+  corresponding integer), we put them into a class <hask>Digit</hask>. We also introduce a class for nonzero digits. The latter has no 
−  methods: we use {{{NonZeroDigit}}} as a constraint on allowable 
+  methods: we use <hask>NonZeroDigit</hask> as a constraint on allowable 
digits. 
digits. 

−  +  <haskell> 

−  
−  {{{ 

class Digit d where  class of digits 
class Digit d where  class of digits 

d2num:: (Num a) => d > a  convert to a number 
d2num:: (Num a) => d > a  convert to a number 

Line 535:  Line 531:  
... 
... 

instance NonZeroDigit D9 
instance NonZeroDigit D9 

−  }}} 
+  </haskell> 
We define a class of nonnegative numerals. We make all 
We define a class of nonnegative numerals. We make all 

singledigit numerals the members of that class: 
singledigit numerals the members of that class: 

−  +  <haskell> 

−  
−  {{{ 

class Card c where 
class Card c where 

c2num:: (Num a) => c > a  convert to a number 
c2num:: (Num a) => c > a  convert to a number 

Line 547:  Line 543:  
... 
... 

instance Card D9 where c2num _ = 9 
instance Card D9 where c2num _ = 9 

−  }}} 
+  </haskell> 
−  We define a twodigit number, a tuple {{{(d1,d2)}}} 
+  We define a twodigit number, a tuple <hask>(d1,d2)</hask> 
−  where {{{d1}}} is a nonzero digit, a member of the class {{{Card}}}. The class {{{NonZeroDigit}}} makes expressing 
+  where <hask>d1</hask> is a nonzero digit, a member of the class <hask>Card</hask>. The class <hask>NonZeroDigit</hask> makes expressing 
the constraint lucid. We also introduce threedigit decimal 
the constraint lucid. We also introduce threedigit decimal 

−  numerals {{{(d1,d2,d3)}}}: 
+  numerals <hask>(d1,d2,d3)</hask>: 
−  +  <haskell> 

−  
−  {{{ 

instance (NonZeroDigit d1,Digit d2) => Card (d1,d2) where 
instance (NonZeroDigit d1,Digit d2) => Card (d1,d2) where 

c2num c = 10*(d2num $ t12 c) + (d2num $ t22 c) 
c2num c = 10*(d2num $ t12 c) + (d2num $ t22 c) 

Line 560:  Line 556:  
c2num c = 100*(d2num $ t13 c) + 10*(d2num $ t23 c) 
c2num c = 100*(d2num $ t13 c) + 10*(d2num $ t23 c) 

+ (d2num $ t33 c) 
+ (d2num $ t33 c) 

−  }}} 
+  </haskell> 
−  The instance constraints of the {{{Card}}} instances 
+  The instance constraints of the <hask>Card</hask> instances 
guarantee the uniqueness of our representation of numbers: the 
guarantee the uniqueness of our representation of numbers: the 

major decimal digit of a multidigit number is not zero. It will be a 
major decimal digit of a multidigit number is not zero. It will be a 

type error to attempt to form such an number: 
type error to attempt to form such an number: 

−  +  <haskell> 

−  
−  {{{ 

*FixedDecT> vec (D0,D1) 'a' 
*FixedDecT> vec (D0,D1) 'a' 

<interactive>:1: 
<interactive>:1: 

No instance for (NonZeroDigit D0) 
No instance for (NonZeroDigit D0) 

−  }}} 
+  </haskell> 
−  The auxiliary compiletime functions {{{t12}}}...{{{t33}}} are tuple selectors. We could have avoided them in GHC with 
+  The auxiliary compiletime functions <hask>t12</hask>...<hask>t33</hask> are tuple selectors. We could have avoided them in GHC with 
Glasgow extensions, which supports local type variables. We feel 
Glasgow extensions, which supports local type variables. We feel 

however that keeping the code Haskell98 justifies the extra hassle: 
however that keeping the code Haskell98 justifies the extra hassle: 

−  +  <haskell> 

−  
−  {{{ 

t12::(a,b) > a; t12 = undefined 
t12::(a,b) > a; t12 = undefined 

t22::(a,b) > b; t22 = undefined 
t22::(a,b) > b; t22 = undefined 

... 
... 

t33::(a,b,c) > c; t33 = undefined 
t33::(a,b,c) > c; t33 = undefined 

−  }}} 
+  </haskell> 
The rest of the code is as before, e.g.: 
The rest of the code is as before, e.g.: 

−  +  <haskell> 

−  
−  {{{ 

newtype Vec size a = Vec (Array Int a) deriving Show 
newtype Vec size a = Vec (Array Int a) deriving Show 

listVec':: Card size => size > [a] > Vec size a 
listVec':: Card size => size > [a] > Vec size a 

listVec' size elems = Vec $ listArray (0,(c2num size)1) elems 
listVec' size elems = Vec $ listArray (0,(c2num size)1) elems 

−  }}} 
+  </haskell> 
−  The implementations of the polymorphic functions {{{listVec}}}, {{{vec}}}, {{{vlength{{{_}}}t}}}, {{{vlength}}}, {{{vat}}}, 
+  The implementations of the polymorphic functions <hask>listVec</hask>, <hask>vec</hask>, <hask>vlength_t</hask>, <hask>vlength</hask>, <hask>vat</hask>, 
−  {{{velems}}}, and {{{vzipWith}}} are precisely the same 
+  <hask>velems</hask>, and <hask>vzipWith</hask> are precisely the same 
−  as those in Section [#sec:unarytype [ sec:unarytype] ]. We elide the code for 
+  as those in Section [[#Encoding the number parameter in type constructors, in unarysec:unarytype]]. We elide the code for 
the sake of space. We introduce a few sample vectors, using the 
the sake of space. We introduce a few sample vectors, using the 

decimal notation this time: 
decimal notation this time: 

−  +  <haskell> 

−  
−  {{{ 

v12c = listVec (D1,D2) $ take 12 ['a'..'z'] 
v12c = listVec (D1,D2) $ take 12 ['a'..'z'] 

v12i = listVec (D1,D2) [1..12] 
v12i = listVec (D1,D2) [1..12] 

v13i = listVec (D1,D3) [1..13] 
v13i = listVec (D1,D3) [1..13] 

−  }}} 
+  </haskell> 
The decimal notation is so much convenient. We can now define long 
The decimal notation is so much convenient. We can now define long 

vectors without pain. As before, the type of our vectors — the size 
vectors without pain. As before, the type of our vectors — the size 

part of the type — looks precisely the same as the corresponding 
part of the type — looks precisely the same as the corresponding 

size term expression: 
size term expression: 

−  +  <haskell> 

−  
−  {{{ 

*FixedDecT> :type v12c 
*FixedDecT> :type v12c 

Vec (D1, D2) Char 
Vec (D1, D2) Char 

−  }}} 
+  </haskell> 
−  We can use the sample vectors in the tests like those of the 
+  We can use the [[#CodeForPapersample vectors]] in the tests like those of the 
−  previous section, [#CodeForPaper [ CodeForPaper] ]. If we attempt to 
+  previous section. If we attempt to 
elementwise add two vectors of different sizes, we get a type 
elementwise add two vectors of different sizes, we get a type 

error: 
error: 

−  +  <haskell> 

−  
−  {{{ 

test5 = vzipWith (+) v12i v13i 
test5 = vzipWith (+) v12i v13i 

Line 616:  Line 612:  
In the third argument of `vzipWith', namely `v13i' 
In the third argument of `vzipWith', namely `v13i' 

In the definition of `test5': vzipWith (+) v12i v13i 
In the definition of `test5': vzipWith (+) v12i v13i 

−  }}} 
+  </haskell> 
The error message literally says that 12 is not equal to 13: the 
The error message literally says that 12 is not equal to 13: the 

typechecker expected a vector of size 12 but found a vector of size 13 
typechecker expected a vector of size 12 but found a vector of size 13 

Line 624:  Line 620:  
== Arbitraryprecision decimal types == 
== Arbitraryprecision decimal types == 

−  [[Anchor(sec:decimalarb)]]From the practical point of view, the fixedprecision 
+  From the practical point of view, the fixedprecision 
numberparameterized vectors of the previous section are 
numberparameterized vectors of the previous section are 

sufficient. The imposition of a limit on the width of the decimal 
sufficient. The imposition of a limit on the width of the decimal 

Line 630:  Line 626:  
unsatisfying. One may wish for an encoding of arbitrarily large decimal 
unsatisfying. One may wish for an encoding of arbitrarily large decimal 

numbers within a framework that has been set up once and for all. Such 
numbers within a framework that has been set up once and for all. Such 

−  an SML framework has been introduced in [#Blume01 [ Blume01] ], to 
+  an SML framework has been introduced in [[#Blume01Blume01]], to 
encode the sizes of arrays in their types. It is interesting to ask 
encode the sizes of arrays in their types. It is interesting to ask 

if such an encoding is possible in Haskell. The present section 
if such an encoding is possible in Haskell. The present section 

Line 641:  Line 637:  
We start by defining the types for the ten digits: 
We start by defining the types for the ten digits: 

−  +  <haskell> 

−  
−  {{{ 

module ArbPrecDecT (..export list elided..) where 
module ArbPrecDecT (..export list elided..) where 

import Data.Array 
import Data.Array 

Line 649:  Line 645:  
... 
... 

data D9 a = D9 a 
data D9 a = D9 a 

−  }}} 
+  </haskell> 
−  Unlike the code in the previous section, {{{D0}}} through {{{D9}}} are type constructors of one argument. We 
+  Unlike the code in the previous section, <hask>D0</hask> through <hask>D9</hask> are type constructors of one argument. We 
use the composition of the constructors to represent sequences of 
use the composition of the constructors to represent sequences of 

digits. And so we introduce a class for arbitrary sequences of 
digits. And so we introduce a class for arbitrary sequences of 

digits: 
digits: 

−  +  <haskell> 

−  
−  {{{ 

class Digits ds where 
class Digits ds where 

ds2num:: (Num a) => ds > a > a 
ds2num:: (Num a) => ds > a > a 

−  }}} 
+  </haskell> 
with a method to convert a sequence to the corresponding 
with a method to convert a sequence to the corresponding 

−  number. The method {{{ds2num}}} is designed in the 
+  number. The method <hask>ds2num</hask> is designed in the 
accumulatorpassing style: its second argument is the accumulator. We 
accumulatorpassing style: its second argument is the accumulator. We 

−  also need a type, which we call {{{Sz}}}, to represent an empty 
+  also need a type, which we call <hask>Sz</hask>, to represent an empty 
sequence of digits: 
sequence of digits: 

−  +  <haskell> 

−  
−  {{{ 

data Sz = Sz  zero size (or the Nil of the sequence) 
data Sz = Sz  zero size (or the Nil of the sequence) 

instance Digits Sz where 
instance Digits Sz where 

ds2num _ acc = acc 
ds2num _ acc = acc 

−  }}} 
+  </haskell> 
We now inductively define arbitrarily long sequences of digits: 
We now inductively define arbitrarily long sequences of digits: 

−  +  <haskell> 

−  
−  {{{ 

instance (Digits ds) => Digits (D0 ds) where 
instance (Digits ds) => Digits (D0 ds) where 

ds2num dds acc = ds2num (t22 dds) (10*acc) 
ds2num dds acc = ds2num (t22 dds) (10*acc) 

Line 679:  Line 675:  
t22::(f x) > x; t22 = undefined 
t22::(f x) > x; t22 = undefined 

−  }}} 
+  </haskell> 
−  The type and the term {{{Sz}}} is an empty sequence; 
+  The type and the term <hask>Sz</hask> is an empty sequence; 
−  {{{D9 Sz}}} — that is, the application of the constructor {{{D9}}} to {{{Sz}}} — is a sequence of one digit, digit 9. The 
+  <hask>D9 Sz</hask> — that is, the application of the constructor <hask>D9</hask> to <hask>Sz</hask> — is a sequence of one digit, digit 9. The 
−  application of the constructor {{{D1}}} to the latter sequence 
+  application of the constructor <hask>D1</hask> to the latter sequence 
−  gives us {{{D1 (D9 Sz)}}}, a twodigit sequence of digits one 
+  gives us <hask>D1 (D9 Sz)</hask>, a twodigit sequence of digits one 
and nine. Compositions of data/type constructors indeed encode 
and nine. Compositions of data/type constructors indeed encode 

sequences of digits. As before, the terms and the types look precisely 
sequences of digits. As before, the terms and the types look precisely 

the same. The compositions can of course be arbitrarily long: 
the same. The compositions can of course be arbitrarily long: 

−  +  <haskell> 

−  
−  {{{ 

*ArbPrecDecT> :type D1$ D2$ D3$ D4$ D5$ D6$ D7$ D8$ D9$ D0$ D9$ 
*ArbPrecDecT> :type D1$ D2$ D3$ D4$ D5$ D6$ D7$ D8$ D9$ D0$ D9$ 

D8$ D7$ D6$ D5$ D4$ D3$ D2$ D1$ Sz 
D8$ D7$ D6$ D5$ D4$ D3$ D2$ D1$ Sz 

Line 695:  Line 691:  
D8$ D7$ D6$ D5$ D4$ D3$ D2$ D1$ Sz) 0 
D8$ D7$ D6$ D5$ D4$ D3$ D2$ D1$ Sz) 0 

1234567890987654321 
1234567890987654321 

−  }}} 
+  </haskell> 
We should point out a notable advantage of Haskell typeclasses in 
We should point out a notable advantage of Haskell typeclasses in 

designing of sophisticated type families — in particular, in 
designing of sophisticated type families — in particular, in 

specifying constraints. Nothing prevents a programmer from using our 
specifying constraints. Nothing prevents a programmer from using our 

−  type constructors, e.g., {{{D1}}}, in unintended ways. For 
+  type constructors, e.g., <hask>D1</hask>, in unintended ways. For 
−  example, a programmer may form a value of the type {{{D1 Bool}}}: either by applying a data constructor {{{D1}}} to a boolean 
+  example, a programmer may form a value of the type <hask>D1 Bool</hask>: either by applying a data constructor <hask>D1</hask> to a boolean 
−  value, or by casting a polymorphic value, {{{undefined}}}, 
+  value, or by casting a polymorphic value, <hask>undefined</hask>, 
into that type: 
into that type: 

−  +  <haskell> 

−  
−  {{{ 

*ArbPrecDecT> :type D1 True 
*ArbPrecDecT> :type D1 True 

D1 Bool 
D1 Bool 

*ArbPrecDecT> :type (undefined::D1 Bool) 
*ArbPrecDecT> :type (undefined::D1 Bool) 

D1 Bool 
D1 Bool 

−  }}} 
+  </haskell> 
However, such types do ''not'' represent decimal 
However, such types do ''not'' represent decimal 

sequences. Indeed, an attempt to pass either of these values to 
sequences. Indeed, an attempt to pass either of these values to 

−  {{{ds2num}}} will result in a type error: 
+  <hask>ds2num</hask> will result in a type error: 
−  +  <haskell> 

−  
−  {{{ 

*ArbPrecDecT> ds2num (undefined::D1 Bool) 0 
*ArbPrecDecT> ds2num (undefined::D1 Bool) 0 

No instance for (Digits Bool) 
No instance for (Digits Bool) 

arising from use of `ds2num' at <interactive>:1 
arising from use of `ds2num' at <interactive>:1 

In the definition of `it': ds2num (undefined :: D1 Bool) 0 
In the definition of `it': ds2num (undefined :: D1 Bool) 0 

−  }}} 
+  </haskell> 
−  In contrast, the approach in [#Blume01 [ Blume01] ] prevented the 
+  In contrast, the approach in [[#Blume01Blume01]] prevented the 
user from constructing (nonbottom) values of these types by a careful 
user from constructing (nonbottom) values of these types by a careful 

design and export of value constructors. That approach relied on SML’s 
design and export of value constructors. That approach relied on SML’s 

Line 728:  Line 724:  
which relies on phantom types, unsound. Fortunately, we are able to 
which relies on phantom types, unsound. Fortunately, we are able to 

eliminate illformed decimal types at the type level rather than at 
eliminate illformed decimal types at the type level rather than at 

−  the term level. Our class {{{Digits}}} admits those and ''only'' those types that represent sequences of digits. 
+  the term level. Our class <hask>Digits</hask> admits those and ''only'' those types that represent sequences of digits. 
To guarantee the bijection between nonnegative numbers and 
To guarantee the bijection between nonnegative numbers and 

Line 735:  Line 731:  
nonzero. Expressing such a restriction is surprisingly 
nonzero. Expressing such a restriction is surprisingly 

straightforward in Haskell, even Haskell98. 
straightforward in Haskell, even Haskell98. 

−  +  <haskell> 

−  
−  {{{ 

class (Digits c) => Card c where 
class (Digits c) => Card c where 

c2num:: (Num a) => c > a 
c2num:: (Num a) => c > a 

Line 745:  Line 741:  
... 
... 

instance (Digits ds) => Card (D9 ds) 
instance (Digits ds) => Card (D9 ds) 

−  }}} 
+  </haskell> 
−  As in the previous sections, the class {{{Card}}} 
+  As in the previous sections, the class <hask>Card</hask> 
represents nonnegative integers. A nonnegative integer is realized 
represents nonnegative integers. A nonnegative integer is realized 

here as a sequence of decimal digits — provided, as the instances 
here as a sequence of decimal digits — provided, as the instances 

specify, that the sequence starts with a digit other than zero. We can 
specify, that the sequence starts with a digit other than zero. We can 

now define the type of our numberparameterized vectors: 
now define the type of our numberparameterized vectors: 

−  +  <haskell> 

−  
−  {{{ 

newtype Vec size a = Vec (Array Int a) deriving Show 
newtype Vec size a = Vec (Array Int a) deriving Show 

−  }}} 
+  </haskell> 
−  which looks precisely as before, and polymorphic functions {{{vec}}}, {{{listVec}}}, {{{vlength{{{_}}}t}}}, {{{vlength}}}, {{{velems}}}, {{{vat}}}, and {{{vzipWith}}} — which are identical to those in Section [#sec:unarytype [ sec:unarytype] ]. We can define a few sample vectors: 
+  which looks precisely as before, and polymorphic functions <hask>vec</hask>, <hask>listVec</hask>, <hask>vlength_t</hask>, <hask>vlength</hask>, <hask>velems</hask>, <hask>vat</hask>, and <hask>vzipWith</hask> — which are identical to those in Section [[#Encoding the number parameter in type constructors, in unarysec:unarytype]]. We can define a few sample vectors: 
−  +  <haskell> 

−  
−  {{{ 

v12c = listVec (D1 $ D2 Sz) $ take 12 ['a'..'z'] 
v12c = listVec (D1 $ D2 Sz) $ take 12 ['a'..'z'] 

v12i = listVec (D1 $ D2 Sz) [1..12] 
v12i = listVec (D1 $ D2 Sz) [1..12] 

v13i = listVec (D1 $ D3 Sz) [1..13] 
v13i = listVec (D1 $ D3 Sz) [1..13] 

−  }}} 
+  </haskell> 
we should note a slight change of notation compared to the 
we should note a slight change of notation compared to the 

−  corresponding vectors of Section [#sec:decimalfixed [ sec:decimalfixed] ]. The 
+  corresponding vectors of Section [[#Fixedprecision decimal typessec:decimalfixed]]. The 
tests are not changed and continue to work as before: 
tests are not changed and continue to work as before: 

−  +  <haskell> 

−  
−  {{{ 

test4 = vzipWith (+) v12i v12i 
test4 = vzipWith (+) v12i v12i 

Line 770:  Line 766:  
*ArbPrecDecT> test4 
*ArbPrecDecT> test4 

Vec (array (0,11) [(0,2),(1,4),(2,6),...(11,24)]) 
Vec (array (0,11) [(0,2),(1,4),(2,6),...(11,24)]) 

−  }}} 
+  </haskell> 
The compiler has been able to infer the size of the result of the 
The compiler has been able to infer the size of the result of the 

−  {{{vzipWith}}} operation. The size is lucidly spelled in 
+  <hask>vzipWith</hask> operation. The size is lucidly spelled in 
decimal in the type of the vector. Again, an attempt to elementwise 
decimal in the type of the vector. Again, an attempt to elementwise 

add vectors of different sizes leads to a type error: 
add vectors of different sizes leads to a type error: 

−  +  <haskell> 

−  
−  {{{ 

test5 = vzipWith (+) v12i v13i 
test5 = vzipWith (+) v12i v13i 

Couldn't match `D2 Sz' against `D3 Sz' 
Couldn't match `D2 Sz' against `D3 Sz' 

Line 782:  Line 778:  
In the third argument of `vzipWith', namely `v13i' 
In the third argument of `vzipWith', namely `v13i' 

In the definition of `test5': vzipWith (+) v12i v13i 
In the definition of `test5': vzipWith (+) v12i v13i 

−  }}} 
+  </haskell> 
The typechecker complains that 2 is not equal to 3: it found the 
The typechecker complains that 2 is not equal to 3: it found the 

vector of size 13 whereas it expected a vector of size 12. The decimal 
vector of size 13 whereas it expected a vector of size 12. The decimal 

Line 788:  Line 784:  
We must again point out a significant difference of our approach 
We must again point out a significant difference of our approach 

−  from that of [#Blume01 [ Blume01] ]. We were able to state that only 
+  from that of [[#Blume01Blume01]]. We were able to state that only 
those types of digital sequences that start with a nonzero digit 
those types of digital sequences that start with a nonzero digit 

−  correspond to a nonnegative number. SML, as acknowledged in [#Blume01 [ Blume01] ], is unable to express such a restriction directly. The 
+  correspond to a nonnegative number. SML, as acknowledged in [[#Blume01Blume01]], is unable to express such a restriction directly. The 
−  paper [#Blume01 [ Blume01] ], therefore, prevents the user from building 
+  [[#Blume01paper]], therefore, prevents the user from building 
invalid decimal sequences by relying on the module system: by 
invalid decimal sequences by relying on the module system: by 

exporting carefullydesigned value constructors. The latter use an 
exporting carefullydesigned value constructors. The latter use an 

auxiliary phantom type to keep track of “nonzeroness” of the major 
auxiliary phantom type to keep track of “nonzeroness” of the major 

digit. Our approach does not incur such a complication. Furthermore, 
digit. Our approach does not incur such a complication. Furthermore, 

−  by the very inductive construction of the classes {{{Digits}}} 
+  by the very inductive construction of the classes <hask>Digits</hask> 
−  and {{{Card}}}, there is a onetoone correspondence between 
+  and <hask>Card</hask>, there is a onetoone correspondence between 
−  ''types'', the members of {{{Card}}}, and the integers 
+  ''types'', the members of <hask>Card</hask>, and the integers 
−  in decimal notation. In [#Blume01 [ Blume01] ], the similar mapping 
+  in decimal notation. In [[#Blume01Blume01]], the similar mapping 
holds only when the family of decimal types is restricted to the types 
holds only when the family of decimal types is restricted to the types 

that correspond to constructible values. A user of that system may 
that correspond to constructible values. A user of that system may 

still form bottom values of invalid decimal types, which will cause 
still form bottom values of invalid decimal types, which will cause 

runtime errors. In our case, when the digit constructors are 
runtime errors. In our case, when the digit constructors are 

−  misapplied, the result will no longer be in the class {{{Card}}}, and so the error will be detected ''statically'' by the 
+  misapplied, the result will no longer be in the class <hask>Card</hask>, and so the error will be detected ''statically'' by the 
typechecker: 
typechecker: 

−  +  <haskell> 

−  
−  {{{ 

*ArbPrecDecT> vec (D1$ D0$ D0$ True) 0 
*ArbPrecDecT> vec (D1$ D0$ D0$ True) 0 

No instance for (Digits Bool) 
No instance for (Digits Bool) 

Line 816:  Line 812:  
arising from use of `vec' at <interactive>:1 
arising from use of `vec' at <interactive>:1 

In the definition of `it': vec (D0 $ (D1 $ (D0 Sz))) 0 
In the definition of `it': vec (D0 $ (D1 $ (D0 Sz))) 0 

−  }}} 
+  </haskell> 
== Computations with decimal types == 
== Computations with decimal types == 

−  [[Anchor(sec:arithmetic)]]The previous sections gave many examples of functions such as 
+  The previous sections gave many examples of functions such as 
−  {{{vzipWith}}} that take two vectors ''statically'' 
+  <hask>vzipWith</hask> that take two vectors ''statically'' 
known to be of equal size. The signature of these functions states 
known to be of equal size. The signature of these functions states 

quite detailed invariants whose violations will be reported at 
quite detailed invariants whose violations will be reported at 

compiletime. Furthermore, the invariants can be inferred by the 
compiletime. Furthermore, the invariants can be inferred by the 

compiler itself. This use of the type system is not particular to 
compiler itself. This use of the type system is not particular to 

−  Haskell: Matthias Blume [#Blume01 [ Blume01] ] has derived a similar 
+  Haskell: [[#Blume01Matthias Blume]] has derived a similar 
parameterization of arrays in SML, which can express such equality of 
parameterization of arrays in SML, which can express such equality of 

size constraints. Matthias Blume however cautions one not to overstate 
size constraints. Matthias Blume however cautions one not to overstate 

Line 838:  Line 834:  
statically and sometimes even inferred by a compiler. In this section, 
statically and sometimes even inferred by a compiler. In this section, 

we consider the example of vector concatenation. We shall see that the 
we consider the example of vector concatenation. We shall see that the 

−  inferred type of {{{vappend}}} manifestly affirms that the size 
+  inferred type of <hask>vappend</hask> manifestly affirms that the size 
of the result is the sum of the sizes of two argument vectors. We also 
of the result is the sum of the sizes of two argument vectors. We also 

−  introduce the functions {{{vhead}}} and {{{vtail}}}, 
+  introduce the functions <hask>vhead</hask> and <hask>vtail</hask>, 
whose type specifies that they can only be applied to nonempty 
whose type specifies that they can only be applied to nonempty 

−  vectors. Furthermore, the type of {{{vtail}}} says that the 
+  vectors. Furthermore, the type of <hask>vtail</hask> says that the 
size of the result vector is less by one than the size of the argument 
size of the result vector is less by one than the size of the argument 

vector. These examples are quite unusual and almost cross into the 
vector. These examples are quite unusual and almost cross into the 

Line 849:  Line 845:  
We must note however that the examples in this section require the 
We must note however that the examples in this section require the 

Haskell98 extension to multiparameter classes with functional 
Haskell98 extension to multiparameter classes with functional 

−  dependencies. That extension is activated by flags {{{98}}} of 
+  dependencies. That extension is activated by flags <hask>98</hask> of 
−  Hugs and {{{fglasgowexts fallowundecidableinstances}}} of 
+  Hugs and <hask>fglasgowexts fallowundecidableinstances</hask> of 
GHCi. 
GHCi. 

Line 860:  Line 856:  
such numbers starting from the leastsignificant digit. Therefore, we 
such numbers starting from the leastsignificant digit. Therefore, we 

need a way to reverse digital sequences, or more precise, types of the 
need a way to reverse digital sequences, or more precise, types of the 

−  class {{{Digits}}}. We use the conventional sequence reversal 
+  class <hask>Digits</hask>. We use the conventional sequence reversal 
algorithm written in the accumulatorpassing style. 
algorithm written in the accumulatorpassing style. 

−  +  <haskell> 

−  
−  {{{ 

class DigitsInReverse' df w dr  df w > dr 
class DigitsInReverse' df w dr  df w > dr 

Line 868:  Line 864:  
instance (Digits (d drest), DigitsInReverse' drest (d acc) dr) 
instance (Digits (d drest), DigitsInReverse' drest (d acc) dr) 

=> DigitsInReverse' (d drest) acc dr 
=> DigitsInReverse' (d drest) acc dr 

−  }}} 
+  </haskell> 
−  We introduced the class {{{DigitsInReverse{{{'}}} df w dr}}} where 
+  We introduced the class <hask>DigitsInReverse' df w dr</hask> where 
−  {{{df}}} is the source sequence, {{{dr}}} is the 
+  <hask>df</hask> is the source sequence, <hask>dr</hask> is the 
−  reversed sequence, and {{{w}}} is the accumulator. The three 
+  reversed sequence, and <hask>w</hask> is the accumulator. The three 
−  digit sequence types belong to {{{DigitsInReverse{{{'}}}}}} if 
+  digit sequence types belong to <hask>DigitsInReverse'</hask> if 
−  the reverse of {{{df}}} appended to {{{w}}} gives the 
+  the reverse of <hask>df</hask> appended to <hask>w</hask> gives the 
−  digit sequence {{{dr}}}. The functional dependency and the two 
+  digit sequence <hask>dr</hask>. The functional dependency and the two 
instances spell this constraint out. We can now introduce a class that 
instances spell this constraint out. We can now introduce a class that 

relates a sequence of digits with its reverse: 
relates a sequence of digits with its reverse: 

−  +  <haskell> 

−  
−  {{{ 

class DigitsInReverse df dr  df > dr, dr > df 
class DigitsInReverse df dr  df > dr, dr > df 

instance (DigitsInReverse' df Sz dr, DigitsInReverse' dr Sz df) 
instance (DigitsInReverse' df Sz dr, DigitsInReverse' dr Sz df) 

=> DigitsInReverse df dr 
=> DigitsInReverse df dr 

−  }}} 
+  </haskell> 
−  Two sequences of digits {{{df}}} and {{{dr}}} belong 
+  Two sequences of digits <hask>df</hask> and <hask>dr</hask> belong 
−  to the class {{{DigitsInReverse}}} if they are the reverse of 
+  to the class <hask>DigitsInReverse</hask> if they are the reverse of 
each other. The functional dependencies make the “each other” part 
each other. The functional dependencies make the “each other” part 

clear: one sequence uniquely determines the other. The typechecker 
clear: one sequence uniquely determines the other. The typechecker 

−  will verify that given {{{df}}}, it can find {{{dr}}} so 
+  will verify that given <hask>df</hask>, it can find <hask>dr</hask> so 
−  that both {{{DigitsInReverse{{{'}}} df Sz dr}}} and {{{DigitsInReverse{{{'}}} dr Sz df}}} are satisfied. To test the reversal 
+  that both <hask>DigitsInReverse' df Sz dr</hask> and <hask>DigitsInReverse' dr Sz df</hask> are satisfied. To test the reversal 
−  process, we define a function {{{digits{{{_}}}rev}}}: 
+  process, we define a function <hask>digits_rev</hask>: 
−  +  <haskell> 

−  
−  {{{ 

digits_rev:: (Digits ds, Digits dsr, DigitsInReverse ds dsr) 
digits_rev:: (Digits ds, Digits dsr, DigitsInReverse ds dsr) 

=> ds > dsr 
=> ds > dsr 

digits_rev = undefined 
digits_rev = undefined 

−  }}} 
+  </haskell> 
It is again a compiletime function specified entirely by its 
It is again a compiletime function specified entirely by its 

type. Its body is therefore undefined. We can now run a few 
type. Its body is therefore undefined. We can now run a few 

examples: 
examples: 

−  +  <haskell> 

−  
−  {{{ 

*ArbArithmT> :t digits_rev (D1$D2$D3 Sz) 
*ArbArithmT> :t digits_rev (D1$D2$D3 Sz) 

D3 (D2 (D1 Sz)) 
D3 (D2 (D1 Sz)) 

*ArbArithmT> :t (\v > digits_rev v `asTypeOf` (D1$D2$D3 Sz)) 
*ArbArithmT> :t (\v > digits_rev v `asTypeOf` (D1$D2$D3 Sz)) 

D3 (D2 (D1 Sz)) > D1 (D2 (D3 Sz)) 
D3 (D2 (D1 Sz)) > D1 (D2 (D3 Sz)) 

−  }}} 
+  </haskell> 
Indeed, the process of reversing sequences of decimal digits works 
Indeed, the process of reversing sequences of decimal digits works 

−  both ways. Given the type of the argument to {{{digits{{{_}}}rev}}}, 
+  both ways. Given the type of the argument to <hask>digits_rev</hask>, 
the compiler infers the type of the result. Conversely, given the type 
the compiler infers the type of the result. Conversely, given the type 

of the result the compiler infers the type of the argument. 
of the result the compiler infers the type of the argument. 

−  A sequence of digits belongs to the class {{{Card}}} only 
+  A sequence of digits belongs to the class <hask>Card</hask> only 
if the mostsignificant digit is not a zero. To convert an arbitrary 
if the mostsignificant digit is not a zero. To convert an arbitrary 

−  sequence to {{{Card}}} we need a way to strip leading zeros: 
+  sequence to <hask>Card</hask> we need a way to strip leading zeros: 
−  +  <haskell> 

−  
−  {{{ 

class NoLeadingZeros d d0  d > d0 
class NoLeadingZeros d d0  d > d0 

instance NoLeadingZeros Sz Sz 
instance NoLeadingZeros Sz Sz 

Line 919:  Line 915:  
... 
... 

instance NoLeadingZeros (D9 d) (D9 d) 
instance NoLeadingZeros (D9 d) (D9 d) 

−  }}} 
+  </haskell> 
We are now ready to build the addition machinery. We draw our 
We are now ready to build the addition machinery. We draw our 

inspiration from the computer architecture: the adder of an 
inspiration from the computer architecture: the adder of an 

Line 927:  Line 923:  
our case, the summands and the result are decimal rather than 
our case, the summands and the result are decimal rather than 

binary. Carry is still binary. 
binary. Carry is still binary. 

−  +  <haskell> 

−  
−  {{{ 

class FullAdder d1 d2 cin dr cout 
class FullAdder d1 d2 cin dr cout 

 d1 d2 cin > cout, d1 d2 cin > dr, 
 d1 d2 cin > cout, d1 d2 cin > dr, 

Line 934:  Line 930:  
_unused:: (d1 xd1) > (d2 xd2) > cin > (dr xdr) 
_unused:: (d1 xd1) > (d2 xd2) > cin > (dr xdr) 

_unused = undefined 
_unused = undefined 

−  }}} 
+  </haskell> 
−  The class {{{FullAdder}}} establishes a relation among 
+  The class <hask>FullAdder</hask> establishes a relation among 
−  three digits {{{d1}}}, {{{d2}}}, and {{{dr}}} and 
+  three digits <hask>d1</hask>, <hask>d2</hask>, and <hask>dr</hask> and 
−  two carry bits {{{cin}}} and {{{cout}}}: {{{d1 + d2 + cin = dr + 10*cout}}}. The digits are represented by the type 
+  two carry bits <hask>cin</hask> and <hask>cout</hask>: <hask>d1 + d2 + cin = dr + 10*cout</hask>. The digits are represented by the type 
−  constructors {{{D0}}} through {{{D9}}}. The sole purpose 
+  constructors <hask>D0</hask> through <hask>D9</hask>. The sole purpose 
−  of the method {{{{{{_}}}unused}}} is to cue the compiler that 
+  of the method <hask>_unused</hask> is to cue the compiler that 
−  {{{d1}}}, {{{d2}}}, and {{{dr}}} are type 
+  <hask>d1</hask>, <hask>d2</hask>, and <hask>dr</hask> are type 
constructors. The functional dependencies of the class tell us that 
constructors. The functional dependencies of the class tell us that 

the summands and the input carry uniquely determine the result digit 
the summands and the input carry uniquely determine the result digit 

and the output carry. On the other hand, if we know the result digit, 
and the output carry. On the other hand, if we know the result digit, 

−  one of the summands, {{{d1}}}, and the input carry, we can 
+  one of the summands, <hask>d1</hask>, and the input carry, we can 
−  determine the other summand. The same relation {{{FullAdder}}} 
+  determine the other summand. The same relation <hask>FullAdder</hask> 
can therefore be used for addition and for subtraction. In the latter 
can therefore be used for addition and for subtraction. In the latter 

case, the carry bits should be more properly called borrow bits. 
case, the carry bits should be more properly called borrow bits. 

−  +  <haskell> 

−  
−  {{{ 

data Carry0 
data Carry0 

data Carry1 
data Carry1 

Line 959:  Line 955:  
instance FullAdder D9 D9 Carry0 D8 Carry1 
instance FullAdder D9 D9 Carry0 D8 Carry1 

instance FullAdder D9 D9 Carry1 D9 Carry1 
instance FullAdder D9 D9 Carry1 D9 Carry1 

−  }}} 
+  </haskell> 
−  The full code [#CodeForPaper [ CodeForPaper] ] indeed contains 200 instances of 
+  The [[#CodeForPaperfull code]] indeed contains 200 instances of 
−  {{{FullAdder}}}. The exhaustive enumeration verifies the 
+  <hask>FullAdder</hask>. The exhaustive enumeration verifies the 
functional dependencies of the class. The number of instances could be 
functional dependencies of the class. The number of instances could be 

significantly reduced if we availed ourselves to an overlapping 
significantly reduced if we availed ourselves to an overlapping 

Line 969:  Line 965:  
into a module and separately compile it. Furthermore, we did not write 
into a module and separately compile it. Furthermore, we did not write 

those instances by hand: we used Haskell itself: 
those instances by hand: we used Haskell itself: 

−  +  <haskell> 

−  
−  {{{ 

make_full_adder 
make_full_adder 

= mapM_ putStrLn 
= mapM_ putStrLn 

Line 983:  Line 979:  
tod n  (n >= 0 && 9 >= n) = "D" ++ (show n) 
tod n  (n >= 0 && 9 >= n) = "D" ++ (show n) 

toc 0 = "Carry0"; toc 1 = "Carry1" 
toc 0 = "Carry0"; toc 1 = "Carry1" 

−  }}} 
+  </haskell> 
That function is ready for Template Haskell. Currently we used a 
That function is ready for Template Haskell. Currently we used a 

lowtech approach of cutting and pasting from an Emacs buffer with 
lowtech approach of cutting and pasting from an Emacs buffer with 

GHCi into the Emacs buffer with the code. 
GHCi into the Emacs buffer with the code. 

−  We use {{{FullAdder}}} to build the full adder of two 
+  We use <hask>FullAdder</hask> to build the full adder of two 
−  littleendian decimal sequences {{{ds1}}} and {{{ds2}}}. 
+  littleendian decimal sequences <hask>ds1</hask> and <hask>ds2</hask>. 
−  The relation {{{DigitsSum ds1 ds2 cin dsr}}} holds if {{{ds1+ds2+cin = dsr}}}. We add the digits from the least significant 
+  The relation <hask>DigitsSum ds1 ds2 cin dsr</hask> holds if <hask>ds1+ds2+cin = dsr</hask>. We add the digits from the least significant 
onwards, and we propagate the carry. If one input sequence turns out 
onwards, and we propagate the carry. If one input sequence turns out 

shorter than the other, we pad it with zeros. The correctness of the 
shorter than the other, we pad it with zeros. The correctness of the 

algorithm follows by simple induction. 
algorithm follows by simple induction. 

−  +  <haskell> 

−  
−  {{{ 

class DigitsSum ds1 ds2 cin dsr  ds1 ds2 cin > dsr 
class DigitsSum ds1 ds2 cin dsr  ds1 ds2 cin > dsr 

instance DigitsSum Sz Sz Carry0 Sz 
instance DigitsSum Sz Sz Carry0 Sz 

Line 1,005:  Line 1,001:  
DigitsSum d1rest d2rest cout d12rest) => 
DigitsSum d1rest d2rest cout d12rest) => 

DigitsSum (d1 d1rest) (d2 d2rest) cin (d12 d12rest) 
DigitsSum (d1 d1rest) (d2 d2rest) cin (d12 d12rest) 

−  }}} 
+  </haskell> 
−  We also need the inverse relation: {{{DigitsDif ds1 ds2 cin dsr}}} holds on precisely the same condition as {{{DigitsSum}}}. Now, however, the sequences {{{ds1}}}, {{{dsr}}} and 
+  We also need the inverse relation: <hask>DigitsDif ds1 ds2 cin dsr</hask> holds on precisely the same condition as <hask>DigitsSum</hask>. Now, however, the sequences <hask>ds1</hask>, <hask>dsr</hask> and 
−  the input carry {{{cin}}} determine one of the summands, 
+  the input carry <hask>cin</hask> determine one of the summands, 
−  {{{ds2}}}. The input carry actually means the input borrow 
+  <hask>ds2</hask>. The input carry actually means the input borrow 
−  bit. The relation {{{DigitsDif}}} is defined only if the output 
+  bit. The relation <hask>DigitsDif</hask> is defined only if the output 
−  sequence {{{dsr}}} has at least as many digits as {{{ds1}}} — which is the necessary condition for the result of the 
+  sequence <hask>dsr</hask> has at least as many digits as <hask>ds1</hask> — which is the necessary condition for the result of the 
subtraction to be nonnegative. 
subtraction to be nonnegative. 

−  +  <haskell> 

−  
−  {{{ 

class DigitsDif ds1 ds2 cin dsr  ds1 dsr cin > ds2 
class DigitsDif ds1 ds2 cin dsr  ds1 dsr cin > ds2 

instance DigitsDif Sz ds Carry0 ds 
instance DigitsDif Sz ds Carry0 ds 

Line 1,020:  Line 1,016:  
DigitsDif d1rest d2rest cout d12rest) => 
DigitsDif d1rest d2rest cout d12rest) => 

DigitsDif (d1 d1rest) (d2 d2rest) cin (d12 d12rest) 
DigitsDif (d1 d1rest) (d2 d2rest) cin (d12 d12rest) 

−  }}} 
+  </haskell> 
−  The class {{{CardSum}}} with a single instance puts it all 
+  The class <hask>CardSum</hask> with a single instance puts it all 
together: 
together: 

−  +  <haskell> 

−  
−  {{{ 

class (Card c1, Card c2, Card c12) => 
class (Card c1, Card c2, Card c12) => 

CardSum c1 c2 c12  c1 c2 > c12, c1 c12 > c2 
CardSum c1 c2 c12  c1 c2 > c12, c1 c12 > c2 

Line 1,034:  Line 1,030:  
DigitsInReverse c12r c12) 
DigitsInReverse c12r c12) 

=> CardSum c1 c2 c12 
=> CardSum c1 c2 c12 

−  }}} 
+  </haskell> 
−  The class establishes the relation between three {{{Card}}} 
+  The class establishes the relation between three <hask>Card</hask> 
−  sequences {{{c1}}}, {{{c2}}}, and {{{c12}}} such 
+  sequences <hask>c1</hask>, <hask>c2</hask>, and <hask>c12</hask> such 
that the latter is the sum of the formers. The two summands determine 
that the latter is the sum of the formers. The two summands determine 

the sum, or the sum and one summand determine the other. The class can 
the sum, or the sum and one summand determine the other. The class can 

be used for addition and subtraction of sequences. The dependencies of 
be used for addition and subtraction of sequences. The dependencies of 

−  the sole {{{CardSum}}} instance spell out the algorithm. We 
+  the sole <hask>CardSum</hask> instance spell out the algorithm. We 
reverse the summand sequences to make them littleendian, add them 
reverse the summand sequences to make them littleendian, add them 

together with the zero carry, and reverse the result. We also make 
together with the zero carry, and reverse the result. We also make 

sure that the subtraction and summation are the exact inverses. The 
sure that the subtraction and summation are the exact inverses. The 

−  addition algorithm {{{DigitsSum}}} never produces a sequence 
+  addition algorithm <hask>DigitsSum</hask> never produces a sequence 
with the major digit zero. The subtraction algorithm however may 
with the major digit zero. The subtraction algorithm however may 

result in a sequence with zero major digits, which have to be stripped 
result in a sequence with zero major digits, which have to be stripped 

−  away, with the help of the relation {{{NoLeadingZeros}}}. We 
+  away, with the help of the relation <hask>NoLeadingZeros</hask>. We 
−  introduce a compiletime function {{{card{{{_}}}sum}}} so we can try 
+  introduce a compiletime function <hask>card_sum</hask> so we can try 
the addition out: 
the addition out: 

−  +  <haskell> 

−  
−  {{{ 

card_sum:: CardSum c1 c2 c12 => c1 > c2 > c12 
card_sum:: CardSum c1 c2 c12 => c1 > c2 > c12 

card_sum = undefined 
card_sum = undefined 

−  }}} 
+  </haskell> 
−  +  <haskell> 

−  {{{ 

*ArbArithmT> :t card_sum (D1 Sz) (D9$D9 Sz) 
*ArbArithmT> :t card_sum (D1 Sz) (D9$D9 Sz) 

D1 (D0 (D0 Sz)) 
D1 (D0 (D0 Sz)) 

Line 1,061:  Line 1,057:  
*ArbArithmT> :t \v > card_sum (D9$D9 Sz) v `asTypeOf` (D1$D0$D0 Sz) 
*ArbArithmT> :t \v > card_sum (D9$D9 Sz) v `asTypeOf` (D1$D0$D0 Sz) 

D1 Sz > D1 (D0 (D0 Sz)) 
D1 Sz > D1 (D0 (D0 Sz)) 

−  }}} 
+  </haskell> 
The typechecker can indeed add and subtract with carry and 
The typechecker can indeed add and subtract with carry and 

−  borrow. Now we define the function {{{vappend}}} to 
+  borrow. Now we define the function <hask>vappend</hask> to 
concatenate two vectors. 
concatenate two vectors. 

−  +  <haskell> 

−  
−  {{{ 

vappend va vb = listVec (card_sum (vlength_t va) (vlength_t vb)) 
vappend va vb = listVec (card_sum (vlength_t va) (vlength_t vb)) 

$ (velems va) ++ (velems vb) 
$ (velems va) ++ (velems vb) 

−  }}} 
+  </haskell> 
−  We could have used the function {{{listVec{{{'}}}}}}; for illustration, 
+  We could have used the function <hask>listVec'</hask>; for illustration, 
we chose however to perform a runtime check and avoid proving the theorem 
we chose however to perform a runtime check and avoid proving the theorem 

about the size of the list concatenation result. We did not declare 
about the size of the list concatenation result. We did not declare 

−  the type of {{{vappend}}}; still the compiler is able to infer it: 
+  the type of <hask>vappend</hask>; still the compiler is able to infer it: 
−  +  <haskell> 

−  
−  {{{ 

*ArbArithmT> :t vappend 
*ArbArithmT> :t vappend 

vappend :: (CardSum size size1 c12) => 
vappend :: (CardSum size size1 c12) => 

Vec size a > Vec size1 a > Vec c12 a 
Vec size a > Vec size1 a > Vec c12 a 

−  }}} 
+  </haskell> 
which literally says that the size of the result vector is the sum 
which literally says that the size of the result vector is the sum 

of the sizes of the argument vectors. The constraint is spelled out 
of the sizes of the argument vectors. The constraint is spelled out 

−  patently, as part of the type of {{{vappend}}}. The sizes may 
+  patently, as part of the type of <hask>vappend</hask>. The sizes may 
be arbitrarily large decimal numbers: for example, the following 
be arbitrarily large decimal numbers: for example, the following 

expression demonstrates the concatenation of a vector of 25 elements 
expression demonstrates the concatenation of a vector of 25 elements 

and a vector of size 979: 
and a vector of size 979: 

−  +  <haskell> 

−  
−  {{{ 

*ArbArithmT> :t vappend (vec (D2$D5 Sz) 0) (vec (D9$D7$D9 Sz) 0) 
*ArbArithmT> :t vappend (vec (D2$D5 Sz) 0) (vec (D9$D7$D9 Sz) 0) 

(Num a) => Vec (D1 (D0 (D0 (D4 Sz)))) a 
(Num a) => Vec (D1 (D0 (D0 (D4 Sz)))) a 

−  }}} 
+  </haskell> 
−  We introduce the deconstructor functions {{{vhead}}} and 
+  We introduce the deconstructor functions <hask>vhead</hask> and 
−  {{{vtail}}}. The type of the latter is exactly what was listed in 
+  <hask>vtail</hask>. The type of the latter is exactly what was listed in 
−  [#Blume01 [ Blume01] ] as an unattainable wish. 
+  [[#Blume01Blume01]] as an unattainable wish. 
−  +  <haskell> 

−  
−  {{{ 

vhead:: CardSum (D1 Sz) size1 size => Vec size a > Vec (D1 Sz) a 
vhead:: CardSum (D1 Sz) size1 size => Vec size a > Vec (D1 Sz) a 

vhead va = listVec (D1 Sz) $ [head (velems va)] 
vhead va = listVec (D1 Sz) $ [head (velems va)] 

Line 1,097:  Line 1,093:  
vtail va = result 
vtail va = result 

where result = listVec (vlength_t result) $ tail (velems va) 
where result = listVec (vlength_t result) $ tail (velems va) 

−  }}} 
+  </haskell> 
−  Although the body of {{{vtail}}} seem to refer to that 
+  Although the body of <hask>vtail</hask> seem to refer to that 
function result, the function is not divergent and not 
function result, the function is not divergent and not 

−  recursive. Recall that {{{vlength{{{_}}}t}}} is a compiletime, 
+  recursive. Recall that <hask>vlength_t</hask> is a compiletime, 
−  ‘type’ function. Therefore the body of {{{vtail}}} refers to 
+  ‘type’ function. Therefore the body of <hask>vtail</hask> refers to 
−  the statically known type of {{{result}}} rather than to its 
+  the statically known type of <hask>result</hask> rather than to its 
−  value. The type of {{{vhead}}} is also noteworthy: it 
+  value. The type of <hask>vhead</hask> is also noteworthy: it 
essentially specifies an ''inequality'' constraint: the input 
essentially specifies an ''inequality'' constraint: the input 

vector is nonempty. The constraint is expressed via an implicitly 
vector is nonempty. The constraint is expressed via an implicitly 

−  existentially quantified variable {{{size1}}}: the type of 
+  existentially quantified variable <hask>size1</hask>: the type of 
−  {{{vhead}}} says that there must exist a nonnegative number 
+  <hask>vhead</hask> says that there must exist a nonnegative number 
−  {{{size1}}} such that incrementing it by one should give the 
+  <hask>size1</hask> such that incrementing it by one should give the 
size of the input vector. 
size of the input vector. 

Line 1,114:  Line 1,110:  
correctly infer the type of the result, which includes the size of the 
correctly infer the type of the result, which includes the size of the 

vector after appending or truncating it. 
vector after appending or truncating it. 

−  +  <haskell> 

−  
−  {{{ 

*ArbArithmT> let v = vappend (vec (D9 Sz) 0) (vec (D1 Sz) 1) 
*ArbArithmT> let v = vappend (vec (D9 Sz) 0) (vec (D1 Sz) 1) 

*ArbArithmT> :t v 
*ArbArithmT> :t v 

Line 1,128:  Line 1,124:  
*ArbArithmT> :type (vappend (vhead v) (vtail v)) 
*ArbArithmT> :type (vappend (vhead v) (vtail v)) 

Vec (D1 (D0 Sz)) Integer 
Vec (D1 (D0 Sz)) Integer 

−  }}} 
+  </haskell> 
−  The types of {{{vhead}}} and {{{vtail}}} embed a 
+  The types of <hask>vhead</hask> and <hask>vtail</hask> embed a 
nonempty argument vector constraint. Indeed, an attempt to apply 
nonempty argument vector constraint. Indeed, an attempt to apply 

−  {{{vhead}}} to an empty vector results in a type error: 
+  <hask>vhead</hask> to an empty vector results in a type error: 
−  +  <haskell> 

−  
−  {{{ 

*ArbArithmT> vtail (vec Sz 0) 
*ArbArithmT> vtail (vec Sz 0) 

<interactive>:1:0: 
<interactive>:1:0: 

Line 1,142:  Line 1,138:  
DigitsInReverse' size1 Sz c2r) 
DigitsInReverse' size1 Sz c2r) 

arising from use of `vtail' at <interactive>:1:04 
arising from use of `vtail' at <interactive>:1:04 

−  }}} 
+  </haskell> 
The error message essentially says that there is no such decimal 
The error message essentially says that there is no such decimal 

−  type {{{c2r}}} such that {{{DigitsSum (D1 Sz) c2r Carry0 Sz}}} 
+  type <hask>c2r</hask> such that <hask>DigitsSum (D1 Sz) c2r Carry0 Sz</hask> 
holds. That is, there is no nonnegative number that gives zero if 
holds. That is, there is no nonnegative number that gives zero if 

added to one. 
added to one. 

−  We can form quite complex expressions from the functions {{{vappend}}}, {{{vhead}}}, and {{{vtail}}}, and the 
+  We can form quite complex expressions from the functions <hask>vappend</hask>, <hask>vhead</hask>, and <hask>vtail</hask>, and the 
compiler will ''infer'' and verify the corresponding 
compiler will ''infer'' and verify the corresponding 

constraints on the sizes of involved vectors. For example: 
constraints on the sizes of involved vectors. For example: 

−  +  <haskell> 

−  
−  {{{ 

testc1 = 
testc1 = 

let va = vec (D1$D2 Sz) 0 
let va = vec (D1$D2 Sz) 0 

Line 1,159:  Line 1,155:  
*ArbArithmT> testc1 
*ArbArithmT> testc1 

Vec (array (0,11) [(0,1),...,(4,1),(5,2),(6,2),...,(11,2)]) 
Vec (array (0,11) [(0,1),...,(4,1),(5,2),(6,2),...,(11,2)]) 

−  }}} 
+  </haskell> 
−  The size of the vector {{{va}}} must be the sum of the 
+  The size of the vector <hask>va</hask> must be the sum of the 
−  sizes of {{{vb}}} and {{{vc}}} minus one. Furthermore, 
+  sizes of <hask>vb</hask> and <hask>vc</hask> minus one. Furthermore, 
−  the vector {{{vc}}} must be nonempty. The compiler has 
+  the vector <hask>vc</hask> must be nonempty. The compiler has 
inferred this nontrivial constraint and checked it. Indeed, if we by 
inferred this nontrivial constraint and checked it. Indeed, if we by 

−  mistake write {{{vc = vec (D9 Sz) 2}}}, as we actually did when 
+  mistake write <hask>vc = vec (D9 Sz) 2</hask>, as we actually did when 
writing the example, the compiler will instantly report a type 
writing the example, the compiler will instantly report a type 

error: 
error: 

−  +  <haskell> 

−  
−  {{{ 

Couldn't match `D9 Sz' against `D8 Sz' 
Couldn't match `D9 Sz' against `D8 Sz' 

Expected type: D9 Sz 
Expected type: D9 Sz 

Line 1,176:  Line 1,172:  
DigitsSum (D1 Sz) c2r Carry0 (D8 Sz), 
DigitsSum (D1 Sz) c2r Carry0 (D8 Sz), 

arising from use of `vtail' at ArbArithmT.hs:411:3438 
arising from use of `vtail' at ArbArithmT.hs:411:3438 

−  }}} 
+  </haskell> 
−  The result {{{12  5 + 1}}} is expected to be 8 rather than 9. 
+  The result <hask>12  5 + 1</hask> is expected to be 8 rather than 9. 
We can define other operations that extend or shrink our 
We can define other operations that extend or shrink our 

−  vectors. For example, Section [#sec:unarytype [ sec:unarytype] ] introduced 
+  vectors. For example, Section [[#Encoding the number parameter in type constructors, in unarysec:unarytype]] introduced 
−  the operator {{{&+}}} to make the entering of vectors 
+  the operator <hask>&+</hask> to make the entering of vectors 
easier. It is straightforward to implement such an operator for 
easier. It is straightforward to implement such an operator for 

decimallytyped vectors. 
decimallytyped vectors. 

−  We must point out that the type system guarantees that {{{vhead}}} and {{{vtail}}} are applied to nonempty 
+  We must point out that the type system guarantees that <hask>vhead</hask> and <hask>vtail</hask> are applied to nonempty 
vectors. Therefore, we no longer need the corresponding runtime 
vectors. Therefore, we no longer need the corresponding runtime 

−  check. The bodies of {{{vhead}}} and {{{vtail}}} may 
+  check. The bodies of <hask>vhead</hask> and <hask>vtail</hask> may 
−  ''safely'' use unsafe versions of the library functions {{{head}}} and {{{tail}}}, and hence increase the performance 
+  ''safely'' use unsafe versions of the library functions <hask>head</hask> and <hask>tail</hask>, and hence increase the performance 
of the code without compromising its safety. 
of the code without compromising its safety. 

Line 1,194:  Line 1,190:  
== Staticallysized vectors in a dynamic context == 
== Staticallysized vectors in a dynamic context == 

−  [[Anchor(sec:dynamic)]]In the present version of the paper, we demonstrate the simplest 
+  In the present version of the paper, we demonstrate the simplest 
method of handling numberparameterized vectors in the dynamic 
method of handling numberparameterized vectors in the dynamic 

context. The method involves runtime checks. The successful result of 
context. The method involves runtime checks. The successful result of 

Line 1,213:  Line 1,209:  
vector processing code does not have such a degree of variation in 
vector processing code does not have such a degree of variation in 

vector sizes. The code is quite simple: 
vector sizes. The code is quite simple: 

−  +  <haskell> 

−  
−  {{{ 

vreverse v = listVec (vlength_t v) $ reverse $ velems v 
vreverse v = listVec (vlength_t v) $ reverse $ velems v 

−  }}} 
+  </haskell> 
whose inferred type is obviously 
whose inferred type is obviously 

−  +  <haskell> 

−  
−  {{{ 

*ArbArithmT> :t vreverse 
*ArbArithmT> :t vreverse 

vreverse :: (Card size) => Vec size a > Vec size a 
vreverse :: (Card size) => Vec size a > Vec size a 

−  }}} 
+  </haskell> 
−  The use of {{{listVec}}} implies a dynamic test — as a 
+  The use of <hask>listVec</hask> implies a dynamic test — as a 
−  witness to ‘acquire’ the static type {{{size}}}, the size type 
+  witness to ‘acquire’ the static type <hask>size</hask>, the size type 
of the input vector. We do this test only once, at the conclusion of 
of the input vector. We do this test only once, at the conclusion of 

the algorithm. We can treat the result as any other numberparameterized 
the algorithm. We can treat the result as any other numberparameterized 

vector, for example: 
vector, for example: 

−  +  <haskell> 

−  
−  {{{ 

testv = let v = vappend (vec (D3 Sz) 1) (vec (D1 Sz) 4) 
testv = let v = vappend (vec (D3 Sz) 1) (vec (D1 Sz) 4) 

vr = vreverse v 
vr = vreverse v 

in vhead (vtail (vtail vr)) 
in vhead (vtail (vtail vr)) 

−  }}} 
+  </haskell> 
−  using the versions of {{{vhead}}} and {{{vtail}}} 
+  using the versions of <hask>vhead</hask> and <hask>vtail</hask> 
without any further runtime size checks. 
without any further runtime size checks. 

Line 1,237:  Line 1,233:  
== Related work == 
== Related work == 

−  [[Anchor(sec:related)]]This paper was inspired by Matthias Blume’s messages on the 
+  This paper was inspired by Matthias Blume’s messages on the 
newsgroup comp.lang.functional in February 2002. Many ideas 
newsgroup comp.lang.functional in February 2002. Many ideas 

of this paper were first developed during the USENET discussion, and 
of this paper were first developed during the USENET discussion, and 

posted in a series of three messages at that time. In more detail 
posted in a series of three messages at that time. In more detail 

−  Matthias Blume described his method in [#Blume01 [ Blume01] ], 
+  Matthias Blume described his method in [[#Blume01Blume01]], 
although that paper uses binary rather than decimal types of array 
although that paper uses binary rather than decimal types of array 

sizes for clarity. The approaches by Matthias Blume and ours both rely on 
sizes for clarity. The approaches by Matthias Blume and ours both rely on 

phantom types to encode additional information about a value (e.g., 
phantom types to encode additional information about a value (e.g., 

the size of an array) in a manner suitable for a typechecker. The 
the size of an array) in a manner suitable for a typechecker. The 

−  paper [#Blume01 [ Blume01] ] exhibits the most pervasive and thorough 
+  [[#Blume01paper]] exhibits the most pervasive and thorough 
use of phantom types: to represent the size of arrays and the 
use of phantom types: to represent the size of arrays and the 

constness of imported C values, to encode C structure tag ''names'' and C function prototypes. 
constness of imported C values, to encode C structure tag ''names'' and C function prototypes. 

−  However, the paper [#Blume01 [ Blume01] ] was written in the context 
+  However, [[#Blume01paper]] was written in the context 
of SML, whereas we use Haskell. The language has greatly influenced 
of SML, whereas we use Haskell. The language has greatly influenced 

the method of specifying and enforcing complex static constraints, 
the method of specifying and enforcing complex static constraints, 

e.g., that digit sequences representing nonnegative numbers must 
e.g., that digit sequences representing nonnegative numbers must 

−  not have leading zeros. The SML approach in [#Blume01 [ Blume01] ] 
+  not have leading zeros. The SML approach in [[#Blume01Blume01]] 
relies on the sophisticated module system of SML to restrict the 
relies on the sophisticated module system of SML to restrict the 

availability of value constructors so that users cannot build 
availability of value constructors so that users cannot build 

values of outlawed types. Haskell typeclasses on the other hand can 
values of outlawed types. Haskell typeclasses on the other hand can 

directly express the constraint, as we saw in Section 
directly express the constraint, as we saw in Section 

−  [#sec:decimalarb [ sec:decimalarb] ]. Furthermore, Haskell typeclasses let us 
+  [[#Arbitraryprecision decimal typessec:decimalarb]]. Furthermore, Haskell typeclasses let us 
specify arithmetic equality and inequality constraints — which, as 
specify arithmetic equality and inequality constraints — which, as 

−  admitted in [#Blume01 [ Blume01] ], seems quite unlikely to be possible 
+  admitted in [[#Blume01Blume01]], seems quite unlikely to be possible 
in SML. 
in SML. 

Arrays of a statically known size — whose size is a part of their 
Arrays of a statically known size — whose size is a part of their 

type — are a fairly popular feature in programming languages. Such 
type — are a fairly popular feature in programming languages. Such 

−  arrays are present in Fortran, Pascal, C [[FootNote(C does permit truly staticallysized arrays like those in Pascal. To achieve this, we should make a C array a member of a C structure. The compiler preserves the array size information when passing such a wrapped array as an argument. It is even possible to assign such ``arrays''.)]] . Pascal has the most complete realization of statically sized 
+  arrays are present in Fortran, Pascal, C 
+  <ref>C does permit truly staticallysized arrays like those in Pascal. 

+  To achieve this, we should make a C array a member of a C structure. 

+  The compiler preserves the array size information when passing such a 

+  wrapped array as an argument. It is even possible to assign such “arrays”.</ref>. 

+  Pascal has the most complete realization of statically sized 

arrays. A Pascal compiler can therefore typecheck array functions like 
arrays. A Pascal compiler can therefore typecheck array functions like 

−  our {{{vzipWith}}}. Statically sized arrays also contribute to 
+  our <hask>vzipWith</hask>. Statically sized arrays also contribute to 
expressiveness and efficiency: for example, in Pascal we can copy one 
expressiveness and efficiency: for example, in Pascal we can copy one 

instance of an array into another instance of the same type by a 
instance of an array into another instance of the same type by a 

Line 1,297:  Line 1,293:  
A different approach to array processing is a socalled 
A different approach to array processing is a socalled 

shapeinvariant programming, which is a key feature of arrayoriented 
shapeinvariant programming, which is a key feature of arrayoriented 

−  languages such as APL or SaC [#SaC [ SaC] ]. These languages let a 
+  languages such as APL or [[#SaCSaC]]. These languages let a 
programmer define operations that can be applied to arrays of 
programmer define operations that can be applied to arrays of 

arbitrary shape/dimensionality. The code becomes shorter and free from 
arbitrary shape/dimensionality. The code becomes shorter and free from 

Line 1,304:  Line 1,300:  
eventually. Determining it at runtime is greatly 
eventually. Determining it at runtime is greatly 

inefficient. Therefore, highperformance arrayoriented languages 
inefficient. Therefore, highperformance arrayoriented languages 

−  employ shape inference [#Scholz01 [ Scholz01] ], which tries to 
+  employ shape inference [[#Scholz01Scholz01]], which tries to 
statically infer the dimensionalities or even exact sizes of all 
statically infer the dimensionalities or even exact sizes of all 

arrays in a program. Shape inference is, in general, undecidable, 
arrays in a program. Shape inference is, in general, undecidable, 

since arrays may be dynamically allocated. Therefore, one can either 
since arrays may be dynamically allocated. Therefore, one can either 

restrict the class of acceptable shapeinvariant programs to a 
restrict the class of acceptable shapeinvariant programs to a 

−  decidable subset, resort to a dependenttype language like Cayenne 
+  decidable subset, resort to a dependenttype language like 
−  [#Cayenne [ Cayenne] ], or use “soft typing.” The latter approach is 
+  [[#CayenneCayenne]], or use “soft typing”. The latter approach is 
−  described in [#Scholz01 [ Scholz01] ], which introduces a nonunique type 
+  described in [[#Scholz01Scholz01]], which introduces a nonunique type 
system based on a hierarchy of array types: from fully specialized 
system based on a hierarchy of array types: from fully specialized 

ones with the statically known sizes and dimensionality, to a type of 
ones with the statically known sizes and dimensionality, to a type of 

Line 1,322:  Line 1,318:  
and higherorder functions. Using shape inference for compilation of 
and higherorder functions. Using shape inference for compilation of 

shapeinvariant array operations into a highly efficient code is 
shapeinvariant array operations into a highly efficient code is 

−  presented in [#Kreye [ Kreye] ]. Their compiler tries to generate as 
+  presented in [[#KreyeKreye]]. Their compiler tries to generate as 
precise shapespecific code as possible. When the shape inference 
precise shapespecific code as possible. When the shape inference 

fails to give the exact sizes or dimensionalities, the compiler emits 
fails to give the exact sizes or dimensionalities, the compiler emits 

Line 1,332:  Line 1,328:  
shapecorrect. We strive to express assertions about the array sizes 
shapecorrect. We strive to express assertions about the array sizes 

and enforcing the programming style that assures them. We have shown 
and enforcing the programming style that assures them. We have shown 

−  the definitions of functions such as {{{vzipWith}}} whose the 
+  the definitions of functions such as <hask>vzipWith</hask> whose the 
argument and the result vectors are all of the same size. This 
argument and the result vectors are all of the same size. This 

constraint is assured at compiletime — even if we do not statically 
constraint is assured at compiletime — even if we do not statically 

know the exact sizes of the vectors. Because SaC lacks parametric 
know the exact sizes of the vectors. Because SaC lacks parametric 

polymorphism, it cannot express such an assertion and statically 
polymorphism, it cannot express such an assertion and statically 

−  verify it. If a SaC programmer applies a function such as {{{vzipWith}}} to vectors of unequal size, the compiler will not flag 
+  verify it. If a SaC programmer applies a function such as <hask>vzipWith</hask> to vectors of unequal size, the compiler will not flag 
that as an error but will compile a generic array code instead. The 
that as an error but will compile a generic array code instead. The 

error will be raised at run time during a range check. 
error will be raised at run time during a range check. 

The approach of the present paper comes close to emulating a 
The approach of the present paper comes close to emulating a 

−  dependent type system, of which Cayenne [#Cayenne [ Cayenne] ] is the 
+  dependent type system, of which [[#CayenneCayenne]] is the 
epitome. We were particularly influenced by a practical dependent type 
epitome. We were particularly influenced by a practical dependent type 

−  system of Hongwei Xi [#Xi98 [ Xi98] ] [#XiThesis [ XiThesis] ], which is 
+  system of Hongwei Xi [[#Xi98Xi98]] [[#XiThesisXiThesis]], which is 
−  a conservative extension of SML. In [#Xi98 [ Xi98] ], Hongwei Xi et 
+  a conservative extension of SML. In [[#Xi98Xi98]], Hongwei Xi et 
al. demonstrated an application of their system to the elimination of 
al. demonstrated an application of their system to the elimination of 

array bound checking and list tag checking. The related work section 
array bound checking and list tag checking. The related work section 

Line 1,354:  Line 1,350:  
C++ templates provide parametric polymorphism and indexing of 
C++ templates provide parametric polymorphism and indexing of 

types by true integers. A C++ programmer can therefore define 
types by true integers. A C++ programmer can therefore define 

−  functions like {{{vzipWith}}} and {{{vtail}}} with 
+  functions like <hask>vzipWith</hask> and <hask>vtail</hask> with 
equality and even arithmetic constraints on the sizes of the argument 
equality and even arithmetic constraints on the sizes of the argument 

−  vectors. Blitz++ [#Blitz [ Blitz] ] was the first example of using a 
+  vectors. [[#BlitzBlitz++]] was the first example of using a 
socalled template metaprogramming for generating efficient and safe 
socalled template metaprogramming for generating efficient and safe 

array code. The type system of C++ however presents innumerable 
array code. The type system of C++ however presents innumerable 

Line 1,367:  Line 1,363:  
incomprehensible. 
incomprehensible. 

−  McBride [#McBride [ McBride] ] gives an extensive survey of the 
+  [[#McBrideMcBride]] gives an extensive survey of the 
emulation of dependent type systems in Haskell. He also describes 
emulation of dependent type systems in Haskell. He also describes 

numberparameterized arrays that are similar to the ones discussed in 
numberparameterized arrays that are similar to the ones discussed in 

−  Section [#sec:Okasaki [ sec:Okasaki] ]. The paper by Fridlender and Indrika 
+  Section [[#Encoding the number parameter in data constructorssec:Okasaki]]. The 
−  [#Fridlender [ Fridlender] ] shows another example of emulating dependent 
+  [[#Fridlenderpaper by Fridlender and Indrika]] shows another example of emulating dependent 
types within the HindleyMilner type system: namely, emulating 
types within the HindleyMilner type system: namely, emulating 

−  variablearity functions such as generic {{{zipWith}}}. Their 
+  variablearity functions such as generic <hask>zipWith</hask>. Their 
technique relies on ad hoc codings for natural numbers which resemble 
technique relies on ad hoc codings for natural numbers which resemble 

Peano numerals. They aim at defining more functions (i.e., 
Peano numerals. They aim at defining more functions (i.e., 

Line 1,379:  Line 1,375:  
functions more restrictive by expressing sophisticated invariants in 
functions more restrictive by expressing sophisticated invariants in 

functions’ types. Another approach to multivariate functions — 
functions’ types. Another approach to multivariate functions — 

−  multivariate composition operator — is discussed in [#mcomp [ mcomp] ]. 
+  multivariate composition operator — is discussed in [[#mcompmcomp]]. 
== Conclusions == 
== Conclusions == 

−  [[Anchor(sec:conclusions)]]Throughout this paper we have demonstrated several realizations of 
+  Throughout this paper we have demonstrated several realizations of 
numberparameterized types in Haskell, using arrays parameterized by 
numberparameterized types in Haskell, using arrays parameterized by 

their size as an example. We have concentrated on techniques that 
their size as an example. We have concentrated on techniques that 

Line 1,404:  Line 1,400:  
vector sizes. Furthermore, we can write inequality constraints by 
vector sizes. Furthermore, we can write inequality constraints by 

means of an implicit existential quantification, e.g., the function 
means of an implicit existential quantification, e.g., the function 

−  {{{vhead}}} must be applied to a nonempty vector. The 
+  <hask>vhead</hask> must be applied to a nonempty vector. The 
programmer should benefit from more expressive function signatures 
programmer should benefit from more expressive function signatures 

and from the ability of the compiler to statically check complex 
and from the ability of the compiler to statically check complex 

Line 1,416:  Line 1,412:  
= References = 
= References = 

−  [[Anchor(Cayenne)]]Augustsson, L. Cayenne — a language with dependent types. Proc. ACM SIGPLAN International Conference on Functional Programming, pp. 239—250, 1998. 
+  <span id="Cayenne"></span>Augustsson, L. Cayenne — a language with dependent types. Proc. ACM SIGPLAN International Conference on Functional Programming, pp. 239—250, 1998. 
−  [[Anchor(Blume01)]]Matthias Blume: NoLongerForeign: Teaching an ML compiler to speak C “natively.” In BABEL’01: First workshop on multilanguage infrastructure and interoperability, September 2001, Firenze, Italy. [http://people.cs.uchicago.edu/~blume/pub.html] 
+  <span id="Blume01"></span>Matthias Blume: NoLongerForeign: Teaching an ML compiler to speak C “natively.” In BABEL’01: First workshop on multilanguage infrastructure and interoperability, September 2001, Firenze, Italy. [http://people.cs.uchicago.edu/~blume/pub.html] 
−  [[Anchor(CodeForPaper)]]The complete source code for the article. August 9, 2005. [http://pobox.com/~oleg/ftp/Haskell/numberparamvectorcode.tar.gz] 
+  <span id="CodeForPaper"></span>The complete source code for the article. August 9, 2005. [http://pobox.com/~oleg/ftp/Haskell/numberparamvectorcode.tar.gz] 
−  [[Anchor(Fridlender)]]Daniel Fridlender and Mia Indrika: Do we Need Dependent Types? BRICS Report Series RS0110, March 2001. [http://www.brics.dk/RS/01/10/] 
+  <span id="Fridlender"></span>Daniel Fridlender and Mia Indrika: Do we Need Dependent Types? BRICS Report Series RS0110, March 2001. [http://www.brics.dk/RS/01/10/] 
−  [[Anchor(mcomp)]]Oleg Kiselyov: Polyvariadic composition. October 31, 2003. [http://pobox.com/~oleg/ftp/Haskell/types.scm{{{#}}}polyvarcomp] 
+  <span id="mcomp"></span>Oleg Kiselyov: Polyvariadic composition. October 31, 2003. [http://pobox.com/~oleg/ftp/Haskell/types.scm{{{#}}}polyvarcomp] 
−  [[Anchor(stanamictrees)]]Oleg Kiselyov: Polymorphic stanamically balanced AVL trees. April 26, 2003. [http://pobox.com/~oleg/ftp/Haskell/types.scm{{{#}}}stanamicAVL] 
+  <span id="stanamictrees"></span>Oleg Kiselyov: Polymorphic stanamically balanced AVL trees. April 26, 2003. [http://pobox.com/~oleg/ftp/Haskell/types.scm{{{#}}}stanamicAVL] 
−  [[Anchor(Kreye)]]Dietmar Kreye: A Compilation Scheme for a Hierarchy of Array Types. Proc. 3th International Workshop on Implementation of Functional Languages (IFL’01). 
+  <span id="Kreye"></span>Dietmar Kreye: A Compilation Scheme for a Hierarchy of Array Types. Proc. 3th International Workshop on Implementation of Functional Languages (IFL’01). 
−  [[Anchor(McBride)]]Conor McBride: Faking it — simulating dependent types in Haskell. Journal of Functional Programming, 2002, v.12, pp. 375392 [http://www.cs.nott.ac.uk/~ctm/faking.ps.gz] 
+  <span id="McBride"></span>Conor McBride: Faking it — simulating dependent types in Haskell. Journal of Functional Programming, 2002, v.12, pp. 375392 [http://www.cs.nott.ac.uk/~ctm/faking.ps.gz] 
−  [[Anchor(Okasaki99)]]Chris Okasaki: From fast exponentiation to square matrices: An adventure in types. Proc. fourth ACM SIGPLAN International Conference on Functional Programming (ICFP ’99), Paris, France, September 2729, pp. 28  35, 1999 [http://www.eecs.usma.edu/Personnel/okasaki/pubs.html{{{#}}}icfp99] 
+  <span id="Okasaki99"></span>Chris Okasaki: From fast exponentiation to square matrices: An adventure in types. Proc. fourth ACM SIGPLAN International Conference on Functional Programming (ICFP ’99), Paris, France, September 2729, pp. 28  35, 1999 [http://www.eecs.usma.edu/Personnel/okasaki/pubs.html{{{#}}}icfp99] 
−  [[Anchor(Scholz01)]]SvenBodo Scholz: A Type System for Inferring Array Shapes. Proc. 3th International Workshop on Implementation of Functional Languages (IFL’01). [http://homepages.feis.herts.ac.uk/~comqss/research.html] 
+  <span id="Scholz01"></span>SvenBodo Scholz: A Type System for Inferring Array Shapes. Proc. 3th International Workshop on Implementation of Functional Languages (IFL’01). [http://homepages.feis.herts.ac.uk/~comqss/research.html] 
−  [[Anchor(SaC)]]SingleAssignment C homepage. [http://www.sachome.org/] 
+  <span id="SaC"></span>SingleAssignment C homepage. [http://www.sachome.org/] 
−  [[Anchor(Haskelllistquote)]]Dominic Steinitz: Re: Polymorphic Recursion / Rank2 Confusion. Message posted on the Haskell mailing list on Sep 21 2003. [http://www.haskell.org/pipermail/haskell/2003September/012726.html] 
+  <span id="Haskelllistquote"></span>Dominic Steinitz: Re: Polymorphic Recursion / Rank2 Confusion. Message posted on the Haskell mailing list on Sep 21 2003. [http://www.haskell.org/pipermail/haskell/2003September/012726.html] 
−  [[Anchor(Blitz)]]Todd L. Veldhuizen: Arrays in Blitz++. Proc. 2nd International Scientific Computing in ObjectOriented Parallel Environments (ISCOPE’98). Santa Fe, New Mexico, 1998. [http://www.oonumerics.org/blitz/manual/blitz.html] 
+  <span id="Blitz"></span>Todd L. Veldhuizen: Arrays in Blitz++. Proc. 2nd International Scientific Computing in ObjectOriented Parallel Environments (ISCOPE’98). Santa Fe, New Mexico, 1998. [http://www.oonumerics.org/blitz/manual/blitz.html] 
−  [[Anchor(Xi98)]]Hongwei Xi, Frank Pfenning: Eliminating Array Bound Checking Through Dependent Types. Proc. ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 249—257, 1998. [http://www2.cs.cmu.edu/~hwxi/] 
+  <span id="Xi98"></span>Hongwei Xi, Frank Pfenning: Eliminating Array Bound Checking Through Dependent Types. Proc. ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 249—257, 1998. [http://www2.cs.cmu.edu/~hwxi/] 
−  [[Anchor(XiThesis)]]Hongwei Xi: Dependent Types in Practical Programming. Ph.D thesis, Carnegie Mellon University, September 1998. [http://www.cs.bu.edu/~hwxi/] 
+  <span id="XiThesis"></span>Hongwei Xi: Dependent Types in Practical Programming. Ph.D thesis, Carnegie Mellon University, September 1998. [http://www.cs.bu.edu/~hwxi/] 
+   

+  <references/> 

 
 

CategoryCategory CategoryArticle 
CategoryCategory CategoryArticle 
Revision as of 05:51, 26 October 2008
This article needs reformatting! Please help tidy it up.WouterSwierstra 14:26, 9 May 2008 (UTC)
1 Numberparameterized types
This article is also available in PDF. This Wiki page is not the master file: rather, it is the result of the SXML>Wiki conversion.
2 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 compiletime error
with a clear error message. Numberparameterized types let the
programmer capture more invariants through types and eliminate some
runtime checks.
We review several encodings of the numeric
parameter but concentrate on the phantom type representation of a
sequence of decimal digits. The decimal encoding makes
programming with numberparameterized types convenient and error
messages more comprehensible. We implement arithmetic on
decimal numberparameterized types, which lets us statically
typecheck operations such as array concatenation.
Overall we demonstrate a practical
dependenttypelike system that is just a Haskell library. The basics
of the numberparameterized types are written in Haskell98.
2.1 Keywords:
Haskell, numberparameterized types, type arithmetic, decimal types, typedirected programming.
3 Contents
3.1 Introduction
Discussions about types parameterized by values — especially types of arrays or finite groups parameterized by their size — reoccur every couple of months on functional programming languages newsgroups and mailing lists. The often expressed wish is to guarantee that, for example, we never attempt to add two vectors of different lengths. As one poster said, “This [feature] would be helpful in the crypto library where I end up having to either define new length Words all the time or using lists and losing the capability of ensuring I am manipulating lists of the same length.” Numberparameterized types as other more expressive types let us tell the typechecker our intentions. The typechecker may then help us write the code correctly. Many errors (which are often trivial) can be detected at compile time. Furthermore, we no longer need to litter the code with array boundary match checks. The code therefore becomes more readable, reliable, and fast. Numberparameterized types when expressed in signatures also provide a better documentation of the code and let the invariants be checked across module boundaries.
In this paper, we develop realizations of numberparameterized types in Haskell that indeed have all the above advantages. The numeric parameter is specified in decimal rather than in binary, which makes types smaller and far easier to read. Type error messages also become more comprehensible. The programmer may write or the compiler can infer equality constraints (e.g., two argument vectors of a function must be of the same size), arithmetic constraints (e.g., one vector must be larger by some amount), and inequality constraints (e.g., the size of the argument vector must be at least one). The violations of the constraints are detected at compile time. We can remove runtime tag checks in functions like
vector.
Although we come close to the dependenttype programming, we do not extend either a compiler or the language. Our system is a regular Haskell library. In fact, the basic numberparameterized types can be implemented entirely in Haskell98. Advanced operations such as type arithmetic require commonly supported Haskell98 extensions to multiparameter classes with functional dependencies and higherranked types.
Our running example is arrays parameterized over their size. The parameter of the vector type is therefore a nonnegative integer number. For simplicity, all the vectors in the paper are indexed from zero. In addition to vector constructors and element accessors, we
define athe third, element by element. An attempt to map vectors of different sizes should be reported as a type error. The typechecker will also guarantee that there is no attempt to allocate a vector of a negative
size. In Section sec:arithmetic we introduce operationsThe types of these operations exhibit arithmetic and inequality constraints.
The present paper describes several gradually more sophisticated numberparameterized Haskell libraries. We start by paraphrasing the approach by Chris Okasaki, who represents the size parameter of vectors in a sequence of data constructors. We then switch to the encoding of the size in a sequence of type constructors. The resulting types are phantom and impose no runtime overhead. Section sec:unarytype describes unary encoding of numerals in type constructors, Sections sec:decimalfixed and sec:decimalarb discuss decimal encodings. Section sec:decimalfixed introduces a type representation for fixedprecision decimal numbers. Section sec:decimalarb removes the limitation on the maximal size of representable numbers, at a cost of a more complex implementation and of replacing commas with unsightly dollars signs. The decimal encoding is extendible to other bases, e.g., 16 or 64. The latter can be used to develop practical realizations of numberparameterized cryptographically interesting groups.
Section sec:arithmetic describes the first contribution of the paper. We develop addition and subtraction of “decimal types”, i.e., of the type constructor applications representing nonnegative integers in decimal notation. The implementation is significantly different from that for more common unary numerals. Although decimal numerals are notably difficult to add, they make numberparameterized programming practical. We can now write arithmetic equality and inequality constraints on numberparameterized types.
Section sec:dynamic briefly describes working with numberparameterized types when the numeric parameter, and even its upper bound, are not known until run time. We show one, quite simple technique, which assures a static constraint by a runtime check — witnessing. The witnessing code, which must be trustworthy, is notably compact. The section uses the method of blending of static and dynamic assurances that was first described in stanamictrees.
Section sec:related compares our approach with the phantom type programming in SML by Matthias Blume, with a practical dependenttype system of Hongwei Xi, with staticallysized and generic arrays in Pascal and C, with the shape inference in arrayoriented languages, and with C++ template metaprogramming. Section sec:conclusions concludes.
3.2 Encoding the number parameter in data constructors
The first approach to vectors parameterized by their size encodes the size as a series of data constructors. This approach has been used extensively by Chris Okasaki. For example, in Okasaki99 he describes square matrixes whose dimensions can be proved equal at compile time. He digresses briefly to demonstrate vectors of statically known size. A similar technique has been described by McBride. In this section, we develop a more naive encoding of the size through data constructors, for introduction and comparison with the encoding of the size via type constructors in the following sections.
Our representation of vectors of a statically checked size is reminiscent of the familiar representation of lists:
data List a = Nil  Cons a (List a)
have the same recursive type. To make the types different (so that we can represent the size, too) we break the explicit recursion in the datatype declaration. We introduce two data constructors:
module UnaryDS where data VZero a = VZero deriving Show infixr 3 :+: data Vecp tail a = a :+: (tail a) deriving Show
type of a vector clearly encodes vector’s size, as repeated
applications of a type constructordesigned a numberparameterized type.
To generically manipulate the family of differentlysized vectors, we define a class of polymorphic functions:
class Vec t where vlength:: t a > Int vat:: t a > Int > a vzipWith:: (a>b>c) > t a > t b > t c
types, but the vectors must have the same shape, i.e., size.
The implementation of the classinstances:
instance Vec VZero where vlength = const 0 vat = error "null array or index out of range" vzipWith f a b = VZero instance (Vec tail) => Vec (Vecp tail) where vlength (_ :+: t) = 1 + vlength t vat (a :+: _) 0 = a vat (_ :+: ta) n = vat ta (n1) vzipWith f (a :+: ta) (b :+: tb) = (f a b) :+: (vzipWith f ta tb)
lists, our vectors reveal their sizes in their types.
That was the complete implementation of the numberparameterized vectors. We can now define a few sample vectors:
v3c = 'a' :+: 'b' :+: 'c' :+: VZero v3i = 1 :+: 2 :+: 3 :+: VZero v4i = 1 :+: 2 :+: 3 :+: 4 :+: VZero
and a few simple tests:
test1 = vlength v3c test2 = [vat v3c 0, vat v3c 1, vat v3c 2]
We can load the code into a Haskell system and run the tests. Incidentally, we can ask the Haskell system to tell us the inferred type of a sample vector:
*UnaryDS> :t v3c Vecp (Vecp (Vecp VZero)) Char
The inferred type indeed encodes the size of the vector as a Peano numeral. We can try more complex tests, of elementwise operations on two vectors:
test3 = vzipWith (\c i > (toEnum $ fromEnum c + fromIntegral i)::Char) v3c v3i test4 = vzipWith (+) v3i v3i *UnaryDS> test3 'b' :+: ('d' :+: ('f' :+: VZero))
vectors of the same shape but of different element types.
An attempt to add, by mistake, two vectors of different sizes is revealing:
test5 = vzipWith (+) v3i v4i Couldn't match `VZero' against `Vecp VZero' Expected type: Vecp (Vecp (Vecp VZero)) a Inferred type: Vecp (Vecp (Vecp (Vecp VZero))) a1 In the third argument of `vzipWith', namely `v4i' In the definition of `test5': vzipWith (+) v3i v4i
We get a type error, with a clear error message (the quoted message, here and elsewhere in the paper, is by GHCi. The Hugs error message is essentially the same). The typechecker, at the compile time, has detected that the sizes of the vectors to add elementwise do not match. To be more precise, the sizes are off by one.
For vectors described in this section, the element access
operation,n is the size of the vector. Chris Okasaki has designed more sophisticated numberparameterized vectors with element access time O(log n). Although this is an improvement, the overhead of accessing an element adds up for many operations. Furthermore, the overhead of data constructors,
vectors. When we encode the size of a vector as a sequence of data constructors, the latter overhead cannot be eliminated.
Although we have achieved the separation of the shape type of a vector from the type of its elements, we did so at the expense of a
sequence of data constructors,level. These constructors add time and space overheads, which increase with the vector size. In the following sections we show more efficient representations for numberparameterized vectors. The structure of their type will still tell us the size of the vector; however there will be no corresponding term structure, and, therefore, no space overhead of storing it nor runtime overhead of traversing it.
3.3 Encoding the number parameter in type constructors, in unary
To improve the efficiency of numberparameterized vectors, we choose a better runtime representation: Haskell arrays. The code in the present section is in Haskell98.
module UnaryT (..elided..) where import Data.Array
First, we need a type structure (an infinite family of types) to encode nonnegative numbers. In the present section, we will use an unary encoding in the form of Peano numerals. The unary type encoding of integers belongs to programming folklore. It is also described in Blume01 in the context of a foreignfunction interface library of SML.
data Zero = Zero data Succ a = Succ a
numerals Peano numerals because the number n is represented as a repeated application of n type (data)
constructorsnumerals and the terms. In fact, a numeral term looks precisely the same as its type. This property is crucial as we shall see on many occasions below. It lets us “lift” number computations to the type level. The property also makes error messages lucid
<ref>We could have declaredtag and all nonbottom Peano numerals share the same runtime representation. As we shall see however, we hardly ever use the values of our numerals.</ref>.
We place our Peano numerals into a classcorresponding number.
class Card c where c2num:: (Num a) => c > a  convert to a number cpred::(Succ c) > c cpred = undefined instance Card Zero where c2num _ = 0 instance (Card c) => Card (Succ c) where c2num x = 1 + c2num (cpred x)
positive Peano numeral. The definition for that function may seem puzzling: it is undefined. We observe that the callers do not need the value returned by that function: they merely need the type of that
value. Indeed, let us examine the definitions of the methodnumber zero, which we return. There can be only one nonbottom value
of the typenot need to examine the value. Likewise, in the instance
The same correspondence between the types and the terms suggests that the numeral type alone is enough to describe the size of a vector. We do not need to store the value of the numeral. The shape type of our vectors could be phantom (as in Blume01).
newtype Vec size a = Vec (Array Int a) deriving Show
constanttime element access. As we mentioned earlier, for simplicity, all the vectors in the paper are indexed from zero. The data
constructorhas to use the following functions to construct vectors.
listVec':: (Card size) => size > [a] > Vec size a listVec' size elems = Vec $ listArray (0,(c2num size)1) elems listVec:: (Card size) => size > [a] > Vec size a listVec size elems  not (c2num size == length elems) = error "listVec: static/dynamic sizes mismatch" listVec size elems = listVec' size elems vec:: (Card size) => size > a > Vec size a vec size elem = listVec' size $ repeat elem
of the requested size initialized with the given values. The function makes no check that the length of the list of the initial values
following expression creates a boolean vector of two elements with the
initial values*UnaryT> listVec (Succ (Succ Zero)) [True,False] Vec (array (0,1) [(0,True),(1,False)])
A Haskell interpreter created the requested value, and printed it out. We can confirm that the inferred type of the vector encodes its size:
*UnaryT> :type listVec (Succ (Succ Zero)) [True,False] Vec (Succ (Succ Zero)) Bool
We can now introduce functions to operate on our vectors. The functions are similar to those in the previous section. As before, they are polymorphic in the shape of vectors (i.e., their sizes). This polymorphism is expressed differently however. In the present section we use just the parametric polymorphism rather than typeclasses.
vlength_t:: Vec size a > size vlength_t _ = undefined vlength:: Vec size a > Int vlength (Vec arr) = let (0,last) = bounds arr in last+1 velems:: Vec size a > [a] velems (Vec v) = elems v vat:: Vec size a > Int > a vat (Vec arr) i = arr ! i vzipWith:: Card size => (a>b>c) > Vec size a > Vec size b > Vec size c vzipWith f va vb = listVec' (vlength_t va) $ zipWith f (velems va) (velems vb)
returns the element of a vector at a given zerobased index. The function
corresponding elements of the argument vectors. The polymorphic types of these functions indicate that the functions generically operate on
numberparameterized vectors of anytwo argument vectors must have the same size. The result will be a vector of the same size as that of the argument vectors. We rely on
the fact that the functionlists of the same size, gives the list of that size. This justifies our
use ofWe have introduced two functions that yield the size of their
argument vector. One is the functionreturns a value whose type represents the size of the vector. We are interested only in the type of the return value — which we extract
statically from the type of the argument vector. The functiontype is sound.
From the practical point of view, passing terms such as
section showed a better approach. We can implement it here too: we let the user enumerate the values, which we accumulate into a list, counting them at the same time:
infixl 3 &+ data VC size a = VC size [a] vs:: VC Zero a; vs = VC Zero [] (&+):: VC size a > a > VC (Succ size) a (&+) (VC size lst) x = VC (Succ size) (x:lst) vc:: (Card size) => VC size a > Vec size a vc (VC size lst) = listVec' size (reverse lst)
The counting operation is effectively performed by a typechecker
at compile time. Finally, the functionand initialize the vector of the right size — and of the right type. Here are a few sample vectors and operations on them:
v3c = vc $ vs &+ 'a' &+ 'b' &+ 'c' v3i = vc $ vs &+ 1 &+ 2 &+ 3 v4i = vc $ vs &+ 1 &+ 2 &+ 3 &+ 4 test1 = vlength v3c; test1' = vlength_t v3c test2 = [vat v3c 0, vat v3c 1, vat v3c 2] test3 = vzipWith (\c i > (toEnum $ fromEnum c + fromIntegral i)::Char) v3c v3i test4 = vzipWith (+) v3i v3i
We can run the tests as follows:
*UnaryT> test3 Vec (array (0,2) [(0,'b'),(1,'d'),(2,'f')]) *UnaryT> :type test3 Vec (Succ (Succ (Succ Zero))) Char
The type of the result bears the clear indication of the size of the vector. If we attempt to perform an elementwise operation on vectors of different sizes, for example:
test5 = vzipWith (+) v3i v4i Couldn't match `Zero' against `Succ Zero' Expected type: Vec (Succ (Succ (Succ Zero))) a Inferred type: Vec (Succ (Succ (Succ (Succ Zero)))) a1 In the third argument of `vzipWith', namely `v4i' In the definition of `test5': vzipWith (+) v3i v4i
we get a message from the typechecker that the sizes are off by one.
3.4 Fixedprecision decimal types
Peano numerals adequately represent the size of a vector in vector’s type. However, they make the notation quite verbose. We want to offer a programmer a familiar, decimal notation for the terms and the types representing nonnegative numerals. This turns out possible even in Haskell98. In this section, we describe a fixedprecision notation, assuming that a programmer will never need a vector with more than 999 elements. The limit is not hard and can be readily extended. The next section will eliminate the limit altogether.
We again will be using Haskell arrays as the runtime representation for our vectors. In fact, the implementation of vectors is the same as that in the previous section. The only change is the use of decimal rather than unary types to describe the sizes of our vectors.
module FixedDecT (..export list elided..) where import Data.Array
Since we will be using the decimal notation, we need the terms and the types for all ten digits:
data D0 = D0 data D1 = D1 ... data D9 = D9
For clarity and to save space, we elide repetitive code fragments. The full code is available. To manipulate the digits uniformly (e.g., to find out the
corresponding integer), we put them into a classdigits.
class Digit d where  class of digits d2num:: (Num a) => d > a  convert to a number instance Digit D0 where d2num _ = 0 instance Digit D1 where d2num _ = 1 ... instance Digit D9 where d2num _ = 9 class Digit d => NonZeroDigit d instance NonZeroDigit D1 instance NonZeroDigit D2 ... instance NonZeroDigit D9
We define a class of nonnegative numerals. We make all singledigit numerals the members of that class:
class Card c where c2num:: (Num a) => c > a  convert to a number  Singledigit numbers are nonnegative numbers instance Card D0 where c2num _ = 0 instance Card D1 where c2num _ = 1 ... instance Card D9 where c2num _ = 9
the constraint lucid. We also introduce threedigit decimal
numeralsinstance (NonZeroDigit d1,Digit d2) => Card (d1,d2) where c2num c = 10*(d2num $ t12 c) + (d2num $ t22 c) instance (NonZeroDigit d1,Digit d2,Digit d3) => Card (d1,d2,d3) where c2num c = 100*(d2num $ t13 c) + 10*(d2num $ t23 c) + (d2num $ t33 c)
guarantee the uniqueness of our representation of numbers: the major decimal digit of a multidigit number is not zero. It will be a type error to attempt to form such an number:
*FixedDecT> vec (D0,D1) 'a' <interactive>:1: No instance for (NonZeroDigit D0)
Glasgow extensions, which supports local type variables. We feel however that keeping the code Haskell98 justifies the extra hassle:
t12::(a,b) > a; t12 = undefined t22::(a,b) > b; t22 = undefined ... t33::(a,b,c) > c; t33 = undefined
The rest of the code is as before, e.g.:
newtype Vec size a = Vec (Array Int a) deriving Show listVec':: Card size => size > [a] > Vec size a listVec' size elems = Vec $ listArray (0,(c2num size)1) elems
as those in Section sec:unarytype. We elide the code for the sake of space. We introduce a few sample vectors, using the decimal notation this time:
v12c = listVec (D1,D2) $ take 12 ['a'..'z'] v12i = listVec (D1,D2) [1..12] v13i = listVec (D1,D3) [1..13]
The decimal notation is so much convenient. We can now define long vectors without pain. As before, the type of our vectors — the size part of the type — looks precisely the same as the corresponding size term expression:
*FixedDecT> :type v12c Vec (D1, D2) Char
We can use the sample vectors in the tests like those of the previous section. If we attempt to elementwise add two vectors of different sizes, we get a type error:
test5 = vzipWith (+) v12i v13i Couldn't match `D2' against `D3' Expected type: Vec (D1, D2) a Inferred type: Vec (D1, D3) a1 In the third argument of `vzipWith', namely `v13i' In the definition of `test5': vzipWith (+) v12i v13i
The error message literally says that 12 is not equal to 13: the typechecker expected a vector of size 12 but found a vector of size 13 instead.
3.5 Arbitraryprecision decimal types
From the practical point of view, the fixedprecision numberparameterized vectors of the previous section are sufficient. The imposition of a limit on the width of the decimal numerals — however easily extended — is nevertheless intellectually unsatisfying. One may wish for an encoding of arbitrarily large decimal numbers within a framework that has been set up once and for all. Such an SML framework has been introduced in Blume01, to encode the sizes of arrays in their types. It is interesting to ask if such an encoding is possible in Haskell. The present section demonstrates a representation of arbitrary large decimal numbers in Haskell98. We also show that typeclasses in Haskell have made the encoding easier and precise: our decimal types are in bijection with nonnegative integers. As before, we use the decimal types as phantom types describing the shape of numberparameterized vectors.
We start by defining the types for the ten digits:
module ArbPrecDecT (..export list elided..) where import Data.Array data D0 a = D0 a data D1 a = D1 a ... data D9 a = D9 a
use the composition of the constructors to represent sequences of digits. And so we introduce a class for arbitrary sequences of digits:
class Digits ds where ds2num:: (Num a) => ds > a > a
with a method to convert a sequence to the corresponding
number. The methodaccumulatorpassing style: its second argument is the accumulator. We
also need a type, which we callsequence of digits:
data Sz = Sz  zero size (or the Nil of the sequence) instance Digits Sz where ds2num _ acc = acc
We now inductively define arbitrarily long sequences of digits:
instance (Digits ds) => Digits (D0 ds) where ds2num dds acc = ds2num (t22 dds) (10*acc) instance (Digits ds) => Digits (D1 ds) where ds2num dds acc = ds2num (t22 dds) (10*acc + 1) ... instance (Digits ds) => Digits (D9 ds) where ds2num dds acc = ds2num (t22 dds) (10*acc + 9) t22::(f x) > x; t22 = undefined
and nine. Compositions of data/type constructors indeed encode sequences of digits. As before, the terms and the types look precisely the same. The compositions can of course be arbitrarily long:
*ArbPrecDecT> :type D1$ D2$ D3$ D4$ D5$ D6$ D7$ D8$ D9$ D0$ D9$ D8$ D7$ D6$ D5$ D4$ D3$ D2$ D1$ Sz D1 (D2 (D3 (D4 (D5 (D6 (D7 (D8 (D9 (D0 (D9 (D8 (D7 (D6 (D5 (D4 (D3 (D2 (D1 Sz)))))))))))))))))) *ArbPrecDecT> ds2num (D1$ D2$ D3$ D4$ D5$ D6$ D7$ D8$ D9$ D0$ D9$ D8$ D7$ D6$ D5$ D4$ D3$ D2$ D1$ Sz) 0 1234567890987654321
We should point out a notable advantage of Haskell typeclasses in designing of sophisticated type families — in particular, in specifying constraints. Nothing prevents a programmer from using our
type constructors, e.g.,into that type:
*ArbPrecDecT> :type D1 True D1 Bool *ArbPrecDecT> :type (undefined::D1 Bool) D1 Bool
However, such types do not represent decimal sequences. Indeed, an attempt to pass either of these values to
*ArbPrecDecT> ds2num (undefined::D1 Bool) 0 No instance for (Digits Bool) arising from use of `ds2num' at <interactive>:1 In the definition of `it': ds2num (undefined :: D1 Bool) 0
In contrast, the approach in Blume01 prevented the user from constructing (nonbottom) values of these types by a careful design and export of value constructors. That approach relied on SML’s module system to preclude the overt misuse of the decimal type system. Yet the user can still form a (latent, in SML) bottom value of the “bad” type, e.g., by attaching an appropriate type signature to an empty list, error function or other suitable polymorphic value. In a nonstrict language like Haskell such values would make our approach, which relies on phantom types, unsound. Fortunately, we are able to eliminate illformed decimal types at the type level rather than at
the term level. Our classTo guarantee the bijection between nonnegative numbers and sequences of digits, we need to impose an additional restriction: the first, i.e., the major, digit of a sequence must be nonzero. Expressing such a restriction is surprisingly straightforward in Haskell, even Haskell98.
class (Digits c) => Card c where c2num:: (Num a) => c > a c2num c = ds2num c 0 instance Card Sz instance (Digits ds) => Card (D1 ds) instance (Digits ds) => Card (D2 ds) ... instance (Digits ds) => Card (D9 ds)
represents nonnegative integers. A nonnegative integer is realized here as a sequence of decimal digits — provided, as the instances specify, that the sequence starts with a digit other than zero. We can now define the type of our numberparameterized vectors:
newtype Vec size a = Vec (Array Int a) deriving Show
v12c = listVec (D1 $ D2 Sz) $ take 12 ['a'..'z'] v12i = listVec (D1 $ D2 Sz) [1..12] v13i = listVec (D1 $ D3 Sz) [1..13]
we should note a slight change of notation compared to the corresponding vectors of Section sec:decimalfixed. The tests are not changed and continue to work as before:
test4 = vzipWith (+) v12i v12i *ArbPrecDecT> :type test4 Vec (D1 (D2 Sz)) Int *ArbPrecDecT> test4 Vec (array (0,11) [(0,2),(1,4),(2,6),...(11,24)])
The compiler has been able to infer the size of the result of the
decimal in the type of the vector. Again, an attempt to elementwise add vectors of different sizes leads to a type error:
test5 = vzipWith (+) v12i v13i Couldn't match `D2 Sz' against `D3 Sz' Expected type: Vec (D1 (D2 Sz)) a Inferred type: Vec (D1 (D3 Sz)) a1 In the third argument of `vzipWith', namely `v13i' In the definition of `test5': vzipWith (+) v12i v13i
The typechecker complains that 2 is not equal to 3: it found the vector of size 13 whereas it expected a vector of size 12. The decimal types make the error message very clear.
We must again point out a significant difference of our approach from that of Blume01. We were able to state that only those types of digital sequences that start with a nonzero digit correspond to a nonnegative number. SML, as acknowledged in Blume01, is unable to express such a restriction directly. The paper, therefore, prevents the user from building invalid decimal sequences by relying on the module system: by exporting carefullydesigned value constructors. The latter use an auxiliary phantom type to keep track of “nonzeroness” of the major digit. Our approach does not incur such a complication. Furthermore,
by the very inductive construction of the classesin decimal notation. In Blume01, the similar mapping holds only when the family of decimal types is restricted to the types that correspond to constructible values. A user of that system may still form bottom values of invalid decimal types, which will cause runtime errors. In our case, when the digit constructors are
misapplied, the result will no longer be in the classtypechecker:
*ArbPrecDecT> vec (D1$ D0$ D0$ True) 0 No instance for (Digits Bool) arising from use of `vec' at <interactive>:1 In the definition of `it': vec (D1 $ (D0 $ (D0 $ True))) 0 *ArbPrecDecT> vec (D0$ D1$ D0 Sz) 0 No instance for (Card (D0 (D1 (D0 Sz)))) arising from use of `vec' at <interactive>:1 In the definition of `it': vec (D0 $ (D1 $ (D0 Sz))) 0
3.6 Computations with decimal types
The previous sections gave many examples of functions such as
known to be of equal size. The signature of these functions states quite detailed invariants whose violations will be reported at compiletime. Furthermore, the invariants can be inferred by the compiler itself. This use of the type system is not particular to Haskell: Matthias Blume has derived a similar parameterization of arrays in SML, which can express such equality of size constraints. Matthias Blume however cautions one not to overstate the usefulness of the approach because the type system can express only fairly simple constraints: “There is still no type that, for example, would force two otherwise arbitrary arrays to differ in size by exactly one.” That was written in the context of SML however. In Haskell with common extensions we can define vector functions whose type contains arithmetic constraints on the sizes of the argument and the result vectors. These constraints can be verified statically and sometimes even inferred by a compiler. In this section, we consider the example of vector concatenation. We shall see that the
inferred type ofof the result is the sum of the sizes of two argument vectors. We also
introduce the functionswhose type specifies that they can only be applied to nonempty
vectors. Furthermore, the type ofsize of the result vector is less by one than the size of the argument vector. These examples are quite unusual and almost cross into the realm of dependent types.
We must note however that the examples in this section require the Haskell98 extension to multiparameter classes with functional
dependencies. That extension is activated by flagsGHCi.
We will be using the arbitrary precision decimal types introduced in the previous section. We aim to design a ‘type addition’ of decimal sequences. Our decimal types spell the corresponding nonnegative numbers in the conventional (i.e., bigendian) decimal notation: the mostsignificant digit first. However, it is more convenient to add such numbers starting from the leastsignificant digit. Therefore, we need a way to reverse digital sequences, or more precise, types of the
classalgorithm written in the accumulatorpassing style.
class DigitsInReverse' df w dr  df w > dr instance DigitsInReverse' Sz acc acc instance (Digits (d drest), DigitsInReverse' drest (d acc) dr) => DigitsInReverse' (d drest) acc dr
instances spell this constraint out. We can now introduce a class that relates a sequence of digits with its reverse:
class DigitsInReverse df dr  df > dr, dr > df instance (DigitsInReverse' df Sz dr, DigitsInReverse' dr Sz df) => DigitsInReverse df dr
each other. The functional dependencies make the “each other” part clear: one sequence uniquely determines the other. The typechecker
will verify that givendigits_rev:: (Digits ds, Digits dsr, DigitsInReverse ds dsr) => ds > dsr digits_rev = undefined
It is again a compiletime function specified entirely by its type. Its body is therefore undefined. We can now run a few examples:
*ArbArithmT> :t digits_rev (D1$D2$D3 Sz) D3 (D2 (D1 Sz)) *ArbArithmT> :t (\v > digits_rev v `asTypeOf` (D1$D2$D3 Sz)) D3 (D2 (D1 Sz)) > D1 (D2 (D3 Sz))
Indeed, the process of reversing sequences of decimal digits works
both ways. Given the type of the argument tothe compiler infers the type of the result. Conversely, given the type of the result the compiler infers the type of the argument.
A sequence of digits belongs to the classif the mostsignificant digit is not a zero. To convert an arbitrary
sequence toclass NoLeadingZeros d d0  d > d0 instance NoLeadingZeros Sz Sz instance (NoLeadingZeros d d') => NoLeadingZeros (D0 d) d' instance NoLeadingZeros (D1 d) (D1 d) ... instance NoLeadingZeros (D9 d) (D9 d)
We are now ready to build the addition machinery. We draw our inspiration from the computer architecture: the adder of an arithmeticallogical unit (ALU) of the CPU is constructed by chaining of socalled fulladders. A fulladder takes two summands and the carryin and yields the result of the summation and the carryout. In our case, the summands and the result are decimal rather than binary. Carry is still binary.
class FullAdder d1 d2 cin dr cout  d1 d2 cin > cout, d1 d2 cin > dr, d1 dr cin > cout, d1 dr cin > d2 where _unused:: (d1 xd1) > (d2 xd2) > cin > (dr xdr) _unused = undefined
constructors. The functional dependencies of the class tell us that the summands and the input carry uniquely determine the result digit and the output carry. On the other hand, if we know the result digit,
one of the summands,can therefore be used for addition and for subtraction. In the latter case, the carry bits should be more properly called borrow bits.
data Carry0 data Carry1 instance FullAdder D0 D0 Carry0 D0 Carry0 instance FullAdder D0 D0 Carry1 D1 Carry0 instance FullAdder D0 D1 Carry0 D1 Carry0 ... instance FullAdder D9 D8 Carry1 D8 Carry1 instance FullAdder D9 D9 Carry0 D8 Carry1 instance FullAdder D9 D9 Carry1 D9 Carry1
The full code indeed contains 200 instances of
functional dependencies of the class. The number of instances could be significantly reduced if we availed ourselves to an overlapping instances extension. For generality however we tried to use as few Haskell98 extensions as possible. Although 200 instances seems like quite many, we have to write them only once. We place the instances into a module and separately compile it. Furthermore, we did not write those instances by hand: we used Haskell itself:
make_full_adder = mapM_ putStrLn [unwords $ doit d1 d2 cin  d1<[0..9], d2<[0..9], cin<[0..1]] where doit d1 d2 cin = ["instance FullAdder", tod d1, tod d2, toc cin, tod d12, toc cout] where (d12,cout) = let sum = d1 + d2 + cin in if sum >= 10 then (sum10,1) else (sum,0) tod n  (n >= 0 && 9 >= n) = "D" ++ (show n) toc 0 = "Carry0"; toc 1 = "Carry1"
That function is ready for Template Haskell. Currently we used a lowtech approach of cutting and pasting from an Emacs buffer with GHCi into the Emacs buffer with the code.
We useonwards, and we propagate the carry. If one input sequence turns out shorter than the other, we pad it with zeros. The correctness of the algorithm follows by simple induction.
class DigitsSum ds1 ds2 cin dsr  ds1 ds2 cin > dsr instance DigitsSum Sz Sz Carry0 Sz instance DigitsSum Sz Sz Carry1 (D1 Sz) instance (DigitsSum (D0 Sz) (d2 d2rest) cin (d12 d12rest)) => DigitsSum Sz (d2 d2rest) cin (d12 d12rest) instance (DigitsSum (d1 d1rest) (D0 Sz) cin (d12 d12rest)) => DigitsSum (d1 d1rest) Sz cin (d12 d12rest) instance (FullAdder d1 d2 cin d12 cout, DigitsSum d1rest d2rest cout d12rest) => DigitsSum (d1 d1rest) (d2 d2rest) cin (d12 d12rest)
subtraction to be nonnegative.
class DigitsDif ds1 ds2 cin dsr  ds1 dsr cin > ds2 instance DigitsDif Sz ds Carry0 ds instance (DigitsDif (D0 Sz) (d2 d2rest) Carry1 (d12 d12rest)) => DigitsDif Sz (d2 d2rest) Carry1 (d12 d12rest) instance (FullAdder d1 d2 cin d12 cout, DigitsDif d1rest d2rest cout d12rest) => DigitsDif (d1 d1rest) (d2 d2rest) cin (d12 d12rest)
together:
class (Card c1, Card c2, Card c12) => CardSum c1 c2 c12  c1 c2 > c12, c1 c12 > c2 instance (Card c1, Card c2, Card c12, DigitsInReverse c1 c1r, DigitsInReverse c2 c2r, DigitsSum c1r c2r Carry0 c12r, DigitsDif c1r c2r' Carry0 c12r, DigitsInReverse c2r' c2', NoLeadingZeros c2' c2, DigitsInReverse c12r c12) => CardSum c1 c2 c12
that the latter is the sum of the formers. The two summands determine the sum, or the sum and one summand determine the other. The class can be used for addition and subtraction of sequences. The dependencies of
the solereverse the summand sequences to make them littleendian, add them together with the zero carry, and reverse the result. We also make sure that the subtraction and summation are the exact inverses. The
addition algorithmwith the major digit zero. The subtraction algorithm however may result in a sequence with zero major digits, which have to be stripped
away, with the help of the relationthe addition out:
card_sum:: CardSum c1 c2 c12 => c1 > c2 > c12 card_sum = undefined
*ArbArithmT> :t card_sum (D1 Sz) (D9$D9 Sz) D1 (D0 (D0 Sz)) *ArbArithmT> :t \v > card_sum (D1 Sz) v `asTypeOf` (D1$D0$D0 Sz) D9 (D9 Sz) > D1 (D0 (D0 Sz)) *ArbArithmT> :t \v > card_sum (D9$D9 Sz) v `asTypeOf` (D1$D0$D0 Sz) D1 Sz > D1 (D0 (D0 Sz))
The typechecker can indeed add and subtract with carry and
borrow. Now we define the functionconcatenate two vectors.
vappend va vb = listVec (card_sum (vlength_t va) (vlength_t vb)) $ (velems va) ++ (velems vb)
we chose however to perform a runtime check and avoid proving the theorem about the size of the list concatenation result. We did not declare
the type of*ArbArithmT> :t vappend vappend :: (CardSum size size1 c12) => Vec size a > Vec size1 a > Vec c12 a
which literally says that the size of the result vector is the sum of the sizes of the argument vectors. The constraint is spelled out
patently, as part of the type ofbe arbitrarily large decimal numbers: for example, the following expression demonstrates the concatenation of a vector of 25 elements and a vector of size 979:
*ArbArithmT> :t vappend (vec (D2$D5 Sz) 0) (vec (D9$D7$D9 Sz) 0) (Num a) => Vec (D1 (D0 (D0 (D4 Sz)))) a
Blume01 as an unattainable wish.
vhead:: CardSum (D1 Sz) size1 size => Vec size a > Vec (D1 Sz) a vhead va = listVec (D1 Sz) $ [head (velems va)] vtail:: CardSum (D1 Sz) size1 size => Vec size a > Vec size1 a vtail va = result where result = listVec (vlength_t result) $ tail (velems va)
function result, the function is not divergent and not
recursive. Recall thatessentially specifies an inequality constraint: the input vector is nonempty. The constraint is expressed via an implicitly
existentially quantified variablesize of the input vector.
We can now run a few examples. We note that the compiler could correctly infer the type of the result, which includes the size of the vector after appending or truncating it.
*ArbArithmT> let v = vappend (vec (D9 Sz) 0) (vec (D1 Sz) 1) *ArbArithmT> :t v Vec (D1 (D0 Sz)) Integer *ArbArithmT> v Vec (array (0,9) [(0,0),(1,0),...,(8,0),(9,1)]) *ArbArithmT> :type vhead v Vec (D1 Sz) Integer *ArbArithmT> :type vtail v Vec (D9 Sz) Integer *ArbArithmT> vtail v Vec (array (0,8) [(0,0),(1,0),...,(7,0),(8,1)]) *ArbArithmT> :type (vappend (vhead v) (vtail v)) Vec (D1 (D0 Sz)) Integer
nonempty argument vector constraint. Indeed, an attempt to apply
*ArbArithmT> vtail (vec Sz 0) <interactive>:1:0: No instances for (DigitsInReverse' c2' Sz c2r', DigitsInReverse' c2r' Sz c2', DigitsDif (D1 Sz) c2r' Carry0 Sz, DigitsSum (D1 Sz) c2r Carry0 Sz, DigitsInReverse' c2r Sz size1, DigitsInReverse' size1 Sz c2r) arising from use of `vtail' at <interactive>:1:04
The error message essentially says that there is no such decimal
typeholds. That is, there is no nonnegative number that gives zero if added to one.
We can form quite complex expressions from the functionscompiler will infer and verify the corresponding constraints on the sizes of involved vectors. For example:
testc1 = let va = vec (D1$D2 Sz) 0 vb = vec (D5 Sz) 1 vc = vec (D8 Sz) 2 in vzipWith (+) va (vappend vb (vtail vc)) *ArbArithmT> testc1 Vec (array (0,11) [(0,1),...,(4,1),(5,2),(6,2),...,(11,2)])
inferred this nontrivial constraint and checked it. Indeed, if we by
mistake writewriting the example, the compiler will instantly report a type error:
Couldn't match `D9 Sz' against `D8 Sz' Expected type: D9 Sz Inferred type: D8 Sz When using functional dependencies to combine DigitsSum (D1 Sz) c2r Carry0 (D9 Sz), arising from use of `vtail' at ArbArithmT.hs:420:3438 DigitsSum (D1 Sz) c2r Carry0 (D8 Sz), arising from use of `vtail' at ArbArithmT.hs:411:3438
We can define other operations that extend or shrink our vectors. For example, Section sec:unarytype introduced
the operatoreasier. It is straightforward to implement such an operator for decimallytyped vectors.
We must point out that the type system guarantees thatvectors. Therefore, we no longer need the corresponding runtime
check. The bodies ofof the code without compromising its safety.
3.7 Staticallysized vectors in a dynamic context
In the present version of the paper, we demonstrate the simplest method of handling numberparameterized vectors in the dynamic context. The method involves runtime checks. The successful result of a runtime check is marked with the appropriate static type. Further computations can therefore rely on the result of the check (e.g., that the vector in question definitely has a particular size) and avoid the need to do that test over and over again. The net advantage is the reduction in the number of runtime checks. The complete elimination of the runtime checks is quite difficult (in general, may not even be possible) and ultimately requires a dependent type system.
For our presentation we use an example of dynamicallysized vectors: reversing a vector by the familiar accumulatorpassing algorithm. Each iteration splits the source vector into the head and the tail, and prepends the head to the accumulator. The sizes of the vectors change in the course of the computation, to be precise, on each iteration. We treat vectors as if they were lists. Most of the vector processing code does not have such a degree of variation in vector sizes. The code is quite simple:
vreverse v = listVec (vlength_t v) $ reverse $ velems v
whose inferred type is obviously
*ArbArithmT> :t vreverse vreverse :: (Card size) => Vec size a > Vec size a
of the input vector. We do this test only once, at the conclusion of the algorithm. We can treat the result as any other numberparameterized vector, for example:
testv = let v = vappend (vec (D3 Sz) 1) (vec (D1 Sz) 4) vr = vreverse v in vhead (vtail (vtail vr))
without any further runtime size checks.
3.8 Related work
This paper was inspired by Matthias Blume’s messages on the newsgroup comp.lang.functional in February 2002. Many ideas of this paper were first developed during the USENET discussion, and posted in a series of three messages at that time. In more detail Matthias Blume described his method in Blume01, although that paper uses binary rather than decimal types of array sizes for clarity. The approaches by Matthias Blume and ours both rely on phantom types to encode additional information about a value (e.g., the size of an array) in a manner suitable for a typechecker. The paper exhibits the most pervasive and thorough use of phantom types: to represent the size of arrays and the constness of imported C values, to encode C structure tag names and C function prototypes.
However, paper was written in the context of SML, whereas we use Haskell. The language has greatly influenced the method of specifying and enforcing complex static constraints, e.g., that digit sequences representing nonnegative numbers must not have leading zeros. The SML approach in Blume01 relies on the sophisticated module system of SML to restrict the availability of value constructors so that users cannot build values of outlawed types. Haskell typeclasses on the other hand can directly express the constraint, as we saw in Section sec:decimalarb. Furthermore, Haskell typeclasses let us specify arithmetic equality and inequality constraints — which, as admitted in Blume01, seems quite unlikely to be possible in SML.
Arrays of a statically known size — whose size is a part of their type — are a fairly popular feature in programming languages. Such arrays are present in Fortran, Pascal, C <ref>C does permit truly staticallysized arrays like those in Pascal. To achieve this, we should make a C array a member of a C structure. The compiler preserves the array size information when passing such a wrapped array as an argument. It is even possible to assign such “arrays”.</ref>. Pascal has the most complete realization of statically sized arrays. A Pascal compiler can therefore typecheck array functions like
ourexpressiveness and efficiency: for example, in Pascal we can copy one instance of an array into another instance of the same type by a single assignment, which, for small arrays, can be fully inlined by the compiler into a sequential code with no loops or range checks. However, in a language without the parametric polymorphism statically sized arrays are a great nuisance. If the size of an array is a part of its type, we cannot write generic functions that operate on arrays of any size. We can only write functions dealing with arrays of specific, fixed sizes. The inability to build generic arrayprocessing libraries is one of the most serious drawbacks of Pascal. Therefore, Fortran and C introduce “generic” arrays whose size type is not statically known. The compiler silently converts a staticallysized array into a generic one when passing arrays as arguments to functions. We can now build generic arrayprocessing libraries. We still need to know the size of the array. In Fortran and C, the programmer must arrange for passing the size information to a function in some other way, e.g., via an additional argument, global variable, etc. It becomes then the responsibility of a programmer to make sure that the size information is correct. The large number of Internet security advisories related to buffer overflows and other arraymanagement issues testify that programmers in general are not to be relied upon for correctly passing and using the array size information. Furthermore, the silent, irreversible conversion of statically sized arrays into generic ones negate all the benefits of the former.
A different approach to array processing is a socalled shapeinvariant programming, which is a key feature of arrayoriented languages such as APL or SaC. These languages let a programmer define operations that can be applied to arrays of arbitrary shape/dimensionality. The code becomes shorter and free from explicit iterations, and thus more reusable, easier to read and to write. The exact shape of an array has to be known, eventually. Determining it at runtime is greatly inefficient. Therefore, highperformance arrayoriented languages employ shape inference Scholz01, which tries to statically infer the dimensionalities or even exact sizes of all arrays in a program. Shape inference is, in general, undecidable, since arrays may be dynamically allocated. Therefore, one can either restrict the class of acceptable shapeinvariant programs to a decidable subset, resort to a dependenttype language like Cayenne, or use “soft typing”. The latter approach is described in Scholz01, which introduces a nonunique type system based on a hierarchy of array types: from fully specialized ones with the statically known sizes and dimensionality, to a type of an array with the known dimensionality but not size, to a fully generic array type whose shape can only be determined at runtime. The system remains decidable because at any time the typechecker can throw up hands and give to a value a fully generic array type. Shape inference of SaC is specific to that language, whose type system is otherwise deliberately constrained: SaC lacks parametric polymorphism and higherorder functions. Using shape inference for compilation of shapeinvariant array operations into a highly efficient code is presented in Kreye. Their compiler tries to generate as precise shapespecific code as possible. When the shape inference fails to give the exact sizes or dimensionalities, the compiler emits code for a dynamic shape dispatch and generic loops.
There is however a great difference in goals and implementation between the shape inference of SaC and our approach. The former aims at accepting more programs than can statically be inferred shapecorrect. We strive to express assertions about the array sizes and enforcing the programming style that assures them. We have shown
the definitions of functions such asargument and the result vectors are all of the same size. This constraint is assured at compiletime — even if we do not statically know the exact sizes of the vectors. Because SaC lacks parametric polymorphism, it cannot express such an assertion and statically
verify it. If a SaC programmer applies a function such asthat as an error but will compile a generic array code instead. The error will be raised at run time during a range check.
The approach of the present paper comes close to emulating a dependent type system, of which Cayenne is the epitome. We were particularly influenced by a practical dependent type system of Hongwei Xi Xi98 XiThesis, which is a conservative extension of SML. In Xi98, Hongwei Xi et al. demonstrated an application of their system to the elimination of array bound checking and list tag checking. The related work section of that paper lists a number of other dependent and pseudodependent type systems. Using the type system to avoid unnecessary runtime checks is a goal of the present paper too.
C++ templates provide parametric polymorphism and indexing of types by true integers. A C++ programmer can therefore define
functions likeequality and even arithmetic constraints on the sizes of the argument vectors. Blitz++ was the first example of using a socalled template metaprogramming for generating efficient and safe array code. The type system of C++ however presents innumerable hurdles to the functional style. For example, the result type of a function is not used for the overloading resolution, which significantly restricts the power of the type inference. Templates were introduced in C++ ad hoc, and therefore, are not well integrated with its type system. Violations of static constraints expressed via templates result in error messages so voluminous as to become incomprehensible.
McBride gives an extensive survey of the emulation of dependent type systems in Haskell. He also describes numberparameterized arrays that are similar to the ones discussed in Section sec:Okasaki. The paper by Fridlender and Indrika shows another example of emulating dependent types within the HindleyMilner type system: namely, emulating
variablearity functions such as generictechnique relies on ad hoc codings for natural numbers which resemble Peano numerals. They aim at defining more functions (i.e., multivariate functions), whereas we are concerned with making functions more restrictive by expressing sophisticated invariants in functions’ types. Another approach to multivariate functions — multivariate composition operator — is discussed in mcomp.
3.9 Conclusions
Throughout this paper we have demonstrated several realizations of numberparameterized types in Haskell, using arrays parameterized by their size as an example. We have concentrated on techniques that rely on phantom types to encode the size information in the type of the array value. We have built a family of infinite types so that different values of the vector size can have their own distinct type. That type is a decimal encoding of the corresponding integer (rather than the more common unary, Peanolike encoding). The examples throughout the paper illustrate that the decimal notation for the numberparameterized vectors makes our approach practical.
We have used the phantom size types to express nontrivial constraints on the sizes of the argument and the result arrays in the type of functions. The constraints include the size equality, e.g., the type of a function of two arguments may indicate that the arguments must be vectors of the same size. More importantly, we can specify arithmetical constraints: e.g., that the size of the vector after concatenation is the sum of the source vector sizes. Furthermore, we can write inequality constraints by means of an implicit existential quantification, e.g., the function
programmer should benefit from more expressive function signatures and from the ability of the compiler to statically check complex invariants in all applications of the vectorprocessing functions. The compiler indeed infers and checks nontrivial constraints involving addition and subtraction of sizes — and presents readable error messages on violation of the constraints.
4 References
Augustsson, L. Cayenne — a language with dependent types. Proc. ACM SIGPLAN International Conference on Functional Programming, pp. 239—250, 1998.
Matthias Blume: NoLongerForeign: Teaching an ML compiler to speak C “natively.” In BABEL’01: First workshop on multilanguage infrastructure and interoperability, September 2001, Firenze, Italy. [1]
The complete source code for the article. August 9, 2005. [2]
Daniel Fridlender and Mia Indrika: Do we Need Dependent Types? BRICS Report Series RS0110, March 2001. [3]
Oleg Kiselyov: Polyvariadic composition. October 31, 2003. [4]
Oleg Kiselyov: Polymorphic stanamically balanced AVL trees. April 26, 2003. [5]
Dietmar Kreye: A Compilation Scheme for a Hierarchy of Array Types. Proc. 3th International Workshop on Implementation of Functional Languages (IFL’01).
Conor McBride: Faking it — simulating dependent types in Haskell. Journal of Functional Programming, 2002, v.12, pp. 375392 [6]
Chris Okasaki: From fast exponentiation to square matrices: An adventure in types. Proc. fourth ACM SIGPLAN International Conference on Functional Programming (ICFP ’99), Paris, France, September 2729, pp. 28  35, 1999 [7]
SvenBodo Scholz: A Type System for Inferring Array Shapes. Proc. 3th International Workshop on Implementation of Functional Languages (IFL’01). [8]
SingleAssignment C homepage. [9]
Dominic Steinitz: Re: Polymorphic Recursion / Rank2 Confusion. Message posted on the Haskell mailing list on Sep 21 2003. [10]
Todd L. Veldhuizen: Arrays in Blitz++. Proc. 2nd International Scientific Computing in ObjectOriented Parallel Environments (ISCOPE’98). Santa Fe, New Mexico, 1998. [11]
Hongwei Xi, Frank Pfenning: Eliminating Array Bound Checking Through Dependent Types. Proc. ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 249—257, 1998. [12]
Hongwei Xi: Dependent Types in Practical Programming. Ph.D thesis, Carnegie Mellon University, September 1998. [13]
<references/>
CategoryCategory CategoryArticle