Haskell Programming: Attractive Types

Haskell has become a laboratory and playground for advanced type hackery
Simon Peyton Jones: Wearing the hair shirt: a retrospective on Haskell. POPL 2003, invited talk.

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


 

Restricted Monads

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.

Version
The current version is 1.1, Feb 8, 2006.
References

CPS-transforming a restricted monad to the ordinary one

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>

 

Polymorphic stanamically balanced AVL trees

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.

Version
The current version is 1.5, Apr 26, 2003.
References

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>

 

Partial signatures

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.

Version
The current version is 1.1, Aug 6, 2004.
References
partial-signatures.lhs [3K]
The literate Haskell code with explanations and the examples
The code was originally posted as Partial signatures on Haskell-Cafe mailing list on Fri, 6 Aug 2004 20:29:40 -0700 (PDT)

How to make a function strict without changing its body
Another application of the trick of adding a clause with an always failing guard

 

Eliminating Array Bound Checking through Non-dependent types

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.

References

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>

Dependently-typed append

 

Dependently-typed append

The 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:

Conor McBride showed the solution in Epigram. The present article gives a Haskell solution, which makes an extensive use of partial signatures and, in general, relies on the compiler to figure out the rest of the constraints. We also separate the skeleton of the list from the type of the list elements. Unlike the proof-term solution given in Martin Sulzmann's message, we do not rely on any trusted kernel (that is, the specially-constructed equality datatype 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.

References

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

 

Reversing Haskell typechecker: converting from undefined to defined

This 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) .) . (.) . flip
Our 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.

Version
The current version is 1.1, Mar 1, 2005.
References

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)

 

Implicit configurations -- or, type classes reflect the values of types

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.

Version
The current version is 1.1, Aug 2004.
References

tr-15-04.pdf [252K]
Technical report TR-15-04, Division of Engineering and Applied Sciences, Harvard University
This is the expanded version of the paper, with extra appendices.
The original paper was published in theProceedings of the ACM SIGPLAN 2004 workshop on Haskell
Snowbird, Utah, USA -- September 22, 2004 -- ACM Press, pp. 33 - 44.

Prepose.hs [10K]
The complete code for the paper, updated for the current GHC

 

Strongly typed heterogeneous collections

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 open, extensible records with first-class, reusable, and compile-time only labels. HList also includes the dual of records: extensible polymorphic variants, or open unions. HList lets the user formulate statically checkable constraints: for example, no two elements of a collection may have the same type (so the elements can be unambiguously indexed by their type).

We and others have used HList for type-safe database access in Haskell. HList-based Records form the basis of OOHaskell. HList is being used in AspectAG, typed EDSL of attribute grammars, and in HaskellDB. The HList library relies on common extensions of Haskell 2010. 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.

The October 2012 version marks the beginning of the significant re-write to take advantage of the fancier types offered by GHC 7.4+. HList now relies on native type-level booleans, natural numbers and lists, and on kind polymorphism. A number of operations are implemented as type functions. Another notable addition is unfold for heterogeneous lists, used to implement projections and splitting. More computations are moved to type-level, with no run-time overhead.

Version
The current version is October 2012.
References

<http://code.haskell.org/HList/>
<http://code.haskell.org/HList/ChangeLog>
<http://hackage.haskell.org/package/HList>
<http://homepages.cwi.nl/~ralf/HList/>

Proceedings of the ACM SIGPLAN 2004 workshop on Haskell
Snowbird, Utah, USA -- September 22, 2004 -- ACM Press, pp. 96 - 107.

HList-ext.pdf [166K]
Expanded version: CWI Technical report SEN-E0420, ISSN 1386-369X, CWI, Amsterdam, August 2004.

 

Binary type arithmetic

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.

Version
The current version is 1.1, Feb 2, 2007.
References

BinaryNumber.hs [10K]
The commented Haskell source code with tests

Lightweight static resources, for safe embedded and systems programming

 

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:

