(Int->)n([]ne)->...
undefined to definedappendMost code samples in this section require a Haskell extension to
multi-parameter classes with functional dependencies. Some examples
need an existential datatype extension. Both extensions are
commonly implemented. They can be activated by passing a flag -fglasgow-exts to the Glasgow Haskell system GHC or GHCi, and a
flag -98 to Hugs.
It is sometimes claimed that Haskell does not have polyvariadic functions. Here we demonstrate how to define functions with indefinitely many arguments; those arguments do not have to be of the same type.
The code referenced below shows that defining polyvariadic
functions takes only a few lines of Haskell code, and requires only
the most common extension of multiparameter classes with functional
dependencies. Here is an example of using a polyvariadic function,
build, which takes an arbitrary number of arguments and
returns them in a list. The function build is first
class, and so can be passed as an argument to other functions, such as
use_build below.
use_build::(forall r a. (BuildList a r) => a -> r)
-> x -> x -> x -> x -> [[x]]
use_build bb a b c d =
let t1 = bb a -- bb is indeed polyvariadic
t2 = bb a b
t3 = bb a b c
t4 = bb a b c d
t5 = bb a b c d a
in [t1,t2,t3,t4,t5]
test_ub = use_build build 'a' 'b' 'c' 'd'
-- result: ["a","ab","abc","abcd","abcda"]
The source code accompanying the HList paper ``Strongly typed
heterogeneous collections'' demonstrates a simular polyvariadic
function hBuild to make heterogeneous lists and records. Not only
hBuild has a variable number of arguments, those
arguments may all have different types.
Literate Haskell code [plain text file]
The complete description of the technique, the explanation
of the type inference for functions with the variable number of
arguments, and many examples.
The code and the explanations were posted in a series of
messages Re: how to write a list builder? fixpoint? on
Haskell and Haskell-Cafe mailing lists on June 1 - 8, 2004.
Strongly typed heterogeneous collections
A poly-variadic function of a non-regular type (Int->)n([]ne)->...
Lambda abstractions in C++ vs. Scheme. Currying
Unexpectedly, the Haskell realization of functions with the
unlimited number of variously typed arguments turns out almost
identical to the implementation of ``currying'' in C++, developed five
years prior.
(Int->)n([]ne)->...This code implements a function for replacing an element in a
multi-dimensional list. The function is overloaded to handle lists of
any dimensions, and so has the variable number of index arguments
specifying the location of the element to replace. The number of index
arguments, of the type Int, must match the dimensionality
of the list. In other words, the desired function has all of
the following signatures all at the same time.
replace :: e -> e -> e -- replacing in a 0-dim list
replace :: Int -> [e] -> e -> [e]
replace :: Int -> Int -> [[e]] -> e -> [[e]]
replace :: Int -> Int -> Int -> [[[e]]] -> e -> [[[e]]]
...
Here e is the type of list elements; the function
returns the updated list. For example,
replace (2::Int) (1::Int) strs 'X' takes the list of strings
and replaces the second character of the third string with the
'X'.
The gist of the solution is the case analysis of the type of function's continuation. Or: bottom-up deterministic parsing of the type of the continuation.
This problem was posed as a `Type class puzzle' by Yitzchak
Gale on the Haskell-Cafe mailing list in Oct 2006. As a matter of
fact, Yitzchak Gale asked for a function with a slightly different
signature, with the different order of the last two arguments, e.g.,
replace :: Int -> Int -> e -> [[e]] -> [[e]], etc. If we consider
the set of the signatures as a language, we notice the problem:
its LALR-like grammar has a shift/reduce conflict. Indeed,
the type of list elements may itself be Int. Thus, after
scanning two Int arguments and looking ahead at another
Int, we cannot tell if we are dealing with the
replacement in a 2D Int list, or the replacement in a
higher-dimensional non-Int list. This problem in the
grammar would compel the use of overlapping instances and other
typeclass tricks. Since the order of replace's last two
arguments seems to have been chosen quite arbitrarily by the
original poster, it makes sense for us to pick the order that
leads to a LALR(1) language and the simple solution, with no need for
overlapping instances.
This puzzle demonstrates the benefits of bringing the tools from quite a different area of computer science -- parsing and grammars -- to seemingly unrelated type class programming. Types and parsing are, of course, deeply related: cf. type logical grammars.
The implementations of replace and the
explanation of the parsing problem and the solutions have been written
by Chung-chieh Shan.
puzzle.hs [3K]
The first, direct-style solution and tests. It is written by Chung-chieh Shan.
puzzle-cps.hs [3K]
Another, continuation-passing-style solution and tests. It is written by Chung-chieh Shan.
We show the Haskell implementation of keyword arguments, which goes well beyond records (e.g., in permitting the re-use of labels). Keyword arguments indeed look just like regular, positional arguments. However, keyword arguments may appear in any order. Furthermore, one may associate defaults with some keywords; the corresponding arguments may then be omitted. It is a type error to omit a required keyword argument. The latter property is in stark contrast with the conventional way of emulating keyword arguments via records. Also in marked contrast with records, keyword labels may be reused throughout the code with no restriction; the same label may be associated with arguments of different types in different functions. Labels of Haskell records may not be re-used. Our solution is essentially equivalent to keyword arguments of DSSSL Scheme or labels of OCaml.
Here's one example: assigning a name to a partially applied keyword argument function without defaults:
tests3 = let f x = kw make_square HNil Color Red x
in f Origin (0::Int,10::Int) Size (1::Int)
The following example illustrates defaults, to be used for omitted keyword arguments:
tests4 = let defaults = Origin .*. (0::Int,10::Int) .*.
RaisedBorder .*. True .*. HNil
in kw make_square defaults Size (1::Int) Color (RGBColor 0 10 255)
The gist of our implementation is a type-level reflection of a function.
Our solution requires no special extensions to Haskell and works with the existing Haskell compilers; it is tested on GHC 6.0.1 and 6.2.1. The overlapping instances extension is not necessary (albeit it is convenient).
Literate Haskell code [plain text file]
The complete description of the technique, and examples.
The code and the explanations were posted in a
message Keyword arguments on a
Haskell mailing list on Fri, 13 Aug 2004 14:58:34 -0700.
Strongly typed heterogeneous collections
The keyword argument code
depends on the HList library, which implements strongly-typed
polymorphic open records. In fact, the keyword argument code
is included as one of the examples in the HList library.
Functions with the variable number of (variously typed) arguments
Macros with keyword (labeled) arguments
Another example of using the ``compile-time'' reflection to
implement keyword arguments. Keyword resolution and argument
re-ordering are done at macro-expand time.
We show how to attain the gist of the restricted datatype proposal (Hughes, 1999) in Haskell, now. We need solely multi-parameter type classes; no functional dependencies, no undecidable instances, let alone more controversial extensions, are required. Restricted monads thus should be implementable in Haskell'.
By definition, monadic operations such as
return :: a -> m a and bind must be fully
polymorphic in the type of the value a associated with
the monadic action m a. Indeed, return must
be a natural transformation. A recurring discussion on Haskell mailing
lists points out the occasional need to restrict that
polymorphism. For example, one of the common implementations of MonadPlus
collects the choices, the results of non-deterministic computations, in a
list. One may wish for a more efficient data structure, such as
Data.Map or a Set. That however
requires the Ord constraint on the values, therefore,
neither Map nor Set may be instances of Monad, let alone
MonadPlus. More examples of restricted monads are discussed in the
article below.
We propose a fully backward-compatible extension to the monadic interface. All monads are members of the extended monads, and all existing monadic code should compile as it is. In addition, restricted monads become expressible. The article defines the extended interface with the functions
ret2 :: MN2 m a => a -> m a
fail2 :: MN2 m a => String -> m a
bind2 :: MN3 m a b => m a -> (a -> m b) -> m b
which have exactly the same type as the ordinary monadic operations
-- only with more general constraints. Because
new operations have exactly the same type, one may use them in the
regular monadic code (given -fno-implicit-prelude flag) and with the
do-notation (cf. `rebindable syntax' feature). Perhaps one day this
more general interface becomes the default one.
The gist of our proposal is the splitting of the Monad class into
two separate classes, MN2 for return and
fail and MN3 for bind. The
latter class implies the former. The new classes explicitly mention
the type of the monadic action value in their interface. That makes it
possible to attach constraints to those types. The article shows
the attaching of the Ord constraint, so to make Set an
instance of Monad and MonadPlus.
RestrictedMonad.lhs [4K]
The literate Haskell source code and a few tests
The code was originally posted as Restricted Data Types Now on the Haskell' mailing list on Wed, 8 Feb 2006 00:06:23 -0800 (PST)
DoRestrictedM.hs [3K]
The illustration of the do-notation for restricted monads, which
works already for GHC 6.6 and later. We demonstrate that the
do-notation works uniformly for ordinary monads and restricted monads.
We show the conventional-looking monadic code which nevertheless
uses Data.Set as the implementation
of MonadPlus -- a frequently requested feature.
John Hughes: Restricted datatypes in Haskell.
Haskell 1999 Workshop, ed. Erik Meijer. Technical Report UU-CS-1999-28, Department of Computer Science, Utrecht University.
<http://www.cs.chalmers.se/~rjmh/Papers/restricted-datatypes.ps>
We describe a datatype of polymorphic balanced binary trees: AVL trees. The trees are polymorphic: the values in different nodes may have different type. The trees are balanced: for each non-leaf node, the heights of its two children can differ at most by one. Here, by definition the height of a node is 1 + max of the heights of its children. A leaf node has the height of 0.
The main feature of the present approach is a blended static
and dynamic enforcement of the balancing constraint. The function
make_node verifies the balancing constraint at compile time
-- if it can. If the static check is not possible, the function delays
the check till the run-time.
A detailed follow-up message by Chris Okasaki describes a very interesting representation of AVL trees with the balancing constraint ensured statically by a type-checker.
stanamically-balanced-trees.lhs [12K]
The literate Haskell source code and a few tests
The code was originally posted as Polymorphic stanamically balanced binary trees on Haskell mailing list on Sun, 20 Apr 2003 15:25:12 -0700 (PDT)
Christopher Okasaki. A follow-up message posted on
Haskell mailing list on Mon, 28 Apr 2003 08:34:37 -0400
<http://www.haskell.org/pipermail/haskell/2003-April/011693.html>
The regular (full) signature of a function specifies the type of the function and -- if the type includes constrained type variables -- enumerates all of the typeclass constraints. The list of the constraints may be quite large. Partial signatures help when:
Contrary to a popular belief, both of the above are easily possible, in Haskell98.
How to make a function strict without changing its body
Another application of the trick of adding a clause with an
always failing guard
There is a view that in order to gain static assurances such as an
array index being always in range or tail being applied to a
non-empty list, we must give up on something significant: on data
structures such as arrays (to be replaced with nested tuples), on
general recursion, on annotation-free programming, on clarity of code,
on well-supported programming languages. That does not have to be the
case. The present messages show non-trivial examples involving native
Haskell arrays, index computations, and general recursion. All arrays
indexing operations are statically guaranteed to be safe -- and so we
can safely use an efficient unsafeAt provided by GHC seemingly for
that purpose. The code is efficient; the static assurances cost us no
run-time overhead. The example uses only Haskell98 + higher-ranked
types. No new type classes are introduced. The safety is based on:
Haskell type system, quantified type variables, and a compact
general-purpose trusted kernel.
This message has been inspired by the work of Hongwei Xi and his initiated movement to make dependent-type programming practical. The influence of his famous PLDI98 paper should be obvious. We should note the parallels between dependent type annotations in Hongwei Xi's Dependent SML code and the corresponding Haskell code. What Hongwei Xi expressed in types, our code expressed in terms. The terms were specifically designed in such a way so that consequences of various tests be visible to the type system, and so the corresponding conclusions could be propagated as part of the regular type inference. There is a trusted kernel involved -- just as the Dependent SML system has to be implicitly trusted. However, in the given example the trusted kernel is a compact Haskell code plus the GHC system. The latter is complex -- but it is being used by thousands of people over extended period of time -- and so has higher confidence than experimental extensions (unless the code of the latter has been formally proven by a trusted system such as ACL2 or Coq).
In the discussion thread, Conor T. McBride has made an
excellent summary of this approach and its relation to genuine
dependent types: ``The abstract brand is just a type-level
proxy for the bounding interval, and the library of operations
provides interval-respecting operations on indices. This is a very
neat solution in Haskell, but it goes round an extra corner which
isn't necessary with dependent types, where you can just talk about
the interval directly. The library-writer would develop and verify the
same convenient operations for working with intervals and indices; the
proofs would be independently recheckable terms in type theory.''
Our most complex example is folding over multiple, variously-sized arrays. This is like a fold over an array -- generalized to an arbitrary number of arrays, whose lower and upper index bounds may differ. The index ranges of some arrays do not even have to overlap and may be empty. Neither the number of arrays to process nor their index bounds are statically known. And yet we can statically guarantee that whenever our code accesses any array element, the index is certainly within the bounds of that array. Typing this example in a genuinely dependent type system is probably going to be quite challenging.
eliminating-array-bound-check.lhs [9K]
The literate Haskell code with explanations and the examples
The first version of the code was originally posted as Eliminating Array Bound Checking through Non-dependent types on the Haskell mailing list on Thu, 5 Aug 2004 19:31:36 -0700. The current version corrects the problem pointed out by Conor T.
McBride in the discussion thread.
Hongwei Xi and Frank Pfenning: Eliminating Array Bound Checking Through Dependent Types (PLDI'98)
The famous paper introducing practical dependent type system as
a dialect of SML. We faithfully re-implement the bsearch
example from that paper in Haskell98 plus higher-ranked types.
Additional explanation of the branding technique [plain text file]
and the response to the questions by Bjorn Lisper about the
relationship to classical range analyses known for a long time for
imperative languages. Verification of the library (perhaps using
Presburger solvers like the Omega Test by Bill Pugh) were also touched
upon.
The message was originally posted as Re: [Haskell] Eliminating Array Bound Checking through
Non-dependent types on the Haskell mailing list on Sun, 8 Aug 2004 16:50:33 -0700
eliminating-mult-array-bound-check.lhs [13K]
Eliminating Multiple-Array Bound Checking through
Non-dependent types
A message posted on the Haskell mailing list on Fri, 10 Feb 2006 22:05:04 -0800 (PST).
Number-parameterized types and decimal type arithmetic
Lightweight Dependent-type Programming
Extensive discussion with Conor T. McBride, with his many
insights and explanations of dependent-type programming. Haskell
mailing list, August 6-9, 2004.
<http://www.haskell.org/pipermail/haskell/2004-August/014399.html>
<http://www.haskell.org/pipermail/haskell/2004-August/014403.html>
<http://www.haskell.org/pipermail/haskell/2004-August/014405.html>
appendThe subject of these article is ``heavier-weight'' dependent-type programming: using the type system to state and guarantee non-trivial properties of terms. Unlike the lightweight approach, we do not resort to a user-supplied trusted kernel: rather, we exclusively rely on the type system.
The poster problem for dependent types is to write a function to append two lists that statically assures that the size of the output list is the sum of the sizes of the two input lists. The lists must therefore be described by a (dependent) type that carries the size of the list.
Martin Sulzmann, in a message on the Haskell list, has posed the problem and gave its solutions:
E). Rather, we base our trust on the Haskell type system only.
The solutions demonstrate two different levels of dependent
typing. In both cases, we formulate the desired properties using
dependent types, and attach them as signatures to functions. We may
regard these dynamically-typed signature as ``compile-time
assertions''. If the use of our function in a particular expression
violates the assertion, the expression is flagged as ill-typed. In a
semi-dynamic case, a run-time check is inserted. If a program
compiled, it does not mean that append truly respects the sum-of-sizes
constraint. It merely means that in this particular compilation unit,
all the uses of append were statically found to respect the length
constraint. The more powerful approach, exhibited in Epigram, is to
say that in all possible compilations append
shall be found to satisfy the length constraint.
Thus, at one level of dependent typing, assertions about a particular function are checked at the usage occurrences of that function, within the particular context of those occurrences. A far more stronger level of dependent typing guarantees that the assertions hold universally, in all possible contexts. That level checks the definition of the function. The difference between the levels is akin to the difference between `dynamic' and `static' typing, but only at the compile-time.
Both approaches are useful. Incidentally, GHC already does ``dynamic kinding'' with respect to typeclass instances: the mere fact that a program unit has compiled does not assure us that all defined instances are problem-free (e.g., non-overlapping). It simply means that the uses of instances within the programming unit in question were problem-free.
dependently-typed-append.lhs [5K]
The literate Haskell code with explanations and the examples
The first version of the code was posted as Re: Dependent Types in Haskell on the Haskell mailing list on Sat, 14 Aug 2004 03:10:04 -0700.
Martin Sulzmann: Dependent Types in Haskell
<http://www.haskell.org/pipermail/haskell/2004-August/014407.html>
<http://www.haskell.org/pipermail/haskell/2004-August/014408.html>
Messages on the Haskell mailing list posted on
Wed Aug 11 2004.
Conor T McBride: Dependent Types in Haskell
<http://www.haskell.org/pipermail/haskell/2004-August/014412.html>
Message on the Haskell mailing list posted on
Wed Aug 11 05:00:25 EDT 2004.
Eliminating Array Bound Checking through Non-dependent types
undefined to definedThis message shows how to make the Haskell typechecker work in reverse: to infer a term of a given type:
rtest4 f g = rr (undefined::(b -> c) -> (a -> b) -> a -> c) HNil f g
*HC> rtest4 (:[]) Just 'x'
[Just 'x']
*HC> rtest4 Just Right True
Just (Right True)
We ask the Haskell typechecker to derive us a function of the
specified type. We get the real function, which we can then apply to
various arguments. The return result does behave like a `composition'
-- which is what the type specifies. Informally, we converted from
undefined to defined.
It must be emphasized that no modifications to the Haskell
compiler are needed, and no external programs are relied upon. In
particular, however surprising it may seem, we get by without eval -- because Haskell has reflexive facilities already
built-in.
Our system solves type habitation for a class of functions with polymorphic types. From another point of view, the system is a prover in the implication fragment of intuitionistic logic. Essentially we turn a type into a logical program -- a set of Horn clauses -- which we then solve by SLD resolution. It is gratifying to see that Haskell typeclasses are up to that task.
The message below presents two different converters from a type to a term. Both derive a program, a term, from its specification, a type -- for a class of fully polymorphic functions. The first converter has just been demonstrated. It is quite limited in that the derived function must be used `polymorphically' -- distinct type variables must be instantiated to different types (or, the user should first instantiate their types and then derive the term). The second converter is far more useful: it can let us `visualize' what a function with a particular type may be doing. For example, it might not be immediately clear what is the function of the type
(((a -> b -> c) -> (a -> b) -> a -> c) -> (t3 -> t1 -> t2 -> t3) -> t) -> t)Our reifier says,
test9 = reify (undefined::(((a -> b -> c) -> (a -> b) -> a -> c) ->
(t3 -> t1 -> t2 -> t3) -> t) -> t) gamma0
*HC> test9
\y -> y (\d h p -> d p (h p)) (\d h p -> d)
that is, the function in question is one of the X combinators. It is
an improper combinator. Similarly the reifier can turn a point-free
function into the pointful form to help really understand the
former. For example, it might take time to comprehend the following
expression:pz = (((. head . uncurry zip . splitAt 1 . repeat) . uncurry) .) . (.) . flipOur system says
test_pz = reify (undefined `asTypeOf` pz) gamma0
*HC> test_pz
\h p y -> h y (p y)
So, pz is just the S combinator.
An attempt to derive a term for the type a->b
expectedly fails. The type error message essentially says that a |- b is underivable.
The examples above exhibit fully polymorphic types -- those with uninstantiated, implicitly universally quantified type variables. That is, our typeclasses can reify not only types but also type schemas. The ability to operate on and compare unground types with uninstantiated type variables is often sought but rarely attained. The contribution of this message is the set of primitives for nominal equality comparison and deconstruction of unground types.
de-typechecker.lhs [20K]
The literate Haskell code with extensive explanations and many
examples, including the code and explanation for the Equality
predicate on type schemas.
The code was originally posted as De-typechecker: converting from a type to a term on the Haskell mailing list on Tue, 1 Mar 2005 00:13:08 -0800 (PST)
Lennart Augustsson: Announcing Djinn, version 2004-12-11, a coding wizard
<http://www.haskell.org/pipermail/haskell/2005-December/017055.html>
A Message posted on the Haskell mailing list on Sun Dec 11
17:32:07 EST 2005.
The user types a Haskell type at DJinn's prompt, and DJinn gives
back a term of that type if one exists. The produced term is in
DJinn's term language. The printed term can be cut and pasted into the
Haskell code.
pointless-translation.lhs [6K]
The literate Haskell98 code for translating proper linear
combinators into point-free style.
The code was originally posted as Automatic pointless translation on the Haskell-Cafe mailing list on Mon, 14 Feb 2005 22:56:04
-0800 (PST)
The 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.
Joint work with Chung-chieh Shan.
Proceedings of the ACM SIGPLAN 2004 workshop on Haskell
Snowbird, Utah, USA -- September 22, 2004 --
ACM Press, pp. 33 - 44.
Expanded version: Technical report TR-15-04, Division of Engineering and Applied Sciences, Harvard University.
A heterogeneous collection is a datatype that is capable of storing data of different types, while providing operations for look-up, update, iteration, and others. There are various kinds of heterogeneous collections, differing in representation, invariants, and access operations. We describe HList --- a Haskell library for strongly typed heterogeneous collections including extensible records. We illustrate HList's benefits in the context of type-safe database access in Haskell. The HList library relies on common extensions of Haskell 98. Our exploration raises interesting issues regarding Haskell's type system, in particular, avoidance of overlapping instances, and reification of type equality and type unification.
Joint work with Ralf Laemmel and Keean Schupke.
Proceedings of the ACM SIGPLAN 2004 workshop on Haskell
Snowbird, Utah, USA -- September 22, 2004 --
ACM Press, pp. 96 - 107.
Expanded version: CWI Technical report SEN-E0420, ISSN 1386-369X, CWI, Amsterdam, August 2004.
We show invertible, terminating, 3-place addition, multiplication, and exponentiation relations on type-level unary, Peano numerals, where any two operands determine the third. We also show the invertible factorial relation. This gives us all common arithmetic operations on Peano numerals, including n-base discrete logarithm, n-th root, and the inverse of factorial. The latter operations and division are defined generically, as inverses of exponentiation, factorial and multiplication, resp. It takes only a couple of lines to define each. The inverting method can work with any representation of (type-level) numerals, binary or decimal.
The inverter itself is generic: it is a type-class function, that is, a type-class parameterized by the type-class to `invert'. The inverter is a simple higher-order for-loop on types. There has been a proposal on Haskell' to give equal rights to types and classes. In Haskell98+multi-parameter type classes, classes are already first-class, for all practical purposes. We can easily define (potentially, higher-order) type functions on type classes.
It becomes relatively straightforward then to implement RSA in types. That prompted Graham Klyne to remark on Haskell Cafe `` Methinks this gives a whole new meaning to "type security"''
We introduce the type-level Haskell library for arbitrary
precision binary arithmetic over natural kinds. The library
supports addition/subtraction, predecessor/successor,
multiplication/division, exp2, all comparisons, GCD, and the maximum.
At the core of the library are multi-mode ternary relations
Add and Mul where any two
arguments determine the third. Such relations are especially suitable
for specifying static arithmetic constraints on computations. The
type-level numerals have no run-time representation; correspondingly,
all arithmetic operations are done at compile time and have no effect
on run-time.
Here are the definitions of the well-formedness condition on binary type numerals -- the kind predicate -- and of a few operations on them:
class Nat0 a where toInt :: a -> Int
class Nat0 a => Nat a -- (positive) naturals
class (Nat0 x, Nat y) => Succ x y | x -> y, y -> x
-- GCD over natural _kinds_
class (Nat0 x, Nat0 y, Nat0 z) => GCD x y z | x y -> z
The numerals are specified in the familiar big-endian bit
notation. The sequence of B0s and B1s is the
bit-string of the number, whereas the number of Us is the
binary logarithm. type N2 = U B1 B0; nat2 = undefined::N2
type N4 = U (U B1 B0) B0; nat4 = undefined::N4
add :: Add x y z => x -> y -> z; add = undefined
sub :: Add x y z => z -> x -> y; sub = undefined
mul :: Mul x y z => x -> y -> z; mul = undefined
div :: Mul x y z => z -> x -> y; div = undefined
*BinaryNumber> :type mul (add nat2 nat4) (succ nat2)
mul (add nat2 nat4) (succ nat2) :: U (U (U (U B1 B0) B0) B1) B0
*BinaryNumber> :type div (add nat2 nat4) (succ nat2)
div (add nat2 nat4) (succ nat2) :: U B1 B0
*BinaryNumber> :type gcd (add nat2 nat4) (succ nat2)
gcd (add nat2 nat4) (succ nat2) :: U B1 B1
We stress that all multiplication, GCD, etc. computations above are
performed as part of type checking: the reported numeral is the type of the expression. The expression's value is undefined: despite the familiar term-level notation,
expressions like (add nat2 nat4) are meant to be
evaluated at compile time and have no executable content. Also despite
the familiar functional term-level notation, the type computations are
invertible. We may ask, for example, what must be the type
of x such that multiplying it by three gives six: x = undefined where _ = mul x (succ nat2) `asTypeOf` (add nat2 nat4)
*BinaryNumber> :type x
x :: U B1 B0
We used the arithmetic type library to statically enforce validity, range, size, and alignment constraints of raw memory pointers, and to statically enforce protocol and time-related constraints when accessing device registers. Our paper `Lightweight static resources' describes the arithmetic type library, type-level records, type-level programming with regular Haskell terms, and two sample applications.
Joint work with Chung-chieh Shan.
BinaryNumber.hs [10K]
The commented Haskell source code with tests
Lightweight static resources, for safe embedded and systems programming
[The abstract]
It is an established trend to develop low-level code --
embedded software, device drivers, and operating systems -- using
high-level languages, especially functional languages with advanced
facilities to abstract and generate code. To be reliable and secure,
low-level code must correctly manage space, time, and other resources,
so special type systems and verification tools arose to regulate
resource access statically. However, a general-purpose functional
language practical today can provide the same static assurances, also
without run-time overhead. We substantiate this claim and promote the
trend with two security kernels in the domain of device drivers:
Joint work with Chung-chieh Shan.
tfp.pdf [129K]
Proc. Trends in Functional Programming. New York, Apr 2-4, 2007.
Chung-chieh Shan: TFP 2007 talk, Apr 3, 2007.
<http://www.cs.rutgers.edu/~ccshan/tfp2007/talk.pdf>
BinaryNumber.hs [10K]
Representation of binary numbers and arithmetic relations
Areas.hs [20K]
Strongly typed memory areas. The implementation of the library
AreaTests.hs [4K]
Sample strongly typed memory areas and examples of type records
VideoRAM.hs [5K]
Extensive example of strongly typed memory areas: safe and efficient
access to videoRAM, with casts, pointer arithmetic and iterations
RealTime.hs [8K]
Statically tracking ticks: enforcing timing and protocol
restrictions when writing device drivers and their generators
This message gives an example of a dynamic type class cast in Haskell. We want to dispatch on a class of a type rather on
a type itself. In other words, we would like to simulate IsInstanceOf. The problem was originally posed by Hal Daume III,
who wrote on the Haskell mailing list:
i'm hoping to be able to simulate a sort of dynamic dispatch
based on class instances. basically a function which takes a value
and depending on what classes it is an instance of, does
something. I've been trying for a while to simulate something along
the lines of: class Foo a where { foo :: a -> Bool }
class Bar a where { bar :: a -> Bool }
foo x
| typeOf x `instanceOf` Foo = Just (foo x)
| typeOf x `instanceOf` Bar = Just (bar x)
| otherwise = Nothing
The following code shows how to implement a dynamic dispatch on a type class context. No unsafe operations are used. The test at the end demonstrates that we can indeed simulate Hal's desired example.
class-based-dispatch.lhs [4K]
The literate Haskell source code and a test
The code was originally posted as simulating dynamic dispatch on the Haskell mailing list on Sun, 23 Mar 2003 13:41:48
Hal Daume III. simulating dynamic dispatch. The message with
the statement of the problem, posted on the Haskell mailing list on on Mar
20, 2003.
<http://www.haskell.org/pipermail/haskell/2003-March/011518.html>
On a simple example we demonstrate that the type system of Haskell with the common rank-2 extension (not counting the extensions in GHC 6.6) is already impredicative, and it permits explicit type, i.e., big-lambda and type applications. This note is based on a message by Shin-Cheng Mu from Feb 2005, and comments by Simon Peyton-Jones and Greg Morrisett. We add the observation that big lambda and type applications are in fact present in Haskell and can be explicitly used by programmers.
Polymorphic types in Haskell can only be instantiated with monomorphic types. In other words, a type variable ranges over ground types, which do not (overtly -- see below) contain quantified type variables. In particular, in the following polymorphic type definition (of Church numerals)
type M = forall a . (a -> a) -> a -> athe type variable
a cannot be instantiated with the type
M itself. This so-called predicativity prevents defining
a type implicitly in terms of itself. This property significantly
simplifies type inference; otherwise, unification, typically used to
solve type equations, becomes higher-order, which is in general
undecidable. The restriction that polytypes can only be instantiated
with monotypes is responsible for the rejection of intuitively correct
programs and seemingly makes Haskell unable to faithfully reproduce
second-order lambda calculus. Shin-Cheng Mu showed the simple example
of that, arithmetic of Church numerals: zero :: M; zero = \f a -> a
succ :: M -> M; succ n = \f a -> f (n f a)
add, mul :: M -> M -> M
add m n = \f a -> m f (n f a)
mul m n = \f a -> m (n f) a
exp, exp2 :: M -> M -> M
exp m n = n (mul m) one
exp2 m n = n m
This program typechecks -- with the sole exception of exp. This may seem surprising as the equivalent exp2 is
accepted by the typechecker. Shin-Cheng Mu pointed out that if we
write exp and exp2 with the explicit big
lambda (denoted ?x -> term) and type application (to be denoted
term[type]) exp (m::M) (n::M) = n [M] ((mul m)::M->M) (one::M)
exp2 (m::M) (n::M) = ?b -> \(f::(b->b)) -> n[b->b] (m[b]) f
then we observe that exp instantiates the polymorphic
term n with the polymorphic type M -- which
is prohibited in Haskell. Hence the typechecker complains, with a
rather uninformative message ``Inferred type is less polymorphic than
expected. Quantified type variable `a' escapes.'' The term exp2 is accepted since the argument b of the
type-lambda is assumed monotype.
The above notation for explicit type-level abstractions and
applications is not Haskell. Or is it? It turns out, the introduction
and elimination of big lambda is already part of Haskell. We can use
them to guide the typechecker when instantiating polytypes with
polytypes -- which is too effectively possible. Our guidance makes the
inference decidable. As Greg Morrisett pointed out on the discussion thread,
Haskell is impredicative: ``You can instantiate a type variable with a
newtype that contains a polymorphic type...
GHC enforces a sub-kind constraint on variables that precludes them
from ranging over types whose top-most constructor is a
forall (and has a few more structural constraints.) The distinction is subtle,
but important. A predicative version of Haskell would have a much,
much simpler denotational semantics, but also prevent a number of
things that are useful and interesting.'' Indeed, we can write
exp after all:
newtype N = N{un:: forall a . (a -> a) -> a -> a}
zero :: N; zero = N ( \f a -> a )
succ :: N -> N; succ n = N ( \f a -> f (un n f a) )
exp, exp2 :: N -> N -> N
exp m n = un n (mul m) one
exp2 m n = N (\f a -> un n (un m) f a)
We should compare exp and exp2 code here
with the explicit type lambda code above. Where we had ?t we have N, and where we had term[t] before we have
un term now. Thus N and un act
as -- mark the places of -- big lambda introduction and
elimination. The notation this time is Haskell. Wrapping polymorphic
types in newtype such as N also permits easy, nominal rather than
structural, equality of polymorphic types.
In this code, one may not replace N (...) with
N $ (...). This is yet another case where ($) is not the same as application with a lower precedence.
Shin-Cheng Mu. Re: Polymorphic types without type constructors? A message that started the discussion, posted on the Haskell mailing list on Tue Feb 1 22:36:00 EST 2005
numerals-second-order.hs [2K]
The complete code of the example, which compiles with Hugs,GHC 6.6. and pre-GHC 6.6.
The code was originally posted on the above discussion thread on Tue Feb 1 22:36:00 EST 2005
Simon Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, and Mark Shields: Practical type inference for arbitrary-rank types. To appear in the Journal of Functional Programming.
<http://research.microsoft.com/Users/simonpj/papers/higher-rank/index.htm>
Didier Le Botlan, Didier Remy: Raising ML to the Power of System F. ICFP 2003.
<http://citeseer.ist.psu.edu/lebotlan03raising.html>
An attempt to implement the following categorical formulas in Haskell:
max3 = max2 . (max2 * id)
max4 = max2 . (max2 * max2)
max5 = max2 . ((max2 * id) . (max2 * max2))
max7 = max3 . ((max2 * max3) * max2)
where * is a categorical product and .
is a categorical composition. We show the code for the product and the
composition that lets us write the above formulas in Haskell as they
are.
A potentially useful side-effect is an automatic deep uncurrying of
arbitrarily complex pairs, such as ((1,2),(3,(4,5)))
Literate Haskell code [plain text file]
The complete description and the implementation. It was posted as Deeply uncurried products, as
categorists might like them on a Haskell mailing list on Apr 30,
2003.
An older approach [plain text file]
It was originally posted as Re: On products and
max3 on a newsgroup comp.lang.functional on Thu, 12
Apr 2001 02:14:27 +0000
The class Typeable provides run-time representation of types and a
type-safe cast operation. According to the documentation,
``To this end, an unsafe cast is guarded by a test for type (representation)
equivalence.'' Alas, that test is trivial to fake, which gives us the
total function of the inferred type a->b. This unsound cast can indeed lead to the Segmentation
fault.
module C where
import Data.Typeable
import Data.Maybe
newtype W a = W{unW :: a}
instance Typeable (W a) where typeOf _ = typeOf ()
bad_cast x = unW . fromJust . cast $ W x
-- inferred type: bad_cast :: a -> b
test1 = bad_cast True ++ ""
When we load the above Haskell98 code in GHCi and try to evaluate
test1 (which casts a boolean to a string), we see: $ ghci /tmp/c.hs
Loading package base ... linking ... done.
[1 of 1] Compiling C ( /tmp/c.hs, interpreted )
Ok, modules loaded: C.
*C> test1
segmentation fault: 11
We show the implementation of the State monad as a term algebra. We represent monadic computation by a term built from the following constructors:
data Bind t f = Bind t f
data Return v = Return v
data Get = Get
data Put v = Put v
For example, the term Get `Bind` (\v -> Put (not v) `Bind` (\() -> Return v)) denotes the action of negating the current state and returning
the original state.runst :: RunState t s a => t -> s -> (s, a)The function
runst is the observer of our
terms, or the interpreter of monadic actions. Given the term t and the initial state of the type s, the function
interprets Get, Bind, etc. actions and
returns the final state and the resulting value. The type of the
result, a, is uniquely determined by the term and the state. The
only non-trivial part is the interpretation of Bind, due to the
polymorphism of the monadic bind operation. We use an auxiliary class
RunBind for that purpose.
For completeness, we show that our term representation of
state monadic actions is an instance of MonadState. We can then use the familiar notation to write our sample term
above:
do{v <- get; put (not v); return v}
Our implementation statically guarantees that only well-formed and well-typed terms can be evaluated.
This article describes a combinator mcomp that does
the farthest composition of functions:
f:: a1->a2-> .... ->cp
g:: cp->d
f `mcomp` g:: a1->a2-> .... ->d
We resolve the ambiguity in the above definition by assuming
that cp is not a functional type.
The problem was originally posed on comp.lang.functional by Immanuel Litzroth, who wrote:
The problem arose quite naturally when I was working on something todo with partial orderPO:: A -> B -> Maybe Orderingand now I wantedgroupBy (isJust . PO)
polyvar-comp.lhs [3K]
The literate Haskell source code and a few tests
The code was originally posted as Re:
composition on a newsgroup comp.lang.functional on
Wed, 30 Oct 2002 19:09:32 -0800
Categorical products in Haskell
Another application of the combinator mcomp
This site's top page is http://pobox.com/~oleg/ftp/
Converted from SXML by SXML->HTML