undefined
to definedOverlappingInstances
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.
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.
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.
Fix.hs [3K]
The complete Haskell code and the tests
All the ways to express the polymorphic fixpoint operator in OCaml
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 bwhich 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.
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>
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
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)
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 mThis 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]) fthen 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>
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.
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>
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:
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>
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 endThe 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) endThe 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.
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 vFor 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 site's top page is http://okmij.org/ftp/
Converted from SXML by SXML->HTML