Our style is convenient in Haskell thanks to custom kinds and predicates (as type classes); type-level numbers, functions, and records (using functional dependencies); and mixed type- and term-level programming (enabling partial type signatures).

Joint work with Chung-chieh Shan.

Version
The current version is 1.1, Feb 2, 2007.
References

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

Tracking dynamic values in types: safe locking

 

Many ways to the fix-point combinator besides the value recursion

Value-level recursion in Haskell is built-in since definitions are implicitly recursive. The explicit polymorphic fix-point combinator can therefore be defined simply as

     fix :: (a -> a) -> a
     fix f = f (fix f)
Had the value-level recursion been unavailable, we still could have safely defined the polymorphic fix-point combinator in Haskell. In fact, in five different ways, without ever resorting to unsafe operations. Iso-recursive data types are a well-known way to fix. Less known is using type classes or families. The lazy ST approach is most puzzling: the reading of a reference cell appears to occur in pure code.

Uncharitably speaking, Haskell, taken as a logic, is inconsistent in more than two ways.

Version
The current version is 1.0, May 2010.
References

Fix.hs [3K]
The complete Haskell code and the tests

All the ways to express the polymorphic fixpoint operator in OCaml

 

Impredicativity and explicit type applications

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 -> a
the 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.

Version
The current version is 1.1, Feb 1, 2005.
References

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>

 

Applications of computable types

We have previously introduced a functional language for computing types and implemented it with Haskell type classes. The implementation is trivial because it relies on the type checker to do all the work. We now demonstrate the applications of computable types, to ascribe signatures to terms and to drive the selection of overloaded functions. One example computes a complex XML type, and instantiate the read function to read the trees of only that shape.

We have implemented Cardelli's example, the type function Prop where Prop(n) is the type of n-ary propositions. For example, Prop(3) is the type Bool -> Bool -> Bool -> Bool. By composing the type functions Prop and Fib we obtain the type function StrangeProp of the kind NAT -> Type: StrangeProp(n) is the type of propositions of arity m, where m is fib(n). We use not only (a->) but also (->a) as unary type functions. The former is just (->) a. The latter is considered impossible. In our approach, (->a) is written almost literally as (flip (->) a).

We demonstrate two different ways of defining type-level abstractions: as `lambda-terms' in our type-level calculus (i.e., types of the form (F t)) and as polymorphic types, Haskell's native type abstractions. The two ways are profoundly related, by the correspondence between type abstraction/instantiation and functional abstraction/application.

Version
The current version is 1.1, Sep 14, 2006.
References

TypeFN.lhs [8K]
The literate Haskell code of type functions and their applications
It was posted as On computable types. II. Flipping the arrow on the Haskell mailing list on Thu, 14 Sep 2006 19:37:19 -0700 (PDT).

TypeLC.lhs [9K]
Lambda-calculator on types: writing and evaluating type-level functions
A type-level functional language with the notation that resembles lambda-calculus with case distinction, fixpoint recursion, etc. Modulo a bit of syntactic tart, the language of the type functions even looks almost like the pure Haskell.

Luca Cardelli: Phase Distinctions in Type Theory.
Unpublished manuscript, 1988.
<http://lucacardelli.name/Papers/PhaseDistinctions.pdf>

Simon Peyton Jones and Erik Meijer: Henk: A Typed Intermediate Language.
<http://www.research.microsoft.com/~simonpj/Papers/henk.ps.gz>

 

Translucent applicative functors

ML is known for its sophisticated, higher-order module system, one of the most interesting examples of which is a translucent applicative functor such as SET parameterized by the element-comparison function. If we make two instances of the SET with the same (>) comparison on integers, we can take an element from one set and put in in the other: the element types are `transparent' and the compiler can clearly see they are both integers. We can also take a union of the two sets. The type of the set itself is opaque -- set values can only be manipulated by the operations of SET. Now the compiler cannot see the concrete representation of the set types and verify they are the same. The compiler knows however that instantiations of SET with the identical element comparisons are type-compatible.

