\documentclass{sig-alt-full}
% Fix bugs in sig-alternate.cls
\makeatletter
\def\@@sect#1#2#3#4#5#6[#7]#8{%
\ifnum #2>\c@@secnumdepth
\let\@@svsec\@@empty
\else
\refstepcounter{#1}%
\edef\@@svsec{%
\begingroup
%\ifnum#2>2 \noexpand\rm \fi % changed to next 29 July 2002 gkmt
\ifnum#2>2 \noexpand#6 \fi
\csname the#1\endcsname
\endgroup
\ifnum #2=1\relax .\fi
\hskip 1em
}%
\fi
\@@tempskipa #5\relax
\ifdim \@@tempskipa>\z@@
\begingroup
#6\relax
\@@hangfrom{\hskip #3\relax\@@svsec}%
\begingroup
\interlinepenalty \@@M
\if@@uchead
\uppercase{#8}%
\else
#8%
\fi
\par
\endgroup
\endgroup
\csname #1mark\endcsname{#7}%
%\vskip -12pt %gkmt, 11 aug 99 and GM July 2000 (was -14) - numbered section head spacing
\addcontentsline{toc}{#1}{%
\ifnum #2>\c@@secnumdepth \else
\protect\numberline{\csname the#1\endcsname}%
\fi
#7%
}%
\else
\def\@@svsechd{%
#6%
\hskip #3\relax
\@@svsec
\if@@uchead
\uppercase{#8}%
\else
#8%
\fi
\csname #1mark\endcsname{#7}%
\addcontentsline{toc}{#1}{%
\ifnum #2>\c@@secnumdepth \else
\protect\numberline{\csname the#1\endcsname}%
\fi
#7%
}%
}%
\fi
\@@xsect{#5}%\hskip 1pt
\par
}
%TODO: spell-check
\setcounter{errorcontextlines}{200}
%include lhs2TeX.fmt
%include lhs2TeX.sty
%subst code a = "\unskip\begingroup\parskip\abovedisplayskip\csname @@par\endcsname\noindent\advance\leftskip\mathindent\('n\begin{pboxed}\SaveRestoreHook'n" a "\ColumnHook'n\end{pboxed}'n\)\parskip\belowdisplayskip\csname @@par\endcsname\noindent\endgroup\resethooks'n"
%subst string a = "\text{``{}" a "{}''''}"
%format * = "\times "
%format ; = ";\ "
%format , = ",\:"
%format __ = undefined
%format forall a = "\Forall " a
%format . = "\circ "
%format ? = "\mathopen?"
%format s1
%format s2
%format a1
%format a2
%format b1
%format b2
%format test1
%format test2
%format test3
%format test3'
%format sort1
%format sort2
%format Label1
%format Label2
\def\Forall#1\circ{\forall#1.\:}
\usepackage{txfonts}
\usepackage[T1]{fontenc}
\usepackage[sort&compress]{natbib1}
\makeatletter \let\@@biblabel\@@empty \makeatother
\providecommand\newblock{}
\renewcommand\bibsection{\section{References}}
\newcommand\bibfont{\scriptsize}
\bibpunct{[}{]}{,}{n}{}{,}
\usepackage{hyphenat}
\usepackage{comment}
\usepackage{amsmath}
\usepackage{amstext}
\usepackage{url}
\usepackage{refrange}
\usepackage{ifpdf}
\ifpdf
\pdfpageheight=11in
\pdfpagewidth=8.5in
\fi
\usepackage{fancyvrb}
\DefineVerbatimEnvironment{java}{Verbatim}{xleftmargin=\mathindent}
\setlength{\parskip}{0pt}
\setlength{\mathindent}{1em}
\begin{document}
\expandafter\ifx\csname thisTR\endcsname\relax
\newcommand{\thisTR}{this technical report}
\newcommand{\ofthisTR}{}
\permission{An appendectomized version of this Harvard University technical
report is published in the proceedings of the 2004 Haskell Workshop
\citep{proc}.}
\global\copyrightetc{}
\else
\conferenceinfo{Haskell'04,} {September 22, 2004, Snowbird, Utah, USA.}
\CopyrightYear{2004}
\crdata{1-58113-850-4/04/0009}
\fi
% Reduce display spacing
\divide\abovedisplayskip 2
\divide\belowdisplayskip 2
\divide\abovedisplayshortskip 2
\divide\belowdisplayshortskip 2
% Reduce list spacing
\makeatletter
\renewcommand\@@listI{\leftmargin\leftmargini
\parsep \z@@
\topsep 3\p@@ \@@plus\p@@ \@@minus 2\p@@
\itemsep 2\p@@ \@@plus\p@@ \@@minus\p@@}
\let\@@listi\@@listI
\@@listi
\makeatother
\title{Functional Pearl: Implicit Configurations}
\subtitle{---or, Type Classes Reflect the Values of Types}
\numberofauthors{2}
\author{%
\alignauthor Oleg Kiselyov\\
\affaddr{Fleet Numerical Meteorology}\\
\affaddr{and Oceanography Center}\\
\affaddr{Monterey, CA 93943, USA}\\
\email{oleg@@pobox.com}
\alignauthor Chung-chieh Shan\\
\affaddr{Division of Engineering and Applied}\\
\affaddr{Sciences, Harvard University}\\
\affaddr{Cambridge, MA 02138, USA}\\
\email{ccshan@@post.harvard.edu}}
\maketitle
\begin{abstract}
The \emph{configurations problem} is to propagate run-time preferences throughout
a program, allowing multiple concurrent configuration sets to coexist safely
under statically guaranteed separation. This problem is common in all software
systems, but particularly acute in Haskell, where currently the most popular
solution relies on unsafe operations and compiler pragmas.
We solve the configurations problem in Haskell using only stable and
widely implemented language features like the type-class system.
In our approach, a term expression can refer to run-time configuration
parameters as if they were compile-time
constants in global scope.
Besides supporting such intuitive term notation and statically guaranteeing separation,
our solution also helps improve the program's performance by transparently
dispatching to specialized code at run-time.
We can propagate any type of configuration data---numbers,
strings, |IO| actions, polymorphic functions, closures, and abstract data types.
No previous approach to propagating configurations implicitly in any language
provides the same static separation guarantees.
The enabling technique behind our solution is to propagate values via types,
with the help of polymorphic recursion and
higher-rank polymorphism. The technique essentially emulates
local type-class instance declarations while preserving coherence.
Configuration parameters are propagated throughout the code implicitly
as part of type inference rather than explicitly by the
programmer.
Our technique can be regarded as a
portable, coherent, and intuitive alternative to implicit parameters.
It motivates adding local instances to Haskell, with a restriction
that salvages principal types.
\end{abstract}
\begingroup
\def\section*#1{\par\smallskip\noindent\textbf{#1: }\ignorespaces}
\sloppy
\category{D.1.1}{Programming Techniques}{Applicative (Functional) Programming}
\category{D.3.2}{Language Classifications}{Haskell}
\category{D.3.3}{Programming Techniques}{Language Constructs and Features}[abstract data types; polymorphism; recursion]
\fussy
\terms Design, Languages
\keywords Type classes; implicit parameters; polymorphic recursion; higher-rank polymorphism; existential types
\endgroup
\begin{comment}
\begin{code}
{-# OPTIONS -fglasgow-exts #-}
module Prepose where
import System.IO.Unsafe (unsafePerformIO)
import Control.Exception (handle, handleJust, errorCalls)
import Foreign.Marshal.Utils (with, new)
import Foreign.Marshal.Array (peekArray, pokeArray)
import Foreign.Marshal.Alloc (alloca)
import Foreign.Ptr (Ptr, castPtr)
import Foreign.Storable (Storable(sizeOf, peek))
import Foreign.C.Types (CChar)
import Foreign.StablePtr (StablePtr, newStablePtr,
deRefStablePtr, freeStablePtr)
import Data.Bits (Bits(..))
import Prelude hiding (getLine)
\end{code}
\end{comment}
\section{Introduction}
Most programs depend on configuration parameters. For
example, a pretty-printing function needs to know the width of the page, modular
arithmetic depends on the modulus, numerical code heavily
depends on tolerances and rounding modes, and most end-user
applications depend on user preferences. Sometimes the parameters of
the computation are known when the code is written or compiled. Most
of the time, however, the parameters are initialized at the beginning of the
computation, such as read from a configuration file. Sometimes the parameters
stay the same throughout a program execution, but other times they need to be
re\hyp initialized. For example, numerical code
may need to be re\hyp executed with different rounding modes
\citep{kahan-java}. Also, a cryptography program may need to perform modular arithmetic with various
moduli. Library code especially should support \emph{multiple}
sets of parameters that are simultaneously in use, possibly in different threads.
We refer to the problem of setting and propagating preference parameters as the
\emph{configurations problem}. We use the term ``configurations'' in the plural
to emphasize that we aim to parameterize code at
run time for several concurrent sets of preferences.
A solution to the configurations problem should keep
configuration parameters out of the way: code that
uses no parameters should not require any change.
In particular, the programmer should not be forced to sequence the computation
(using a monad, say) when it is not otherwise needed. The
parameters should be statically typed and fast to access---ideally,
just like regular lexical variables.
Configuration
data should be allowed to become known only at run time. Moreover, different
configurations should be able to coexist. When different
configurations do coexist, the user should be statically prevented
from inadvertently mixing them up; such
subtle errors are easy to make when the first goal above (that
configuration parameters be implicit) is achieved.
The solution should be available on existing
programming language systems.
Given how pervasive the
configurations problem is, it is not surprising that the topic provokes repeated
discussions in mailing lists \citep{adriano-need,hu-dealing,russell-initialisation},
conferences \citep{lewis-implicit}, and journals \citep{hughes-global}. As these
discussions conclude, no previous solution is entirely satisfactory.
Historically, the configurations problem is ``solved'' with mutable global
variables or dynamically-scoped variables. Neither solution is
satisfactory, because concurrent sets of parameters are hard to support reliably,
be the language pure or impure, functional or imperative. Furthermore,
in a pure functional language like Haskell, mutable global variables are either
unwieldy (all code is written in monadic style) or unsafe
(|unsafePerformIO| is used).
Another common solution is to store
configuration data in a globally accessible \emph{registry}. That
approach suffers from run-time overhead and often the
loss of static typing.
Finally, one type-safe and pure approach is to place all configuration data into
a record and pass it from one function to another. However, it is unappealing
to do so explicitly throughout the whole program, not the least because managing
concurrent sets of parameters is error-prone.
\emph{Implicit parameters} \citep{lewis-implicit}
are a proposal to extend Haskell with dynamically-scoped
variables like LISP's \citep{queinnec-lisp}.
As a solution to the configurations problem, implicit parameters inherit from
dynamically\hyp scoped variables the difficulty of supporting concurrent sets of
parameters: they
interact unintuitively with other parts of Haskell \citep{peyton-jones-implicit}
and easily lead to quite subtle
errors \citep{hughes-global}, whether or not
the monomorphism restriction is abolished.
As \citet{peyton-jones-implicit} puts it,
``it's really not clear what is the right thing to do.''
In this paper, we present a solution to the configurations problem
in Haskell that meets all the requirements enumerated above.
We rely on type classes, higher-rank polymorphism, and---in
advanced cases---the foreign function interface. These
are all well\hyp documented and widely\hyp implemented Haskell
extensions, for instance in Hugs and in the Glasgow Haskell Compiler.
The notation is truly intuitive; for example, the term
\begin{spec}
foo :: (Integral a, Modular s a) => M s a
foo = 1000*1000*5 + 2000
\end{spec}
expresses a modular computation in which \emph{each} addition and multiplication
is performed modulo a modulus. The type signature here\footnote
{This type signature is required.
We argue at the end of Section~\ref{s:notation} that this is an advantage.}
describes a polymorphic ``modulus\hyp bearing number'' of type |M s a|.
As we detail in Section~\ref{s:modular}, the type-class constraints
require that the type~|a| be an |Integral| type (such as |Int|),
and that the type~|s| carry configuration
data for |Modular| arithmetic on~|a|.
The modulus is supplied at run time, for example:
\begin{spec}
withIntegralModulus' 1280 foo
\end{spec}
The same computation can be re-executed with different moduli:
\begin{spec}
[ withIntegralModulus' m foo | m <- [1..100] ]
\end{spec}
We take advantage of the compiler's existing, automatic type inference
to propagate configuration data as type-class constraints.
Thus the type annotations that are sometimes needed are infrequent
and mostly attached to top-level definitions.
Type inference also affords the programmer the flexibility to
choose the most convenient way to pass
configuration data: take an argument whose type mentions~|s|;
return a result whose type mentions~|s| (as |foo| above does), and let
unification propagate the type information in the opposite direction
of data flow; or even propagate configuration data from one argument
of a function to another, by unifying their types.
This flexibility reflects the fact that the compile-time flow
of configuration types need not follow the
run-time flow of configuration values.
Our technique handles not only ``conventional''
parameters, like numbers and strings, but any Haskell value,
including polymorphic functions and abstract data types. We let
configuration data include functions tuned to run-time
input, such as faster modular\hyp arithmetic functions that
exist for composite moduli \citep{koren-computer,parhami-computer,soderstrand-residue}. For another example, we can treat an array
lookup function as a configuration parameter, and selectively disable
bounds\hyp checking where we have
verified already that array indices are in bounds. In general, we can
treat global imports like the Prelude as configuration data, so that
different pieces of code can ``import their own specialized Prelude''.
The basic idea behind our approach is not new. \Citet{thurston-modular}
independently discovered and used our technique for modular
arithmetic. Our contribution here is not just to introduce
\citeauthor{thurston-modular}'s technique to a broader audience, but also to
extend it to the general configurations problem at any type, beyond integers.
We achieve more intuitive notation, as shown above, as well as
better performance by specializing code at run-time.
Along the way, we survey existing attempts at solving the
configurations problem. For multiple configurations, our solution is more
portable, coherent, and intuitive than implicit parameters.
Finally, our technique effectively declares local type-class instances, which
prompts us to sketch an extension to Haskell.
This paper is organized as follows. In Section~\ref{s:problem}, we
discuss the configurations problem and survey previous attempts at solving it.
We demonstrate why these attempts are unsatisfactory and
illustrate how acute the problem is if otherwise pure functional programmers are
willing to resort to operations with no safety guarantee.
Section~\ref{s:modular} introduces the running example of modular arithmetic.
This example calls for the peaceful coexistence and static separation of several
concurrent configurations.
Section~\ref{s:reify} develops our solution in three stages: passing integers;
passing serializable data types, including floating-point numbers and strings;
and finally, passing any type, including functional and abstract values. In
Section~\ref{s:more} we present two real-world examples to demonstrate that our
solution scales to multiple parameters and helps the programmer write fast code with intuitive notation.
Our solution improves over the OpenSSL cryptography library, where the lack of
static separation guarantees seems to have stunted development.
In Section~\ref{s:related}, we compare our solution to previous work,
especially \citearound{'s implicit
parameters}\citet{lewis-implicit}. We argue for
adding local type-class instances to Haskell and sketch how. We then
conclude in Section~\ref{s:conclusions}.
\section{The Configurations Problem}
\label{s:problem}
A Haskell program is a collection of definitions, which are rarely
closed. For example,
\begin{spec}
result approx = last $ take maxIter $ iterate approx (pi/2)
\end{spec}
is an open definition: |last|, |take|, |iterate|, |pi|, and |maxIter|
are defined elsewhere. The values associated with these symbols are
known at compile time. Such a static association is proper for
|pi|, which is truly a constant. However, |maxIter| is more of a user
preference. A user may reasonably wish to run the program for
different values of |maxIter|, without recompiling the
code. Unfortunately, if the value of |maxIter| is to be read from a
configuration file at the beginning of the computation,
or may change from run to run of |result|, it seems that we can no
longer refer to |maxIter| as neatly as above.
The \emph{configurations problem} is to make run-time
user preferences available throughout a program.
As ``configurations'' in the plural shows, we aim to support
concurrent sets of preferences and keep
them from being accidentally mixed.
The sets of preferences should stay out of the way, yet it should be clear to
both the programmer and the compiler which set is used where.
(We discuss the latter \emph{coherence} requirement in Section~\ref{s:related}.)
In this general formulation, the
problem is an instance of run-time code parameterization.
The configurations problem is pervasive and acute, as
evidenced by recurrent discussions on the Haskell
mailing list \citep{adriano-need,hu-dealing,russell-initialisation}. It is often pointed out, for example, that
numerical code typically depends on a multitude of parameters like
|maxIter|: tolerances, initial approximations, and so on. Similarly, most
end-user applications support some customization.
The existing approaches to the configurations problem can be summarized as
follows \citep{hughes-global,adriano-need}.
The most obvious solution is to pass all needed parameters explicitly as
function arguments. For example:
\begin{spec}
result maxIter approx =
last $ take maxIter $ iterate approx (pi/2)
\end{spec}
An obvious drawback of this solution is that many computations depend
on many parameters, and passing a multitude of positional arguments
is error-prone. A more subtle problem is that,
if there are several sets of configuration data (as in Section~\ref{s:phantom}),
it is easy to make a mistake and pass parameters of the wrong set deep
within the code. The mix-up cannot be detected or prevented
statically.
The second solution is to group all the parameters in a single Haskell
record with many fields, and pass it throughout the code:
\begin{spec}
data ConfigRecord = ConfigRecord
{ maxIter:: Int, tolerance::Float {-"\dotsc"-} }
result conf approx =
last $ take (maxIter conf) $ iterate approx (pi/2)
\end{spec}
This approach effectively turns the configuration parameters from
positional arguments to keyword arguments. This way, the functions are easier
to invoke and have tidier signatures. However, to refer to a configuration
parameter, we have to write the more verbose |maxIter conf|. Moreover, we still
have to pass the configuration record explicitly from function to function. Therefore, there is still a
danger of passing the wrong record in the middle of the code when
several configuration records are in scope.
The same criticism applies to the analogous approach of passing configuration
data in first-class objects or modules in the ML language family.
The third approach, advocated with some reluctance by \citet{hughes-global}, is to
use implicit parameters \citep{lewis-implicit}. As the name implies, implicit
parameters do not need to be passed explicitly among functions
that use them. Unfortunately, implicit parameters disturbingly weaken the
equational theory of the language: a piece of code may behave differently if we
add or remove a type signature, or even just perform a $\beta$- or $\eta$\hyp
expansion or reduction. We compare implicit parameters
to our approach in more detail in Section~\ref{s:implicit-parameters}.
The fourth approach to the configurations problem is to use a reader monad
\citep{bromage-dealing}. Its drawback is that any code that uses configuration
data (even only indirectly, by calling other functions that do) must be
sequenced into monadic style---even if it does not otherwise have to be.
Alternatively, we may use mutable reference cells (|IORef|) in conjunction
with the |IO| monad. This method obviously emulates mutable global
variables, which are often used to store configuration data in
impure languages. If our program uses multiple configurations,
we may need to mutate the global variables in the middle of the
computation, which, as is well-known in imperative languages, is greatly
error-prone. Because |IORef| calls for the |IO| monad, using |IORef|
for configuration data requires either the tedium of coding in monadic style
all the time or the unsoundness of using |unsafePerformIO|
\citep{claessen-dealing}. Regrettably, the most popular solution to the
configurations problem in Haskell seems to be the latter: issue compiler pragmas to disable inlining and
common subexpression elimination, invoke |unsafePerformIO|, and pray
\citep{hu-dealing,hughes-global}.
A fifth approach is to generate code at run time, after the necessary
configuration data is known \citep{kiselyov-dealing}. At that time, |maxIter|
above can be treated just like~|pi|: as a compile-time constant. This approach
has the drawback that a compiler and a linker enter the footprint of the
run-time system, and can become a performance bottleneck. Moreover, it is
harder for program components using different sets of configuration data
to communicate.
A final possible solution to the configurations problem is to turn global
definitions into local ones:
\begin{spec}
topLevel maxIter tolerance epsilon {-"\dotsc"-} = main where
main = {-"\dotsb"-}
{-"\text\dots"-}
result approx = last $ take maxIter $ iterate approx (pi/2)
\end{spec}
Most of the code above is local inside
|topLevel|. We pass parameters explicitly to
that function only. Within a local definition like |result|, the
configuration parameters are in scope, do not have to be passed
around, and can be used just by mentioning their names. Furthermore,
to use different sets of configuration
data, we merely invoke |topLevel| with different arguments. We
are statically assured that computations with different
configuration data cannot get mixed up. The solution seems ideal---except
putting all code within one giant function completely
destroys modularity and reuse.
In the following sections, we show how to attain all the benefits
of the last approach with modular code arranged in top-level
definitions. Our type-class constraints, like |Modular s a| in
the introduction,
can be thought of as top-level labels for local scopes.
\section{Motivating Example:\\ Modular Arithmetic}
\label{s:modular}
\emph{Modular arithmetic} is arithmetic in which numbers that differ by
multiples of a given \emph{modulus} are treated as identical: $2
+ 3 = 1 \pmod{4}$ because $2 + 3$ and $1$ differ by a multiple of~$4$. Many
applications, such as modern cryptography, use modular arithmetic with multiple
moduli determined at run time. To simplify these computations, we can define
functions in Haskell like
\begin{spec}
add :: Integral a => a -> a -> a -> a
add m a b = mod (a + b) m
mul :: Integral a => a -> a -> a -> a
mul m a b = mod (a * b) m
\end{spec}
(where |mod| is a member function of the |Integral| type class in the Prelude)
so we can write
\begin{spec}
test1 m a b = add m (mul m a a) (mul m b b)
\end{spec}
to compute |a*a + b*b| modulo~|m|. The modulus~|m| is the parameter of these
computations, which is passed explicitly in the above examples, and which we
want to pass implicitly. Like |test1| above, many cryptographic
routines perform long sequences of arithmetic operations with the same modulus.
Since the parameter |m| is passed explicitly in |test1| above, it is easy
to make a mistake and write, for example, |add m' (mul m a a) (mul m b b)|,
where |m'| is some other integral variable in scope.
As the first step towards making the modulus parameter implicit, let us make sure
that sequences of modular operations like |test1| indeed all use the
same modulus.
\subsection{Phantom Types for Parameter Threads}
\label{s:phantom}
Our first subgoal, then, is to statically guarantee that a sequence
of modular operations is executed with the same modulus.
\Citets{launchbury-lazy,launchbury-state} |ST| monad for state
threads in Haskell uses a type parameter~|s| to keep track of
the state thread in which each computation takes place.
Similarly, we use a type parameter~|s|
to keep track of the modulus used for each computation.
However, because this piece of state is fixed over the course of the
computation, we do not force the programmer to sequence the computation
by writing in monadic or continuation\hyp passing style.
\begin{code}
newtype Modulus s a = Modulus a deriving (Eq, Show)
newtype M s a = M a deriving (Eq, Show)
add :: Integral a => Modulus s a -> M s a -> M s a -> M s a
add (Modulus m) (M a) (M b) = M (mod (a + b) m)
mul :: Integral a => Modulus s a -> M s a -> M s a -> M s a
mul (Modulus m) (M a) (M b) = M (mod (a * b) m)
\end{code}
Also, we need the function |unM| to give us the number back from the
wrapped data type |M s a|.
\begin{code}
unM :: M s a -> a
unM (M a) = a
\end{code}
The type parameter~|s| is \emph{phantom}. That is, it has no term
representation: the parameter~|s| occurs only in type expressions
without affecting term expressions. The expression |test1| remains the
same, but it now has a different type:
\begin{spec}
test1 :: Integral a => Modulus s a -> M s a -> M s a -> M s a
\end{spec}
The argument and result types of |add| and |mul| share the same type
variable~|s|. During type checking, the compiler automatically propagates this
type information to infer the above type for |test1|. As with the |ST| monad,
the type parameter~|s| is threaded, but unlike with the |ST| monad, the
term-level expression is not sequenced monadically. Hence the compiler knows that the
subexpressions |mul m a a| and |mul m b b| of |test1| can be computed in any
order.
We can now existentially quantify over the type variable~|s| to distinguish
among different moduli at the type level and make sure that a series of modular operations is performed with
the same modulus.
\begin{code}
data AnyModulus a = forall s. AnyModulus (Modulus s a)
makeModulus :: a -> AnyModulus a
makeModulus a = AnyModulus (Modulus a)
\end{code}
This |makeModulus| function is typically used as follows.
\begin{spec}
case makeModulus 4 of
AnyModulus m ->
let a = M 3; b = M 5 in
unM $ add m (mul m a a) (mul m b b)
\end{spec} % $
In the case alternative |case makeModulus 4 of AnyModulus m ->|,
the type variable~|s| is existentially quantified. The compiler will therefore make
sure that |s| does not ``leak''---that is, accidentally unify with other
quantified type variables or types. Because |s| is threaded through the type of
|add| and |mul|, all modular operations in the argument to |unM|
are guaranteed to execute with the same~|s|, that is, with the
same modulus.
There is a redundancy, though: the data constructor |AnyModulus|
is applied in |makeModulus|, then peeled off right away
in the case alternative. To eliminate this redundant packing and
unpacking, we apply a continuation\hyp passing\hyp style transform
to turn the existential type in |makeModulus| into a rank-2 polymorphic type:
\begin{spec}
withModulus :: a -> (forall s. Modulus s a -> w) -> w
withModulus m k = k (Modulus m)
\end{spec}
\begin{comment}
\begin{code}
withModulus'' :: a -> (forall s. Modulus s a -> w) -> w
withModulus'' m k = k (Modulus m)
\end{code}
\end{comment}
The |withModulus| function is more usable than |makeModulus|,
because it avoids the verbiage of unpacking data constructors.
We can now write
\begin{spec}
test2 = withModulus 4 (\m ->
let a = M 3; b = M 5 in
unM $ add m (mul m a a) (mul m b b))
\end{spec}
to get the result~$2$. If we by mistake try to mix %different
moduli and evaluate
\begin{spec}
withModulus 4 (\m ->
withModulus 7 (\m' ->
let a = M 3; b = M 5 in
unM $ add m' (mul m a a) (mul m b b)))
\end{spec}
we get a type error, as desired:
\begin{spec}
{-"\text{Inferred type is less polymorphic than expected}"-}
{-"\text{Quantified type variable }"-}s{-"\text{ escapes}"-}
{-"\text{It is mentioned in the environment: }"-}m :: Modulus s a
{-"\text{In the second argument of }"-}withModulus{-"\text{, namely }"-}(\ m' -> {-"\dotsb"-})
\end{spec}
\subsection{Type Classes for Modulus Passing}
\label{s:modularclass}
The second step in our development is to avoid explicitly mentioning
the modulus~|m| in terms. On one hand, in the term |test1|
above, every occurrence of |add| and |mul| uses
the same modulus value~|m|. On the other hand, in the type of |test1|
above, every instantiation of the type-schemes of |add| and |mul| uses
the same phantom type~|s|.
Given that the type checker enforces such similarity between |m| and~|s|
in appearance and function, one may wonder if we could
avoid explicitly mentioning~|m| by somehow associating it with~|s|.
The idea to \emph{associate a value with a type} is not
apocryphal, but quite easy to realize using Haskell's type-class facility.
If we constrain our type variable~|s| to range over
types of a specific type class, then the compiler will associate a class
dictionary with~|s|. Whenever |s| appears in the type of a term,
the corresponding dictionary is available.
We just need a slot in that dictionary for our modulus:
%
\begin{comment}
\begin{code}
__ = __
\end{code}
\end{comment}
\begin{code}
class Modular s a | s -> a where modulus :: s -> a
normalize :: (Modular s a, Integral a) => a -> M s a
normalize a :: M s a = M (mod a (modulus (__ :: s)))
\end{code}
%
The functional dependency |s->a| signifies the fact that the type~|s|
represents a value of at most one type~|a| \citep{jones-type}. As we shall see below, a
stronger invariant holds: each value of type~|a| is represented by
a (different) type~|s|.
For conciseness, the code uses lexically-scoped type variables
\citep{peyton-jones-lexically-scoped} in a non-essential way:\footnote
{This paper is written in literate Haskell and works in the Glasgow Haskell Compiler.
(The code is available alongside \thisTR.)
Not shown here is another version of the code that
avoids lexically-scoped type variables and (so) works in Hugs.}
in the left-hand side |normalize a :: M s a| above, the type |M s a| annotates
the result of |normalize| and binds the type variable~|s| in |__ :: s|
to the right of the equal sign.
Also, we
denote $\mathit{undefined}$ with |__|. One may be aghast at the
appearance of |__| in terms, but that appearance is only
symptomatic of the fact that the polymorphic function |modulus| does not need the
value of its argument. The type checker needs the \emph{type} of that
argument to choose the correct instance of the class |Modular|. Once
the instance is chosen, |modulus| returns the modulus value
stored in that class dictionary. Informally speaking, |modulus|
retrieves the value associated with the type~|s|.
If Haskell had a way to pass a type argument, we would have used it.
We can now avoid mentioning~|m| in |add|
and |mul|. This move makes these functions binary
rather than ternary, so we overload the ordinary arithmetic operators |+|
and~|*| for modular arithmetic, simply by defining an
instance of the class |Num| for our ``modulus\hyp bearing numbers'' |M s a|.
Modular arithmetic now becomes an instance of general
arithmetic, which is mathematically pleasing.
\begin{code}
instance (Modular s a, Integral a) => Num (M s a) where
M a + M b = normalize (a + b)
M a - M b = normalize (a - b)
M a * M b = normalize (a * b)
negate (M a) = normalize (negate a)
fromInteger i = normalize (fromInteger i)
signum = error "Modular numbers are not signed"
abs = error "Modular numbers are not signed"
\end{code}
It is thanks to signatures in the |Num| class that this code propagates the
modulus so effortlessly. For example, the arguments and result of~|+| share
the modulus because |Num| assigns |+| the type |M s a -> M s a -> M s a|. As we
will keep seeing, it is often natural to propagate parameters via types.
By contrast, if we think of |+| as taking two equal modulus \emph{terms} as
input, and passing that modulus on to |normalize|, then we might define |+|
much less simply:
\begin{spec}
(M a :: M s1 a) + (M b :: M s2 a) = normalize (a + b) :: M s1 a
where _ = [__::s1, __::s2] -- equate the two input moduli
\end{spec}
\begin{comment}
Note that |where _ :: s1 = __ :: s2| doesn't work: it just
binds a new, fresh type variable s1 that shadows the existing type
variable of the same name.
\begin{code}
aaa (M a :: M s1 a) (M b :: M s2 a) = normalize (a + b) :: M s1 a
where _ = [__::s1, __ :: s2] -- make sure input moduli are equal
\end{code}
\end{comment}
Anyway, it seems that we are done. We just need to redefine
the function |withModulus| to incorporate
our new type class |Modular|.
\begin{code}
withModulus :: a -> (forall s. Modular s a => s -> w) -> w
\end{code}
%
But here we encounter a stumbling block: how to actually implement
|withModulus|? Given a modulus value~|m| of type~|a| and a
polymorphic continuation~|k|, we need to pass to~|k| an instance of
|Modular s a| defined by |modulus s = m|, for some type~|s|. That is, we need to
construct an instance of the class |Modular| such that the function
|modulus| in that instance returns the desired value |m|. Constructing
such instances is easy when |m| is statically known:
\begin{spec}
m = 5
data Label
instance Modular Label Int where modulus _ = m
\end{spec}
\Citet{hughes-restricted} shows many practical examples of such
instances. But in our case, |m| is not statically
known. We want |withModulus| to manufacture a new instance, based on
the value of its first argument. One may wonder if this is even possible
in Haskell, given that instance declarations cannot appear in the
local scope of a definition and cannot be added at
run time.
Another way to look at our difficulty is from the point of
view of type-class dictionaries. The function |withModulus| must pass
to~|k| an implicit parameter, namely a dictionary for the type class
|Modulus|. This dictionary is not hard to construct---it just
contains the term |\s -> m|.
However, even though type classes have always been
explicated by translating them to dictionary passing
\citep{wadler-ad-hoc,hall-type}, Haskell does not expose dictionaries to the
programmer. In other words, Haskell does not let us explicitly pass an
argument for a double arrow |=>| (as in |Modular s a => {-"\dotsb"-}|), even though it is internally
translated to a single arrow |->| (as in |Modulus s a -> {-"\dotsb"-}|).
In the next section, we explain how to pass dictionary arguments using
some widely\hyp implemented extensions to Haskell. We build up this
capability in three stages:
\begin{enumerate}
\item We describe how to pass an integer as a dictionary argument. This
case handles the motivating example above: modular arithmetic over an
integral domain.
\item We use Haskell's foreign function interface to pass any type in the
|Storable| class as a dictionary argument. This case handles modular arithmetic
over a real (fractional) domain.
\item We take advantage of stable pointers in the foreign function interface to pass any type
whatsoever---even functions and abstract data types---as a dictionary
argument. This technique generalizes our approach to all configuration data.
\end{enumerate}
\section{Building Dictionaries by\\ Reflecting Types}
\label{s:reify}
Dictionaries at run time reflect context reductions at compile time,
in a shining instance of the Curry-Howard correspondence. To pass a
dictionary argument explicitly, then, we need to reify it as a type that
can in turn reflect back as the intended value.
\subsection{Reifying Integers}
\label{s:reify-integral}
We start by reifying integers. We build a family of
types such that each member of the family corresponds to a unique
integer. To encode integers in binary notation,
we introduce the type constant |Zero| and three
unary type constructors.
\begin{code}
data Zero; data Twice s; data Succ s; data Pred s
\end{code}
For example, the number~$5$, or $101$ in binary, corresponds to the
type |Succ (Twice (Twice (Succ Zero)))|.
This representation is
inspired by the way \citet{okasaki-fast} encodes the sizes of square
matrices. Our types, unlike \citeauthor{okasaki-fast}'s,
have no data constructors,
so they are only inhabited by the bottom value~|__|.
We are not interested in values of these types, only in the types
themselves.\footnote
{Like \citeauthor{okasaki-fast}, we include
|Twice| to perform reification and reflection in
time linear (rather than exponential) in the number of bits.
We also include |Pred| to encode negative numbers.
These two type
constructors make our type family larger than necessary:
an integer can be encoded in an infinite number of different ways.
For example, the number~$5$ also corresponds to the type |Succ (Succ (Succ
(Succ (Succ Zero))))|. We can easily use a different set of type constructors
to enforce a unique representation of integers (we elide
the code for brevity), but there is no need for the representation to be unique
in this paper, and the type constructors above are easier to understand.}
\begin{comment}
\begin{code}
class NumNat a
instance NumNat (Succ Zero)
instance NumNat a => NumNat (Succ (Twice a))
instance NumNat a => NumNat (Twice a)
class NumGood a
instance NumGood Zero
instance NumGood (Succ Zero)
instance NumNat a => NumGood (Succ (Twice a))
instance NumNat a => NumGood (Twice a)
instance NumNat a => NumGood (Pred a)
test_num:: NumGood a => a -> (); test_num _ = ()
data Positive s; data Negative s; data TwiceSucc s
class ReflectUnsigned s where reflectUnsigned :: Num a => s -> a
instance ReflectUnsigned Zero where
reflectUnsigned _ = 0
instance ReflectUnsigned s => ReflectUnsigned (Twice s) where
reflectUnsigned _ = reflectUnsigned (__ :: s) * 2
instance ReflectUnsigned s => ReflectUnsigned (TwiceSucc s) where
reflectUnsigned _ = reflectUnsigned (__ :: s) * 2 + 1
instance ReflectUnsigned s => ReflectNum (Positive s) where
reflectNum _ = reflectUnsigned (__ :: s)
instance ReflectUnsigned s => ReflectNum (Negative s) where
reflectNum _ = -1 - reflectUnsigned (__ :: s)
\end{code}
\end{comment}
We need to convert a type in our family to the
corresponding integer---and back. The first process---\emph{reflecting} a
type into the corresponding integer---is given by the class
|ReflectNum|:
\begin{code}
class ReflectNum s where reflectNum :: Num a => s -> a
instance ReflectNum Zero where
reflectNum _ = 0
instance ReflectNum s => ReflectNum (Twice s) where
reflectNum _ = reflectNum (__ :: s) * 2
instance ReflectNum s => ReflectNum (Succ s) where
reflectNum _ = reflectNum (__ :: s) + 1
instance ReflectNum s => ReflectNum (Pred s) where
reflectNum _ = reflectNum (__ :: s) - 1
\end{code}
%
The instances of the class
deconstruct the type and perform corresponding operations (doubling,
incrementing, and so on).
Again, we should not be afraid of~|__| in
terms. As the underscores show, the function |reflectNum| never examines the value of
its argument. We only need the type of the argument to choose the
instance. Informally speaking,
|reflectNum| ``maps types to values''.
The inverse of |reflectNum| is |reifyIntegral|, which turns a signed
integer into a type that represents the given number
in binary notation. In other words, the type says how to make the
given number by applying increment, decrement and double operations to
zero.
\begin{code}
reifyIntegral :: Integral a =>
a -> (forall s. ReflectNum s => s -> w) -> w
reifyIntegral i k = case quotRem i 2 of
(0, 0) -> k (__ :: Zero)
(j, 0) -> reifyIntegral j (\(_ :: s) -> k (__ :: Twice s))
(j, 1) -> reifyIntegral j (\(_ :: s) -> k (__ :: Succ (Twice s)))
(j,- 1) -> reifyIntegral j (\(_ :: s) -> k (__ :: Pred (Twice s)))
\end{code}
%
The second argument to the function |reifyIntegral| is a
continuation~|k| from the generated type~|s| to the answer type~|w|.
The generated type~|s| is in the class |ReflectNum|, so the |reflectNum| function
can convert it back to the value it came from. To be more
precise, |reifyIntegral| passes to the continuation~|k| a value
whose type belongs to the class |ReflectNum|. As we are interested only in the
type of that value, the value itself is~|__|. The continuation passed
to |reifyIntegral| should be able to process a value of any type
belonging to the class |ReflectNum|. Therefore, the continuation is
polymorphic and the function |reifyIntegral| has a
rank-2 type.
At the end of Section~\ref{s:modularclass}, we stumbled over
creating an instance of the class |Modular| to incorporate a
modulus unknown until
run time. Haskell does not let us
create instances at run time or locally,
but we can now get around that. We introduce a polymorphic
instance of the class |Modular|, parameterized over types in
the class |ReflectNum|. Each instance of |ReflectNum|
corresponds to a unique integer. In essence, we introduce
instances of the |Modular| class for \emph{every} integer.
At run time, we do not create a new instance for
the |Modular| class---rather, we use polymorphic recursion to choose
from the infinite family of instances already introduced.
\begin{code}
data ModulusNum s a
instance (ReflectNum s, Num a) =>
Modular (ModulusNum s a) a where
modulus _ = reflectNum (__ :: s)
\end{code}
%
We can now implement the function |withModulus|, which was the
stumbling block above. We call this function |withIntegralModulus|,
as it will be generalized below.
\begin{code}
withIntegralModulus :: Integral a =>
a -> (forall s. Modular s a => s -> w) -> w
withIntegralModulus i k =
reifyIntegral i (\(_ :: s) -> k (__ :: ModulusNum s a))
\end{code}
We can test the function by evaluating
|withIntegralModulus{-"\unskip\penalty0\;"-}(-42){-"\unskip\penalty0\;"-}modulus|.
The result is |-42|: the round-trip through types even leaves negative
numbers unscathed. Our ability to reify any integer, not just positive
ones, is useful below beyond modular arithmetic.
One caveat: The correctness of the round-trip is not checked by the
type system, unlike what one might expect from type systems that truly
offer singleton or dependent types. For example, if we accidentally omitted
|Succ| in |reifyIntegral| above, the compiler would not detect the error.
The reflection and reification functions therefore belong to a (relatively
compact) trusted kernel of our solution, which must be verified manually
and can be put into a library.
We can now write our running example as
\begin{spec}
test3' ::(Modular s a, Integral a) => s -> M s a
test3' _ = let a = M 3; b = M 5 in a*a + b*b
test3 = withIntegralModulus 4 (unM . test3')
\end{spec}
The sequence of modular operations appears in the
mathematically pleasing notation |a*a + b*b|. The modulus is implicit,
just as desired. Because we defined the method |fromInteger| in the class |Num|, this
example can be written more succinctly:
\begin{spec}
test3' :: (Modular s a, Integral a) => s -> M s a
test3' _ = 3*3 + 5*5
\end{spec}
Section~\ref{s:notation} further simplifies this notation.
A word on efficiency: With an ordinary compiler, every time
a modulus needs to be looked up (which is quite often), |reflectNum| performs
recursion of time linear in the number of bits in the modulus. That is pretty
inefficient. Fortunately, we can adjust the code so that Haskell's lazy
evaluation memoizes the result of |reflectNum|, which then only needs to run
once per reification, not once per reflection. For clarity, we do not make the
adjustment here. However, the code in
Section~\ref{s:reify-arbitrary} is so adjusted to memoize appropriately, out of necessity; the crucial
subexpression there is |const a| in |reflect|.
\Citet{thurston-modular} independently discovered the above techniques for
typing modular arithmetic in Haskell. The following extends this basic idea
to reifying values of serializable type, then any type.
\subsection{Reifying Lists}
\label{s:reify-storable}
Our immediate goal of implementing modular arithmetic without explicitly passing
moduli around is accomplished.
Although the type-class machinery we used to achieve this goal may seem heavy
at first, it statically and implicitly distinguishes multiple concurrent moduli,
which cannot be said of any previous solution to the configurations problem in
any pure or impure language. We also avoid using |unsafePerformIO|.
Section~\ref{s:more} below shows more real-world examples
to further illustrate the advantages of our approach. Those examples are
independent of the rest of Section~\ref{s:reify} here.
We now turn to a larger
goal---passing configuration data other than integers. For example,
many parameters for numerical code are floating point numbers, such as
tolerances. Also, user preferences are often strings.
A string can be regarded as a list of integers (character codes).
As the next step, we reify lists of integers into types. In principle,
this step is redundant: we already know how to reify
integers, and a list of integers can always be represented as
one (huge) integer. Supporting lists
directly, however, is faster and more convenient. We extend
our family of types with a type constant |Nil| and a binary type
constructor |Cons|, to build singly-linked lists at the type level.
\begin{code}
data Nil; data Cons s ss
class ReflectNums ss where reflectNums :: Num a => ss -> [a]
instance ReflectNums Nil where
reflectNums _ = []
instance (ReflectNum s, ReflectNums ss) =>
ReflectNums (Cons s ss) where
reflectNums _ = reflectNum (__ :: s) : reflectNums (__ :: ss)
reifyIntegrals :: Integral a =>
[a] -> (forall ss. ReflectNums ss => ss -> w) -> w
reifyIntegrals [] k = k (__ :: Nil)
reifyIntegrals (i:ii) k = reifyIntegral i (\(_ :: s) ->
reifyIntegrals ii (\(_ :: ss) ->
k (__ :: Cons s ss)))
\end{code}
We can check that lists of numbers round-trip unscathed: the expression
|reifyIntegrals [-10..10] reflectNums| returns the list of integers
from |-10| to~|10|.
Being able to reify a list of numbers to a type is more useful than
it may appear: we gain the ability to reflect any value whose type belongs to
the |Storable| type class in Haskell's foreign function interface, or FFI \citep{chakravarty-foreign}.
A |Storable| value is one that can be serialized as a sequence of bytes, then
reconstructed after being transported---over the network; across a foreign
function call; or, in our case, to the left of~|=>|.
(For reference, Appendix~\ref{app:ffi} \ofthisTR summarizes what we use of FFI.)
\begin{code}
type Byte = CChar
data Store s a
class ReflectStorable s where
reflectStorable :: Storable a => s a -> a
instance ReflectNums s => ReflectStorable (Store s) where
reflectStorable _ = unsafePerformIO
$ alloca
$ \p -> do pokeArray (castPtr p) bytes
peek p
where bytes = reflectNums (__ :: s) :: [Byte]
reifyStorable :: Storable a =>
a -> (forall s. ReflectStorable s => s a -> w) -> w
reifyStorable a k =
reifyIntegrals (bytes :: [Byte]) (\(_ :: s) -> k (__ :: Store s a))
where bytes = unsafePerformIO
$ with a (peekArray (sizeOf a) . castPtr)
\end{code}
The |reifyStorable| function defined here first serializes the value~|a| into an
array of |(sizeOf a)| bytes, temporarily allocated by FFI's |with|. It then
uses |reifyIntegrals| above to reify the bytes into a type. In the opposite
direction, the |reflectStorable| function first uses |reflectNums| to reflect
the type into another array of bytes, temporarily allocated by FFI's |alloca| to
ensure proper alignment. It then reconstructs the original value using FFI's
|peek|.
We must comment on the use of |unsafePerformIO| above, which
emphatically neither compromises static typing nor weakens static
guarantees.
The type signatures of |reifyStorable| and |reflectStorable| make it clear that
the values before reification and after reflection have the same type;
we do not replace type errors with run-time exceptions.
The code above invokes |unsafePerformIO| only because
it relies on FFI,
in which even mere serialization operates in the |IO| monad.
If functions like |pokeArray|, |peek|, and |peekArray| operated in the
|ST| monad instead, then we would be able to (happily) replace
|unsafePerformIO| with |runST|. We do not see any reason why serialization
should require the |IO| monad.
We can now round-trip floating-point numbers through the type system into
a dictionary: the expression
\begin{spec}
reifyStorable (2.5::Double) reflectStorable
\end{spec}
returns |2.5|. This capability is useful for modular arithmetic over a
real (fractional) domain---that is, over a circle with
a specified circumference as a metric space. Although multiplication no
longer makes sense in such a domain, addition and subtraction still do.
Admittedly, a floating-point number can be converted into a pair of
integers using the |decodeFloat| function, which provides a more portable
way to reify a value whose type belongs to the |RealFloat| type class in the Prelude.
Furthermore, any type that belongs
to both the |Show| class and the |Read| class can be transported without
involving FFI, as long as |read . show| is equivalent
to the identity as usual so that we can serialize the data thus.
However, we are about to reify
|StablePtr| values from FFI, and
the |StablePtr| type belongs to none of these classes, only |Storable|.
\subsection{Reifying Arbitrary Values}
\label{s:reify-arbitrary}
We now turn to our ultimate goal: to round-trip any Haskell value through the
type system, so as to be able to pass any dictionary as an explicit
argument, even ones involving polymorphic functions or abstract data
types. To achieve this, we use FFI to
convert the value to a |StablePtr| (``stable pointer''), which we then
reify as a type. From
the perspective of an ordinary Haskell value, Haskell's type system and
type-class instances are foreign indeed!\footnote
{The type variable |p| in this section is bound but never used.}
%format * = "\star "
\begin{code}
class Reflect s a | s -> a where reflect :: s -> a
data Stable (s :: * -> *) a
instance ReflectStorable s => Reflect (Stable s a) a where
reflect = unsafePerformIO
$ do a <- deRefStablePtr p
return (const a)
where p = reflectStorable (__ :: s p)
reify :: a -> (forall s. Reflect s a => s -> w) -> w
reify (a :: a) k = unsafePerformIO
$ do p <- newStablePtr a
reifyStorable p (\(_ :: s p) ->
k' (__ :: Stable s a))
where k' s = return (k s)
\end{code}
%format * = "\times "
We can now define the completely polymorphic |withModulus| function that
we set out to implement.
\begin{code}
data ModulusAny s
instance Reflect s a => Modular (ModulusAny s) a where
modulus _ = reflect (__ :: s)
withModulus a k = reify a (\(_ :: s) -> k (__ :: ModulusAny s))
\end{code}
This code passes configuration
data ``by reference'', whereas the code in Sections
\refrange{s:reify-integral}{s:reify-storable} passes them ``by
value''. Configuration data of arbitrary type may not be serialized,
so they must be passed by reference.
We use a stable pointer as that reference, so that the value is not
garbage\hyp collected away while the reference is in transit.
The code above has a memory leak: it allocates stable
pointers using |newStablePtr| but
never deallocates them using |freeStablePtr|. Thus every set of
configuration data leaks a stable pointer when reified. Configuration data in
programs are typically few and long-lived, so this memory leak is usually not
a problem. However, if the program dynamically generates and discards many pieces of
configuration data over its lifetime, then leaking one stable pointer per
reification is a significant resource drain.
If these memory leaks are significant, then we need to carefully ensure that the
|StablePtr| allocated in each reification operation is freed exactly once.
Unfortunately, this requires us to worry about how lazy evaluation and |seq|
interact with impure uses of |unsafePerformIO|: we need to make sure that each
stable pointer is freed exactly once. Below is the modified code.
\begin{spec}
instance ReflectStorable s => Reflect (Stable s a) a where
reflect = unsafePerformIO
$ do a <- deRefStablePtr p
freeStablePtr p
return (const a)
where p = reflectStorable (__ :: s p)
reify :: a -> (forall s. Reflect s a => s -> w) -> w
reify (a :: a) k = unsafePerformIO
$ do p <- newStablePtr a
reifyStorable p (\(_ :: s p) ->
k' (__ :: Stable s a))
where k' (s :: s) = (reflect :: s -> a) `seq` return (k s)
\end{spec}
We emphasize that this impure use of |unsafePerformIO| is only necessary if the
program reifies many non\hyp serializable parameters outside the |IO| monad over its lifetime. Such programs
are rare in practice; for example, a numerical analysis program or
a cryptography server may reify many parameters in a single run, but these
parameters are |Storable| values, like numbers.
\section{More Examples}
\label{s:more}
In this section we discuss two more examples of our approach to the
configurations problem. The first example illustrates how the flexibility of our
solution and its integration with type inference helps the programmer write code
in the most intuitive notation. The second example demonstrates how our solution
helps write fast code by guaranteeing that specialized versions of algorithms
are used when appropriate.
The second example also shows that our approach is wieldy to apply to
more realistic problems.
In particular, it shows that it is straightforward to generalize our
technique from one parameter (|modulus|) to many.
Appendix~\ref{app:jni} \ofthisTR contains another real-world example, where we contrast our
approach more concretely with implicit parameters.
\subsection{Flexible Propagation for\\ Intuitive Notation}
\label{s:notation}
Let us revisit the modular arithmetic example from
Section~\ref{s:reify-integral}, and trace how the modulus is propagated.
\begin{spec}
withIntegralModulus :: Integral a =>
a -> (forall s. Modular s a => s -> w) -> w
withIntegralModulus i k =
reifyIntegral i (\(_ :: t) -> k (__ :: ModulusNum t a))
test3' :: (Modular s a, Integral a) => s -> M s a
test3' _ = 3*3 + 5*5
test3 = withIntegralModulus 4 (unM . test3')
\end{spec}
The modulus~|4| starts out as the
argument to |withIntegralModulus|. Given this modulus, the function
|reifyIntegral| finds the corresponding type of the |ReflectNum|
family. That type, denoted by the type variable |t|, is then used to
build the type |ModulusNum t a|. The latter type is an instance of the
|Modular s a| class, with the type variable |s| now instantiated to
|ModulusNum t a|. When the function |test3'| is applied to the (bottom) value
of the latter type, |s| propagates from the argument of
|test3'| throughout the body of |test3'|. Because |s| is instantiated to |ModulusNum t a|, and
|t| uniquely corresponds to a particular modulus, the
modulus is available throughout |test3'|.
In this example, then, a parameter is propagated to |test3'| when the
argument type~|s| of |test3'| is unified with |ModulusNum t a|.
Because type unification works the same way for a function's argument type and
return type,
the type checker can propagate type information not only via arguments
of the function but also via its result. In the case of modular arithmetic,
propagating configuration information via the return type rather than argument
type of |test3'| leads to a
particularly concise and intuitive notation.
As the first step, we move the function |unM| inside
|withIntegralModulus|:
\begin{spec}
withIntegralModulus :: Integral a =>
a -> (forall s. Modular s a => s -> M s w) -> w
withIntegralModulus i k =
reifyIntegral i (\(_ :: t) -> unM $ k (__ :: ModulusNum t a))
\end{spec} % $
The type variable~|s| now appears in the result type of~|k|.
The modulus is now propagated to~|k|---in other words, the type variable~|s|
is now instantiated in the type of~|k|---in two ways: through its
argument type as well as its return type. If only for brevity,
we can now eliminate the first way by getting rid of the argument to~|k|:
\begin{code}
withIntegralModulus' :: Integral a =>
a -> (forall s. Modular s a => M s w) -> w
withIntegralModulus' (i::a) k :: w =
reifyIntegral i ( \(_ :: t) ->
unM (k :: M (ModulusNum t a) w))
test4' :: (Modular s a, Integral a) => M s a
test4' = 3*3 + 5*5
test4 = withIntegralModulus' 4 test4'
\end{code}
In the terminology of logic programming, we have switched from one mode of
invoking~|k|, where the argument type is bound and the result type is free, to
another mode, where the result type is bound. The resulting definition
|test4' = 3*3 + 5*5| cannot be more intuitive. The body of |test4'| performs
a sequence of arithmetic computations using the same modulus, which however
appears nowhere in the term, only in the type. The modulus parameter is
implicit; it explicitly appears only in the function |normalize| used in the
implementation of modular operations. The configuration data are indeed
pervasive and do stay out of the way. Furthermore, |test4'| is a top-level
binding, which can be exported from its home module and imported into other
modules. We have achieved implicit configuration while preserving modularity and
reuse.
The definition |test4' = 3*3 + 5*5| looks so intuitive that one may
even doubt whether every arithmetic operation in the term is indeed
performed modulo the invisible modulus. One might even think that we
first compute $3\times3 + 5\times5$ and later on divide~$34$ by the modulus.
However, what |term4'| actually computes is
\begin{spec}
mod ( mod (mod 3 m * mod 3 m) m
+ mod (mod 5 m * mod 5 m) m ) m
\end{spec}
Each operation is performed modulo the modulus~|m|
corresponding to the type~|s| in the signature of~|test4'|.
That top-level type signature is the only indication
that implicit configuration is at work, as desired. To check
that each operation in |term4'| is performed modulo~|m|, we can
trace the code using a debugger. We can also try to omit the type signature
of |test4'|. If we do that, we get a type error:
\begin{spec}
{-"\text{Inferred type is less polymorphic than expected}"-}
{-"\text{Quantified type variable }"-}s{-"\text{ escapes}"-}
{-"\text{It is mentioned in the environment: }"-}test4' :: M s w
{-"\text{In the second argument of }"-}withIntegralModulus'{-"\text{, namely }"-}test4'
{-"\text{In the definition of }"-}test4{-"\text{: }"-}test4 = withIntegralModulus' 4 test4'
\end{spec}
The fact that we get an error
contrasts with the implicit
parameter approach \citep{lewis-implicit}. In the latter, omitting the
signature may silently change the behavior of
the code. Our approach thus is both free from unpleasant surprises and
notationally intuitive.
\subsection{Run-Time Dispatch for Fast Performance}
\label{s:performance}
We now turn from optimizing the visual appearance of the code to
optimizing its run-time performance. A general
optimization strategy is to identify ``fast paths''---that is,
particular circumstances that permit specialized, faster
algorithms. We can then structure our code to first check for
auspicious circumstances. If they are present, we branch to the
specialized code; otherwise, generic code is run.
\begin{comment}
This approach,
to dynamically dispatch to statically known and optimized alternatives,
is used extensively in the compilation of Single Assignment~C
\citep{kreye-compilation}, for example.
\end{comment}
Modular arithmetic is a good example of such a
specialization. Modern cryptography uses lots of modular arithmetic, so
it is important to exploit fast execution paths.
\Citet{openssl}, a well-known open-source cryptography library,
uses specialized code on many levels. At
initialization time, it detects any cryptographic acceleration hardware
and sets up method handlers accordingly. Cryptographic operations
include sequences of modular addition and multiplication over the
same modulus. Moduli of certain forms permit
faster computations. OpenSSL maintains a
context |CTX| with pointers to addition and multiplication functions
for the modulus in effect. When initializing |CTX|, OpenSSL checks the
modulus to see if a faster version of modular operations can be used.
To use these optimized functions,
one can pass them as explicit function arguments, as OpenSSL does. This
impairs the appearance and maintainability of the code.
If several moduli are in use, each with its own |CTX| structure,
it is easy to pass the wrong one by
mistake. Our technique can improve this situation.
Because we can pass functions implicitly, we can pass
the addition and multiplication functions themselves as configuration data.
In simple cases, specialized
functions use the same data representation but a more efficient implementation.
For example, the Haskell |mod| function can be specialized to use bitwise operators when
the modulus is a power of~$2$. More often, however,
specialized functions operate
on custom representations of input data. For example,
\citearound{'s technique for modular multiplication}\citet{montgomery-modular}
is much faster than the standard algorithm when the modulus is odd, but it requires
input numbers to be represented by their
so-called $N$-residues. Furthermore, the algorithm needs several
parameters that are pre-computed from the modulus. Therefore,
at the beginning of a sequence of operations, we have to convert the
inputs into their $N$-residues, and compute and cache required
parameters. At the end, we have to convert the
result from its $N$-residue back to the regular
representation. For a long sequence of operations, switching
representations induces a net performance gain.
OpenSSL
uses Montgomery multiplication for modular exponentiation when the modulus is odd. Modular
exponentiation is a long sequence of modular multiplications. As
exponentiation begins, OpenSSL
converts the radix into its $N$-residue, computes the parameters, and
caches them. At the end, the library converts the result back from its $N$-residue and
disposes of the cache. Diffie-Hellman key exchanges, for example, invoke
modular exponentiation several times. To avoid converting representations
and computing parameters redundantly,
OpenSSL can save the Montgomery context
as the part of the overall |CTX|. This option raises correctness
concerns that are more severe than the mere inconvenience of explicitly
passing |CTX| around: While the Montgomery context is in effect,
what appears to be modular numbers to the client are actually their $N$-residues.
The client must take care
not to pass them to functions unaware of the Montgomery context.
The programmer must keep track of which
context---generic or Montgomery---is in effect and thus which
representation is in use. In sum, although the Montgomery
specialization is faster, its implementation in
OpenSSL invites user errors that jeopardize data integrity.
In this section, we show how to use a specialized representation
for modular numbers that is even more different from the standard
representation than Montgomery multiplication calls for. We represent
a modular number as not one $N$-residue but a pair of residues. The
type system statically guarantees the safety of the specialization;
different representations are statically separated.
Yet actual code specifying what to compute is not duplicated.
In our code so far, only the
modulus itself is propagated through the type
environment. Our instance of the |Num| class for the modulus\hyp
bearing numbers |M s a| implements general, unspecialized algorithms for
modular addition and multiplication.
If the modulus~$m$ is even, say of the form $2^p q$ where $p$ is positive and $q$ is odd, we can perform
modular operations more efficiently: taking advantage of the Chinese Remainder
Theorem, we can represent each modular number not as one residue modulo~$2^pq$
but as two residues, modulo $2^p$ and~$q$.
When we need to perform a long sequence of modular operations, such as
multiplications to compute $a^n \bmod m$ for large~$n$,
we first determine the residues of $a$ mod $2^p$ and $q$.
We perform the multiplications on each of the two residues, then
recombine them into one result. We
use the fact that the two factor moduli are smaller, and
operations modulo~$2^p$ are very fast.
This technique is known as \emph{residue number system arithmetic}
\citep{koren-computer,parhami-computer,soderstrand-residue}.
Four numbers need to be precomputed that depend on the modulus: $p$, $q$, $u$,
and~$v$, such that the modulus is $2^p q$ and
\[ \def\pod#1{\ (#1)}
u \equiv 1 \pmod{2^p} \text{, \ }
u \equiv 0 \pmod{q} \text{, \ }
v \equiv 0 \pmod{2^p} \text{, \ }
v \equiv 1 \pmod{q}.
\]
In order to propagate these four numbers as configuration data for even\hyp
modulus\hyp bearing numbers, we define a new data type |Even|. The type
arguments to |Even| specifies the configuration data to propagate; the
data constructor~|E| of |Even| specifies the run-time representation of even\hyp
modulus\hyp bearing numbers, as a pair of residues.
\begin{code}
data Even p q u v a = E a a deriving (Eq, Show)
\end{code}
We then define a |Num| instance for |Even|.
\begin{code}
normalizeEven :: ( ReflectNum p, ReflectNum q, Integral a,
Bits a) => a -> a -> Even p q u v a
normalizeEven a b :: Even p q u v a =
E (a .&. (shiftL 1 (reflectNum (__ :: p)) - 1)) -- $a \bmod 2^p$
(mod b (reflectNum (__ :: q))) -- $b \bmod q$
instance ( ReflectNum p, ReflectNum q,
ReflectNum u, ReflectNum v,
Integral a, Bits a) => Num (Even p q u v a) where
E a1 b1 + E a2 b2 = normalizeEven (a1 + a2) (b1 + b2)
{-"\raisebox{0pt}[2.5ex][0pt]{$\vdots$}"-}
\end{code}
\begin{comment}
\begin{code}
E a1 b1 - E a2 b2 = normalizeEven (a1 - a2) (b1 - b2)
E a1 b1 * E a2 b2 = normalizeEven (a1 * a2) (b1 * b2)
negate (E a b) = normalizeEven (-a) (-b)
fromInteger i = normalizeEven (fromInteger i)
(fromInteger i)
signum = error "Modular numbers are not signed"
abs = error "Modular numbers are not signed"
\end{code}
\end{comment}
Following this pattern, we can introduce several varieties of modulus\hyp
bearing numbers, optimized for particular kinds of moduli.
Each time the |withIntegralModulus'| function is called with a modulus, it
should select the best instance of the |Num| class for that
modulus. The implementation of modular operations in that instance will then be
used throughout the entire sequence of modular operations. This pattern of
run-time dispatch and compile-time propagation is illustrated below with two
|Num| instances: the general instance for~|M|, and the
specialized instance for~|Even|.
%format dotsb = "\dotsb "
\begin{comment}
\begin{code}
dotsb = dotsb
\end{code}
\end{comment}
\begin{code}
withIntegralModulus'' :: (Integral a, Bits a) =>
a -> (forall s. Num (s a) => s a) -> a
withIntegralModulus'' (i::a) k = case factor 0 i of
(0, i) -> withIntegralModulus' i k -- odd case
(p, q) -> let (u, v) = dotsb in -- even case: $i = 2^p q$
reifyIntegral p (\(_::p ) ->
reifyIntegral q (\(_::q ) ->
reifyIntegral u (\(_::u ) ->
reifyIntegral v (\(_::v ) ->
unEven (k :: Even p q u v a)))))
factor :: (Num p, Integral q) => p -> q -> (p, q)
factor p i = case quotRem i 2 of
(0, 0) -> (0, 0) -- just zero
(j, 0) -> factor (p+1) j -- accumulate powers of two
_ -> (p, i) -- not even
unEven ::( ReflectNum p, ReflectNum q, ReflectNum u,
ReflectNum v, Integral a, Bits a) => Even p q u v a -> a
unEven (E a b :: Even p q u v a) =
mod (a * (reflectNum (__ :: u)) + b * (reflectNum (__ :: v)))
(shiftL (reflectNum (__ :: q)) (reflectNum (__ :: p)))
\end{code}
%We elide above the computation of the factors |u| and~|v|.
The function
|withIntegralModulus''| checks at run time whether the received
modulus is even. This check is done only once per
sequence of modular operations denoted by the continuation~|k|. If the
modulus is even, the function chooses the
instance |Even| and computes the necessary parameters for that
instance: |p|, |q|, |u|, and~|v|. The continuation~|k|
then uses the faster versions of modular operations,
without any further checks or conversions between representations.
In Section~\ref{s:reify}, we introduced our technique with a type class with
a single member (|modulus|), parameterized by a single integer. The code above
propagates multiple pieces of configuration information (namely the
members of the |Num| class: |+|, |-|, |*|, etc.), parameterized by four
integers. The generalization is straightforward:
|withIntegralModulus''| calls |reifyIntegral| four times, and the instance
|Num (Even p q u v a)| defines multiple members at once.
OpenSSL's source code for modular exponentiation
(\texttt{bn\_exp.c}) mentions, in comments, this
specialized multiplication
algorithm for even moduli. However, it does not
implement the specialization, perhaps because it is too much trouble for the programmer to
explicitly deal with the significantly different
representation of numbers (as residue pairs) and ensure the
correctness of the C code.
The example below tests both the general and specialized cases:
\begin{code}
test5 :: Num (s a) => s a
test5 = 1000*1000 + 513*513
test5' = withIntegralModulus'' 1279 test5 :: Integer
test5'' = withIntegralModulus'' 1280 test5 :: Integer
\end{code}
The body of |test5| contains two multiplications and one addition.
Whereas |test5'| uses the generic implementation of
these operations, |test5''| invokes
the specialized versions as the modulus $1280$ is even.
We can see that by tracing both versions of functions.
\begin{comment}
\todo{perhaps we should mention -- a bit here and perhaps even in the
introduction that many creative uses of the type system (type
hacking) work only in the static context: all types in question are
known statically, all choices of instances are made statically.
[For example, in C++, partial template specialization, intended to
give specialized, more efficient implementations -- is performed
statically. Overlapping instances in Hugs, which serve the similar
purpose, are also chosen and instantiated statically.] This
example clearly shows that our technique indeed works in the dynamic
case, where the parameters -- and even the types of the
modulus-bearing numbers in question -- are not known until the run
time.}
\end{comment}
This example shows that types can propagate
not just integers but also functions parameterized
by them---in other words, closures. Crucially, exactly the
same sequence of operations |test5| uses either generic or
specialized modular operations, depending on the
modulus value at run time. The specialized modular operations use a
different representation of numbers, as residue pairs. The
type system encapsulates the specialized representation of numbers.
We thus attain a static correctness guarantee that OpenSSL cannot provide.
This comparison underscores the fact that our approach to the
configurations problem benefits pure and impure languages alike.
%stopzone
\section{Discussion and Related Work}
\label{s:related}
Our solution to the configurations problem can be understood from several
different perspectives.
\begin{enumerate}
\item It emulates local type-class instance declarations while preserving
principal types.
\item It ensures the coherence of implicit parameters by associating them
with phantom types.
\item It fakes dependent types: types can depend on not values but
types that faithfully represent each value.
\end{enumerate}
We now detail these perspectives in turn. Overall, we
recommend that local type-class instances be added to Haskell as a built-in
feature to replace implicit parameters and fake dependent types.
\subsection{Local Type-Class Instances}
The purpose of the type-system hackery in Section~\ref{s:reify}, first
stated in Section~\ref{s:modularclass}, is not to market headache medicine but
to explicitly pass a dictionary to a function with a qualified type. For
example, we want to apply a function of type |forall s. Modular s a => s -> w|
to a dictionary witnessing the type-class constraint |Modular s a|. In general,
we want to manufacture and use type-class instances at run time. In other
words, we want to declare type-class instances not just at the top level but
also \emph{locally}, under the scope of variables.
Sections \ref{s:modular} and~\ref{s:more} of this paper show that local
type-class instances are very useful. Although we can emulate local instances
using the hackery in Section~\ref{s:reify}, it would be more convenient if
a future version of Haskell could support them directly as a language feature.
At first try, the syntax for this feature might look like the following.
\begin{spec}
data Label
withModulus :: a -> (forall s. Modular s a => s -> w) -> w
withModulus (m :: a) k =
let instance Modular Label a where modulus _ = m
in k (__ :: Label)
\end{spec}
The new syntax added is the |instance| declaration under |let|, against
which the continuation~|k| resolves its overloading.
A problem with this first attempt, pointed out early on by
\citet[Section~A.7]{wadler-ad-hoc}, is that principle types are lost in the
presence of unrestricted local instances. For example, the term
\begin{spec}
data Label1; data Label2
let instance Modular Label1 Int where modulus _ = 4
instance Modular Label2 Int where modulus _ = 4
in modulus
\end{spec}
has no principle type, only the types |Label1 -> Int| and |Label2 -> Int|,
neither of which subsumes the other.
(It may seem that this term should have the (principal) type
|Modular s Int => s -> Int|, but that would result in unresolved overloading
and defeat the purpose of the local instances.)
This problem is one reason why Haskell
today allows only global instances, as \citeauthor{wadler-ad-hoc}
suggested.
\Citeauthor{wadler-ad-hoc} close their paper by asking the open question ``whether
there is some less drastic restriction that still ensures the existence of
principal types.'' We conjecture that one such restriction is to require that
the type-class parameters of each local instance mention some
\emph{opaque} type at the very same |let|-binding scope.
We define an opaque type at a given scope to be a type
variable whose existential quantification is eliminated (``opened''), or
universal quantification is introduced (``generalized''), at that scope.
For example, |withModulus| would be implemented as follows.
\begin{spec}
data Any = forall s. Any s
withModulus (m :: a) k =
let Any (_ :: s) = Any ()
instance Modular s a where modulus _ = m
in k (__ :: s)
\end{spec}
The above code satisfies our proposed restriction because the local instance
|Modular s a| mentions the type variable~|s|, which results from
existential elimination (|let Any (_ :: s) = dotsb|) at the very same scope.
This restriction is directly suggested by our technique in
Section~\ref{s:reify}. There, we build a different type for
each modulus value to be represented, so a function that
can take any modulus value as input is one that can take any
modulus\hyp representing opaque type as input. Just as
\citet{launchbury-lazy,launchbury-state} use an opaque type to
represent an unknown state thread, we use an opaque type to
represent an unknown modulus.
The term below is analogous to the problematic term
above without a principal type, but adheres to our proposed restriction.
\begin{spec}
let Any (_ :: s1 ) = Any ()
instance Modular s1 Int where modulus _ = 4
Any (_ :: s2 ) = Any ()
instance Modular s2 Int where modulus _ = 4
in modulus
\end{spec}
This term satisfies the principal type property---vacuously, because it simply
does not type! Although |modulus| has both the type |s1 -> Int| and the type
|s2 -> Int| within the scope of the |let|, neither type survives outside,
because the type variables |s1| and~|s2| cannot escape.
Our proposed restriction not only rescues the principal type property in
\citeauthor{wadler-ad-hoc}'s example above, but also preserves the
\emph{coherence} of type classes.
Coherence means that two typing derivations for the same term at the same
type in the same environment must be observationally equivalent.
Coherence is important in our solution to the configurations problem, because we
need each type to represent at most one value in order to statically separate
multiple configuration sets---be they multiple moduli as in the examples above,
or multiple threads of the Java virtual machine as in Appendix~\ref{app:jni} \ofthisTR \unskip.
Standard Haskell ensures coherence by prohibiting overlapping instances.
By requiring that every local instance mention an opaque type, we ensure that two
local instances from different scopes cannot overlap---at least, not if their
parameters are fully instantiated. We leave
local instances with uninstantiated type variables in the head
for future research.
To sum up, when examined from the perspective of local type-class instances, our
type-system hackery suggests a restriction on local instances that (we
conjecture) salvages principal types. In other words, we suggest
adding local instances to Haskell as syntactic sugar for our reification
technique. As an aside, local instances
as a built-in language feature would allow constraints in their contexts.
To support such constraints under our current technique would call for
\citearound{'s simulation}\citet{trifonov-simulating}.
\subsection{Implicit Parameters}
\label{s:implicit-parameters}
Our approach to the configurations problem is in the same
implicit spirit as \citearound{'s implicit parameters}\citet{lewis-implicit}.
Emulating LISP's dynamically-scoped variables (as explained by \citet{queinnec-lisp} among others),
\citeauthor{lewis-implicit}\ extend Haskell's
type-class constraints like |Modular s a| with implicit\hyp parameter
constraints like |?modulus :: a|. Under this proposal, modular arithmetic
would be implemented by code such as
\begin{spec}
add :: (Integral a, ?modulus :: a) => a -> a -> a
add a b = mod (a + b) {-"\;"-}?modulus
mul :: (Integral a, ?modulus :: a) => a -> a -> a
mul a b = mod (a * b) {-"\;"-}?modulus
\end{spec}
The type checker can infer the signatures above.
The implicit parameter |?modulus| can be assigned a value within a dynamic scope
using a new $\mathbf{with}$ construct; for example:\footnote
{In the Glasgow Haskell Compiler, implicit parameters are bound not using a
separate $\mathbf{with}$ construct but using a special |let| or |where| binding
form, as in |let {-""-}?modulus = 4 in add (mul 3 3) (mul 5 5)|.
We stick with \citeauthor{lewis-implicit}'s notation here.}
\begin{spec}
add (mul 3 3) (mul 5 5) {-"\;\mathbf{with}\;"-} ?modulus = 4 -- evaluates to~$2$
\end{spec}
%
\Citeauthor{lewis-implicit}, like us, intend to solve the configurations problem,
so the programming examples they give to justify their work apply equally to
ours. Both approaches rely on dictionaries, which are arguments
implicitly available to any polymorphic function with a quantified type.
Dictionary arguments are passed like any other argument at run-time, but they
are hidden from the term representation and managed by the compiler,
so the program is less cluttered.
Whereas we take advantage of the type-class system, implicit parameters augment
it. \Citeauthor{lewis-implicit}\ frame their work as ``the first half of
a larger research programme to de\hyp construct the complex type class system of
Haskell into simpler, orthogonal language features''. Unfortunately, because
implicit parameters are a form of dynamic scoping, they interact with the type
system in several undesirable ways \citep{peyton-jones-implicit}:
\begin{enumerate}
\item It is not sound to inline code (in other words, to $\beta$-reduce)
in the presence of implicit parameters.
\item A term's behavior can change if its signature is added, removed, or
changed.
\item Generalizing over implicit parameters is desirable, but may
contradict the monomorphism restriction.
\item Implicit parameter constraints cannot appear in the context of a
class or instance declaration.
\end{enumerate}
One may claim that the many troubles of implicit parameters come from the
monomorphism restriction, which ought to be abandoned. Without defending
the monomorphism restriction in any way, we
emphasize that trouble (such as unexpected loss of sharing and undesired
generalization) would still remain without the monomorphism restriction.
\Citet[Section~6]{hughes-global} shows a problem that arises
exactly when the monomorphism restriction does not apply.
The trouble with implicit parameters begins when multiple configurations come
into play in the same program, as \citeauthor{lewis-implicit}\ allow.
We blame the trouble on the fact that implicit parameters express configuration
dependencies in dynamic scopes, whereas we express those dependencies in static
types. Dynamic scopes change as the program executes, whereas static types do
not. Because dependencies should not change once established by the programmer,
static types are more appropriate than dynamic scopes for carrying multiple
configurations. Expressing value dependencies in static types is the
essence of type classes, which our solution relies on.
Because Haskell programmers are already familiar with type classes,
they can bring all their intuitions
to bear on the propagation of configuration data, along with
guarantees of coherence. In
particular, a type annotation can always be added
without ill effects.
We ask the programmer to specify which configurations to pass
where by giving type annotations.
Taking advantage of type flow as distinct from data flow in this
way enables notation that can be more flexible than extending the term language as
\citeauthor{lewis-implicit}\ propose, yet more concise than passing function
arguments explicitly.
Appendix~\ref{app:jni} \ofthisTR shows a real-world example, where we contrast our type-based
approach more concretely with the scope-based approach of implicit parameters.
Because we tie configuration dependencies to type variables, we can easily
juggle multiple sets of configurations active in the same scope, such
as multiple modular numbers with different moduli. More precisely, we use
phantom types to distinguish between multiple instances of the same
configuration class. For example, if two moduli are active in the same scope,
two instances |Modular s1 a| and |Modular s2 a| are available and do not overlap
with each other. Another way to make multiple instances available while
avoiding the incoherence problem caused by overlapping instances is to introduce
\emph{named instances} into the language, as proposed by \citet{kahl-named}.
By contrast, when multiple implicit parameters with the same name and type are
active in the same scope, \citet{hughes-global} cautions that ``programmers must
just be careful!''
One way to understand our work is that we use the coherence of type classes to
temper ambiguous overloading among multiple implicit parameters.
There is a drawback to using types to
propagate configurations, though: any dependency
must be expressed in types,
or the overloading will be rejected as unresolved or
ambiguous. For example, whereas |sort| can have the type
\begin{spec}
sort :: (?compare :: a -> a -> Ordering) => [a] -> [a]
\end{spec}
with implicit parameters, the analogous type on our approach
\begin{spec}
sort :: Compare s a => [a] -> [a] -- illegal
class Compare s a where compare :: s -> a -> a -> Ordering
\end{spec}
is illegal because the phantom type~|s| does not appear in the type
|[a] -> [a]|. Instead, we may write one of the following signatures.
\begin{spec}
sort1 :: Compare s a => s -> [a] -> [a] -- ok
sort2 :: Compare s a => [M s a] -> [M s a] -- ok
\end{spec}
Using |sort1| is just like passing the comparison function as an explicit
argument. Using |sort2| is just like defining a type class to compare values.
Standard Haskell already provides for both of these possibilities, in the form
of the |sortBy| function and the |Ord| class. We have nothing better to offer
than using them directly, except we effectively allow an instance of the |Ord| class to be
defined locally, in case a comparison function becomes known only at run time.
By contrast, a program that uses only one comparison function (so that coherence
is not at stake) can be written more succinctly and intuitively using implicit
parameters, or even |unsafePerformIO|.
This problem is essentially the ambiguity of |show . read|.
Such overloading issues have proven reasonably intuitive for Haskell programmers
to grasp and fix, if only disappointedly.
The success of type classes in Haskell suggests that the natural type
structure of programs often makes expressing dependencies easy.
Our examples, including the additional example in Appendix~\ref{app:jni} \ofthisTR \unskip, illustrate this point.
Nevertheless, our use of types to enforce coherence
incurs some complexity that is worthwhile only in
more advanced cases of the configurations problem, when multiple
configurations are present.
\subsection{Other Related Work}
Our use of FFI treats the type (class)
system as foreign to values, and uses phantom types to bridge the gap.
\citearound{'s foreign function interface for SML/NJ}\Citet{blume-foreign}
also uses phantom types extensively---for array dimensions, |const|-ness
of objects, and even names of C structures. For names of C structures, he
introduces type constructors for each letter that can appear in an identifier.
The present paper shows how to reflect strings
into types more frugally.
We showed how to specialize code at run time with
different sets of primitive operations (such as for modular
arithmetic). Our approach in this regard is related to overloading but
specifically not partial evaluation, nor run-time code generation. It
can however be fruitfully complemented by partial evaluation
\citep{jones-dictionary-free}, for example when an integral modulus
is fixed at compile time.
In our approach, specialized code can use custom data representations.
The example in Section~\ref{s:performance} shows that we effectively select a
particular class instance based on run-time values.
We are therefore ``faking it'' \citep{mcbride-faking}---faking a dependent
type system---more than before.
\citearound{'s paper}\Citet{mcbride-faking} provides an excellent overview of
various approaches to dependent types in Haskell.
In approaches based on type classes, Haskell's coherence property
guarantees that each type represents at most one value (of a given
type), so compile-time type equality entails (that is, soundly approximates) run-time value equality.
Appendix~\ref{app:jni} demonstrates the utility of this entailment.
\Citeauthor{mcbride-faking} mentions that, with all the tricks,
the programmer still must decide if data belong in compile-time types or
run-time terms. ``The barrier represented by~|::| has not been
broken, nor is it likely to be in the near future.'' If our |reflect| and
especially |reify| functions have not broken the
barrier, they at least dug a tunnel underneath.
\section{Conclusions}
\label{s:conclusions}
We have presented a solution to the configurations problem that satisfies
our desiderata.
Although its start-up cost in complexity is higher than previous approaches,
it is more flexible and robust, especially in the presence of multiple
configurations.
We have shifted the burden of propagating user
preferences from the programmer to the
type checker. Hence, the configuration data are statically typed,
and differently parameterized pieces of code are statically
separated. Type annotations are required, but they are infrequent and
mostly attached to top-level terms. The compiler will point out
if a type annotation is missing, as a special case of the monomorphism
restriction. By contrast, implicit parameters interact badly with
the type system, with or without the monomorphism restriction.
Our solution leads to
intuitive term notation: run-time configuration parameters can be
referred to just like compile-time constants in
global scope. We can propagate any type of configuration data---numbers,
strings, polymorphic functions, closures, and abstract data like |IO| actions.
Our code only uses |unsafePerformIO| as part of FFI,
so no dynamic typing is involved. Furthermore, |unsafePerformIO| is unnecessary
for the most frequent parameter types---numbers, lists, and strings.
At run-time, our solution introduces negligible time and space overhead:
linear in the size of the parameter data or pointers to
them, amortized over their lifetimes.
Our solution is available in Haskell today;
this paper shows all needed code.
% TODO{put the report online, put this .lhs file online, and make a reference here}
Our solution to the configurations problem lends itself to performance
optimizations by dynamically dispatching to specialized, optimized versions of
code based on run-time input values. The optimized versions of code
may use specialized data representations,
whose separation is statically guaranteed.
Refactoring existing code to support such
run-time parameterization requires minimum or no changes, and no code duplication.
Our approach relies on phantom types, polymorphic recursion, and
higher-rank polymorphism. To propagate values via types, we build
a family of types, each
corresponding to a unique value. In one direction, a value is reified into its
corresponding type by a polymorphic recursive
function with a higher-rank continuation argument. In the other direction,
a type is reflected back into its corresponding value by
a type class whose polymorphic instances encompass the type family.
In effect, we emulate local type-class instance declarations by
choosing, at run time, the appropriate instance indexed by the member of
the type family that reifies the desired dictionary.
This emulation suggests adding local instances to Haskell, with a
restriction that we conjecture preserves principal types and coherence.
This technique allows Haskell's existing type system to emulate
dependent types even more closely.
\section{Acknowledgements}
Thanks to Jan-Willem Maessen, Simon Peyton Jones, Andrew Pimlott, Gregory Price, Stuart Shieber, Dylan Thurston,
and the anonymous reviewers for the 2004 ICFP and Haskell Workshop. The second author
is supported by the United States National Science Foundation Grant BCS-0236592.
\bibliographystyle{abbrvnat}
\setlength\bibsep{0pt}
%%% ACM CUT %%%
\bibliography{prepose}
\appendix
\section{Another Example:\\ Java Native Interface}
\label{app:jni}
This appendix shows a real-world example in which the natural type structure of
the program lends itself to phantom-type annotations on not just one type (like
|M| in modular arithmetic) but many types. We contrast our solution with the
implicit parameters solution originally given by
\citet[Section~4.4]{lewis-implicit}.
The problem arises
in a Haskell binding to the Java Native Interface (JNI). JNI is to
Java as FFI is to Haskell: the purpose of JNI is for
Java code to call and be called by code written in C and (from there) Haskell
(say). These calls require passing an abstract |JNIEnv| value back and forth,
which points to a virtual method table (approximated with |Int| below) and roughly corresponds to a thread in the Java virtual machine.
\Citeauthor{lewis-implicit}\ propose that this |JNIEnv| value be passed as an
implicit parameter.
\begin{code}
type JNIEnv = Ptr Int
\end{code}
To take \citeauthor{lewis-implicit}'s example, suppose we want to implement the
following Java class with a method written in Haskell.
\begin{java}
class HaskellPrompt {
String prompt;
native String ask();
}
\end{java}
The \texttt{ask} method is supposed to display the \texttt{prompt} string,
then read and return a line of input. Although the \texttt{ask} method
appears to take no arguments on the Java side, the corresponding Haskell-side
function |ask| takes two arguments: a |JNIEnv| pointer representing the
current thread, and a |Jobject| pointer representing the \texttt{HaskellPrompt}
object whose \texttt{ask} method is being invoked.
\begin{spec}
ask :: JNIEnv -> Jobject -> IO JString
\end{spec}
To do its job, |ask| needs to access the \texttt{prompt} field of the
|Jobject| it received, as well as create a new Java \texttt{String} containing
the user's response. JNI provides myriad utility functions for such operations,
each of which takes |JNIEnv| as the first argument.\footnote
{For simplicity, we assume that the |getObjectField| function returns a |JString|.
To be more precise, it returns a |Jobject| that in our case can be
coerced to a |JString|.}
\begin{spec}
getObjectClass :: JNIEnv -> Jobject -> IO Jclass
getFieldID :: JNIEnv -> Jclass ->
String -> String -> IO FieldID
getObjectField :: JNIEnv ->
Jobject -> FieldID -> IO JString
getStringUTFChars :: JNIEnv -> JString -> IO String
newStringUTF :: JNIEnv -> String -> IO JString
\end{spec}
Passing parameters explicitly, then, the |ask| function can be implemented as
follows.
\begin{spec}
ask jnienv this =
do cls <- getObjectClass jnienv this
field <- getFieldID jnienv cls "prompt"
"Ljava/lang/String;"
jprompt <- getObjectField jnienv this field
prompt <- getStringUTFChars jnienv jprompt
putStr prompt
answer <- getLine
newStringUTF jnienv answer
\end{spec}
It is tedious to pass the same |JNIEnv| argument all over the place, as we have to
above.
Suppose we move the |JNIEnv| argument into an implicit parameter. That is,
suppose we change the signatures of the JNI utility functions to the following.
\begin{spec}
getObjectClass :: (?jnienv :: JNIEnv) =>
Jobject -> IO Jclass
getFieldID :: (?jnienv :: JNIEnv) => Jclass ->
String -> String -> IO FieldID
getObjectField :: (?jnienv :: JNIEnv) =>
Jobject -> FieldID -> IO JString
getStringUTFChars :: (?jnienv :: JNIEnv) =>
JString -> IO String
newStringUTF :: (?jnienv :: JNIEnv) =>
String -> IO JString
\end{spec}
We can then write cleaner code for |ask|:
\begin{code}
ask this =
do cls <- getObjectClass this
field <- getFieldID cls "prompt"
"Ljava/lang/String;"
jprompt <- getObjectField this field
prompt <- getStringUTFChars jprompt
putStr prompt
answer <- getLine
newStringUTF answer
\end{code}
Gone is the tedious sprinkle of |jnienv| throughout our code. Moreover,
the compiler automatically infers the correct type for |ask|:
\begin{spec}
ask :: (?jnienv :: JNIEnv) => Jobject -> IO JString
\end{spec}
However, nothing prevents the programmer from mixing up one |JNIEnv| with
another. For example, the following code overrides the value of |?jnienv|
during the call to |getFieldID|.
\begin{spec}
ask this = do cls <- getObjectClass this
field <- getFieldID cls "prompt"
"Ljava/lang/String;" {-"\;\mathbf{with}\;"-} ?jnienv = dotsb
{-"\text\dots"-}
\end{spec}
This code passes the type-checker, but is disallowed by JNI.
Using the technique in this paper, we can pass |JNIEnv| values implicitly while
statically preventing this illicit mixing. To apply our approach, we need to
involve a phantom type in the signatures of functions like |getObjectClass| and
|ask|. As in Section~\ref{s:performance}, one phantom type suffices for any
number of parameters, now or potentially added later.
Fortunately, as is often the case, our code already uses many custom types,
namely JNI's |Jobject|, |Jclass|, and |JString|. These types are the ideal
host for a parasitic phantom type.
We change the abstract types |Jobject|, |Jclass|,
and |JString| to take a phantom-type argument. They become
|Jobject s|, |Jclass s|, and |JString s|. The |JNIEnv| can then piggyback on
any of these types, without affecting the run-time representation of any data
or otherwise inflicting too much pain.
\begin{spec}
data Jobject s -- abstract
data Jclass s -- abstract
data JString s -- abstract
\end{spec}
We use the fact that |JNIEnv| is a |Storable| type to reify it.
Because all JNI calls take place in the |IO| monad, we no longer need
to resort to |unsafePerformIO| for reification and reflection, however safe
it was to do so in Section~\ref{s:reify-storable}.
\begin{code}
data JNIENV s
class JNI s where jnienv :: s -> IO JNIEnv
instance ReflectNums s => JNI (JNIENV s) where
jnienv _ = alloca $ \p -> do pokeArray (castPtr p) bytes
peek p
where bytes = reflectNums (__ :: s) :: [Byte]
reifyJNIEnv :: JNIEnv -> (forall s. JNI s => s -> IO w) -> IO w
reifyJNIEnv jnienv k =
do bytes <- with jnienv (peekArray (sizeOf jnienv) . castPtr)
reifyIntegrals (bytes :: [Byte])
(\(_ :: s) -> k (__ :: JNIENV s))
\end{code} %$
We then assign new type signatures to the JNI utility functions.
\begin{code}
getObjectClass :: JNI s => Jobject s -> IO (Jclass s)
getFieldID :: JNI s => Jclass s ->
String -> String -> IO FieldID
getObjectField :: JNI s => Jobject s ->
FieldID -> IO (JString s)
getStringUTFChars :: JNI s => JString s -> IO String
newStringUTF :: JNI s => String -> IO (JString s)
\end{code}
The cleaner version of |ask| above, written to use implicit parameters, works
exactly as is! Of course, our approach assigns it a different type signature:
\begin{code}
ask :: JNI s => Jobject s -> IO (JString s)
\end{code}
Moreover, it no longer type-checks to call |getObjectClass| with one |JNIEnv|
and |getFieldID| subsequently with another |JNIEnv|, as allowed under the
implicit parameters approach. The mismatch is caught under our approach,
because the return type |Jclass s| from |getObjectClass| is unified against the
argument type |Jclass s| to |getFieldID|.
Incidentally, it is semantically significant for us to associate the implicit
|JNIEnv| value with other |J|-types: for example, a |Jobject| pointer makes
sense only in the context of the |JNIEnv| where it was obtained. Thus our
approach statically ensures an invariant of JNI. This kind of invariant is
present in many application frameworks---graphical toolkits, database
libraries, and so on.
Unlike with implicit parameters, we can ensure that |JNIEnv| values are equal at
run time by unifying phantom types at compile time. We can do so
because, as mentioned in Section~\ref{s:modularclass}, each type~|s| corresponds
to at most one |JNIEnv| value. This uniqueness guarantee in turn obtains
because Haskell prohibits overlapping instances to ensure the coherence of
overloading.
One advantage shared by implicit parameters and our approach is the ability to
interact transparently with higher-order combinators. For example, consider the
|handle| function that is part of Haskell's exception facility.
\begin{spec}
handle :: (Exception -> IO a) -> IO a -> IO a
\end{spec}
The |handle| function takes two arguments, an exception handler and an |IO|
action. The exception handler is invoked in case the |IO| action throws an
exception. In our |ask| function, to prepare for times when the Java virtual
machine is not feeling well, we can wrap |handle| around some monadic code, as
follows.
\begin{code}
ask' this = handle handler (ask this)
handler exception = newStringUTF "error"
\end{code}
Even though the exception |handler| is outside the lexical scope of |ask| and
|ask'|, the necessary configuration information is still propagated. Haskell
knows that an exception handler must use the same |JNIEnv| value to invoke
|newStringUTF| as the main |ask| function does, because both arguments to
|handle| return the same type |IO a|, or |IO (JString s)| with the same phantom
type~|s|. Here, as in Section~\ref{s:notation}, the configuration information
flows from the return type of a function (|handle|) to its arguments, and from
one argument to another---not necessarily in the same direction as data flow.
Here, just as in Section~\ref{s:modularclass}, it is more natural to propagate
configurations via types than via terms:
The two arguments to |handle|, like multiple branches of a |case| expression,
can receive the same configuration via a single type signature.
By contrast, if we chose to solve the configurations problem by putting |JNIEnv|
information in a reader monad transformer applied to the |IO| monad, then the
|handle| combinator would need to undergo custom lifting in order to have the
right type in order to operate on the lifted |IO| monad.
That is, if we lift |IO| to |IO'|, then we also need to lift |handle| to
the type |(Exception -> IO' a) -> IO' a -> IO' a|.
This is a special case of the long-standing issue of lifting monadic
operations through a monad transformer \citep{liang-interpreter}.
\begin{comment}
\begin{spec}
getObjectClass = undefined
getFieldID = undefined
getObjectField = undefined
getStringUTFChars = undefined
newStringUTF = undefined
\end{spec}
\end{comment}
\section{Foreign Function Interface}
\label{app:ffi}
The following type signatures summarize the part of Haskell's foreign function
interface that Section~\ref{s:reify} uses.
\begin{spec}
unsafePerformIO :: IO a -> a
castPtr :: Ptr a -> Ptr b
\end{spec}
A value of type |Ptr a| points to a storage area to or from which Haskell values
of type~|a|, where |a| belongs to the |Storable| type class, may be marshalled.
\begin{spec}
alloca :: Storable a => (Ptr a -> IO b) -> IO b
peek :: Storable a => Ptr a -> IO a
peekArray :: Storable a => Int -> Ptr a -> IO [a]
pokeArray :: Storable a => Ptr a -> [a] -> IO ()
sizeOf :: Storable a => a {-unused-} -> Int
with :: Storable a => a -> (Ptr a -> IO b) -> IO b
\end{spec}
A value of type |StablePtr a| refers to a Haskell
value of type~|a| that will not be garbage\hyp collected until
|freeStablePtr| is called.
\begin{spec}
newStablePtr :: a -> IO (StablePtr a)
deRefStablePtr :: StablePtr a -> IO a
freeStablePtr :: StablePtr a -> IO ()
\end{spec}
\end{document}
\begin{code}
data Jobject s -- abstract
data Jclass s -- abstract
data JString s = JString String
\end{code}
The following text, after the end\{document\} fills in enough details
in the above JNI example that it could actually be run.
\begin{code}
newtype FieldID = FieldID Int deriving Show
getObjectClass (jobj::Jobject s) =
do
str <- jnienv (__::s) >>= call_jni >>= (return . show)
putStrLn $ "Doing getObjectClass, env: " ++ str
return (__::Jclass s)
getFieldID (jcl::Jclass s) fieldn typn =
do
str <- jnienv (__::s) >>= call_jni >>= (return . show)
putStrLn $ "Doing getFieldID, env: " ++ str
++ ":" ++ fieldn ++ ":" ++ typn
return $ FieldID 1
-- The following is the real signature. But it assumes subtyping:
-- Jobject returned may be JString
--getObjectField:: JNIENV s => Jobject s -> FieldID -> IO (Jobject s)
getObjectField (job::Jobject s) (FieldID fid) =
do
env <- jnienv (__::s) >>= call_jni
let sen = show env
-- the following line is to let us check our error handling
if env < 0 then error "getObjectField error" else return ()
putStrLn $ "Doing getObjectField, env: " ++ sen
++ ":" ++ (show fid)
return $ JString "jstring"
getStringUTFChars ((JString str)::JString s) =
do
return str
newStringUTF str :: IO (JString s) = do
sen <- jnienv (__::s) >>= call_jni >>= (return . show)
putStrLn $ "Doing newStringUTF, env: " ++ sen
return $ JString str
getLine = return "answer"
call_jni jenv = peek jenv
\end{code} %$
The test code:
\begin{code}
test_ask =
do
ans <- with 10
(\ jenv -> reifyJNIEnv jenv
(\ (_::s) -> (ask (__::Jobject s)
>>=getStringUTFChars)))
putStrLn ans
\end{code}
Testing the exception handling:
\begin{code}
test_ask' =
do
jenv1 <- new 10
ans1 <- reifyJNIEnv jenv1
(\ (_::s) -> (ask' (__::Jobject s)
>>=getStringUTFChars))
putStrLn ans1
jenv2 <- new (-10)
ans2 <- reifyJNIEnv jenv2
(\ (_::s) -> (ask' (__::Jobject s)
>>=getStringUTFChars))
putStrLn ans2
\end{code}
% vim:filetype=tex