It turns out translucent functors can be implemented in Haskell idiomatically, taking the full use of type classes. We also show that type sharing constraints can be expressed in a scalable manner, so that the whole translation is practically usable. Thus we demonstrate that Haskell already has a higher-order module language. No new extensions are required; furthermore, we avoid even undecidable let alone overlapping instances.

In the process of translating OCaml module expressions into Haskell, we have noted several guidelines:

In our experience these guidelines are also useful when translating from Haskell to OCaml.
References

TranslucentAppFunctor.lhs [18K]
The article with the juxtaposed literate Haskell and OCaml code
It was posted as Applicative translucent functors in Haskell on the Haskell mailing list on Fri, 27 Aug 2004 16:51:43 -0700 (PDT).

Chung-chieh Shan. Higher-order modules in System F-omega and Haskell
<http://www.cs.rutgers.edu/~ccshan/xlate/xlate.pdf>

Stefan Wehr and Manuel M. T. Chakravarty. ML Modules and Haskell Type Classes: A Constructive Comparison
Proc. Sixth Asian Symposium on Programming Languages and Systems. LNCS 5356, Springer, 2008.
<http://www.informatik.uni-freiburg.de/~wehr/publications/WehrChakravarty2008.html>

 

ML-style modules with type sharing by name

This second article on higher-order module programming in Haskell deals with type-equality, or sharing constraints. Recall a module is a collection of type and value definitions. Here is an example, in OCaml notation.

      module TIF = struct
         type a = int
         type b = float
         let  app x = float_of_int x
       end
The module interface can be described by the following signature (module type)
     module type FN = sig
       type a
       type b
       val app  : a -> b
     end

A higher-order module, a functor, is a module parameterized by other modules, such as the following module that composes two instances of FN:

     module Compose(L: FN)(R: (FN with type a = L.b)) = struct
       type a = L.a
       type t = L.b
       type b = R.b
       let  app x = R.app (L.app x)
     end
The composition of the R.app function with L.app is well-typed only when the result type of L.app is the same as the argument type of the R.app. Since these types (namely, L.b and R.a) are abstract, the compiler cannot know if they are the same. We have to specify the type equality L.b = R.a as a sharing constraint: (R: (FN with type a = L.b)).

The naive implementation of sharing constraints -- sharing by position -- leads to the exponential explosion of type parameters, as was shown by Harper and Pierce in 2003. One often hears suggestions of type-level records, to fix the problem.

In the joint article with Chung-chieh Shan, we translate Harper and Pierce's example into Haskell, using only the most common Haskell extensions to give type-equality constraints by name and avoid the exponential blowup. We can indeed refer to type parameters `by name' without any type-level records, taking advantage of the ability of a Haskell compiler to unify type expressions and bind type variables. We hope this message helps clarify the difference between the two sharing styles, and relate the ML and Haskell orthodoxies.

References
Fibration.lhs [16K]
The article with the juxtaposed literate Haskell and OCaml code
It was posted by Chung-chieh Shan on the discussion thread Applicative translucent functors in Haskell on the Haskell mailing list on Mon Sep 13 15:20:33 EDT 2004.
 

Typeable makes Haskell98 unsound

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
Version
The current version is 1.1, Jul 31, 2007.
 

State Monad as a term algebra

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.

Version
The current version is 1.1, Jan 4, 2005.
References
StateAlgebra.hs [4K]
The commented Haskell source code and a few tests
The code was originally posted as Initial (term) algebra for a state monad on the Haskell-Cafe mailing list on Tue, 4 Jan 2005 00:08:04 -0800 (PST)


Last updated May 1, 2014

This site's top page is http://okmij.org/ftp/

oleg-at-okmij.org
Your comments, problem reports, questions are very welcome!

Converted from SXML by SXML->HTML