Aaron Denney | 1 Feb 01:13 2006

Re: Everything Your Professor Failed to Tell You About Functional Programming

On 2006-01-31, Cale Gibbard <cgibbard <at> gmail.com> wrote:
> The point about monads being a design pattern I actually wouldn't take
> too much exception to, except for the fact that I don't really like
> the term "design pattern" in the first place. :) Too often, the things
> people call design patterns are just ordinary functions or general
> interfaces in a more expressive programming language.

Right.  I'd call haskell's typeclasses excellent language support for
formalizing and truly taking advantage of design patterns where


Aaron Denney
peter morris | 1 Feb 12:34 2006

TYPES 2006 Workshop

Registration for TYPES 2006 is now open.
Early registration until 15/3/2006.

The TYPES06 Team


                  TYPES 2006

        Main Conference of the Types Project
           Nottingham, UK, 18-21 April 2006


This is the latest meeting in a series that started 1992, the last
conference was in December 2004 in Paris.

The topic of the meeting is formal reasoning and computer programming
based on Type Theory : languages and computerised tools for reasoning,
and applications in several domains such as analysis of programming
languages, certified software, formalisation of mathematics and
mathematics education.

TYPES 2006 is colocated with TFP 2006 (Trends in Functional
Programming) and we plan to hold a joint session on Dependently Typed

The conference takes place at Jubilee campus of the University of
Nottingham, on-site accomodation will be available together with the

For more information see:  http://www.cs.nott.ac.uk/types06/

Registration is open now. You will be able to submit
your talk and abstract together with your registration. We will try to
accomodate all talks which fit into the scope of the TYPES
project. There will also be invited lectures from Bart Jacobs,
Simon Peyton Jones (joint with TFP) and Hongwei Xi.

Please direct all emails related to TYPES 2006 to
types06 <at> cs.nott.ac.uk


The Organisation Comittee

Thorsten Altenkirch, James Chapman, Conor McBride, Peter Morris and
Wouter Swierstra .

Haskell mailing list
Haskell <at> haskell.org
Simon Peyton-Jones | 1 Feb 17:49 2006

Internships at Microsoft Research, Cambridge

Internships are available at Microsoft Research, Cambridge, for this
summer.  More information is available here:


Internships are usually for graduate students (PhD or Masters) and last
12 weeks (although longer projects are also possible).  Furthermore,
although there is a deadline of *28 Feb* for the main batch of summer
internships, MSR is now taking interns year-round, a non-summer
internship may even be easier to arrange (because it misses the Big

The reason for this mail is to highlight the fact that Simon & I would
particularly like to encourage applicants interested in working on
Haskell-related projects.  We have a number of projects in mind, but
feel free to suggest your own:

  - Parallel garbage collection: to complement GHC's new support
    for SMP parallelism, replacing single-threaded garbage
    collection with parallel GC is a high priority goal, with
    plenty of interesting research too.

  - Parallel Haskell applications: investigate using SMP/multicore
    parallelism for real, either implicit parallelism or using
    concurrency & STM, by tackling some applications.

  - Haskell debugging in GHCi: we have some ideas for building a
    debugger into GHCi, there are some research angles here too.

  - GHC as a library: we have made a start on providing a library
    interface to GHC, but there is much left to do.  Re-targetting
    Haddock on top of GHC would make a good project, for example.

  - C-- code generation: we have a project student working on 
    C-- code gen, but there's a lot to do here.  The ultimate goal
    is to divide the code generator into two: first generate C--
    and then CPS-convert it into C-- with only tail calls, suitable
    for generating code using the existing paths (native code and
    via-C) too.

Let us know by email if you apply.  Good luck!

Simon Peyton Jones and Simon Marlow
Ashley Yakeley | 1 Feb 22:02 2006

Idioms and Proposals

I've added a few Haskell idioms and proposals (well, ideas for changes) 
to the wiki:


I particularly wanted to include "perennial" ideas that often seem to 
get discovered independently (for instance, type arithmetic). Of the 
proposals, I think only MonadPlus reform might be worth moving to the 
Haskell Prime process.

Please add, improve, etc.
Thom Fruehwirth | 2 Feb 12:38 2006

Research position in constraints and CHR

Please pass this message on to whoever you think may be interested.


                    University of Ulm, Germany

A research position is available for Ph.D. students or postdocs at the Faculty
of Computer Science, University of Ulm, Department of Software Engineering and
Compiler Construction in the area of Constraint Handling Rules (CHR).

The successful applicant will be responsible for a research project funded by
the German Research Foundation DFG. Its topic is the specification, generation,
implementation and analysis of rule-based algorithms for solving of global
constraints in CHR. The position thus requires knowledge and interest in one or
more of the aforementioned areas.

At least a master or equivalent in computer science or strongly related area is
required. The initial appointment will be for two years, beginning as soon as
possible, with a possible renewal for another two years depending on the
evaluation of the research foundation.

Gross salary is 56.400 Euro a year according to assistant position BAT IIa. It
includes health and social insurance. Additional money for conference travel and
visit of the advanced summer school on global constraints will be provided.

Ulm is a pleasant city of 150.000 on the Danube, with nearby rocks for free-
climbing, close to Stuttgart, Munich, the Alps, and Lake Konstanz. Every day
life requires a basic command of German.

Prospective applicants should email their resume with three references, and link
to homepage and publications if available, to our secretary Claudia Hammer at

hammer <at> informatik.uni-ulm.de
by February 28th, 2006,
or until the position is filled.

Prof. Thom Fruehwirth
c/o Claudia Hammer
University of Ulm
Faculty of Computer Science
Department PM
D-89069 Ulm, Germany

Email: hammer <at> informatik.uni-ulm.de
WWW:   http://www.informatik.uni-ulm.de/pm/mitarbeiter/fruehwirth/
CHR:   http://www.cs.kuleuven.be/~dtai/projects/CHR/

The University of Ulm aims to increase the representation of women in research
and teaching and therefore expressly encourages female scientists to apply.
Disabled applicants with relevant qualifications will be given priority.
Mads Lindstrøm | 2 Feb 21:48 2006

Type synonyms in the instance head

Hi all

In this url
one can read about "Type synonyms in the instance head". A quote:

"You cannot, for example, write:

  type P a = [[a]]
  instance Monad P where ...

This design decision is independent of all the others, and easily
reversed, but it makes sense to me."

It does not make sense to me! Could anybody explain why this makes

Below, I will try to explain why it does not make sense to me.

If I have:

data LongAndUglyName a = ...
type ShortAndTellingName a = LongAndUglyName a

It seems to make sensible to:

instance Foo ShortAndTellingName

Also it is called a type _synonym_ and the type synonym and what it is
synonym for, should therefore be interchangeable.

This restriction do not only apply to instance heads, but also to
contexts, as in:

instance (Foo LongAndUgleName) => class something ...

Here again LongAndUglyName cannot be replaced by ShortAndTellingName.
This can be annoying if you have a lot of these instance declarations.

Also what the type synonym is synonym for, may not have any name and
thus properly not be telling at all, as in:

type TellingName a = \a -> String

/Mads Lindstrøm
Ashley Yakeley | 2 Feb 21:53 2006

Re: Type synonyms in the instance head

Mads Lindstrøm wrote:
> "You cannot, for example, write:
>   type P a = [[a]]
>   instance Monad P where ...
> This design decision is independent of all the others, and easily
> reversed, but it makes sense to me."

It's not clear to me how this can be reversed. Wouldn't reversing this 
mean introducing "type lambda", and doesn't that raise all kinds of 
nasty issues (like having to type-annotate function applications)?

> If I have:
> data LongAndUglyName a = ...
> type ShortAndTellingName a = LongAndUglyName a
> It seems to make sensible to:
> instance Foo ShortAndTellingName

You can do this instead:

type ShortAndTellingName = LongAndUglyName


Ashley Yakeley
Ralf Lammel | 2 Feb 22:39 2006

RULE 2006 at FLoC --- paper deadline 14 May

                         Call for Papers

                           RULE 2006 
         7th International Workshop on Rule-Based Programming

                          Seattle, USA
                        11th August 2006

                 A satellite event of RTA 2006 at FLoC

The basic concepts of rule-based programming appear throughout Computer
Science, from theoretical foundations to practical implementations. Term
rewriting is used in semantics in order to describe the meaning of
programming languages, as well as in the implementation of program
transformation systems. Rules are used implicitly or explicitly to
perform computations, e.g., in Mathematica, OBJ, ELAN, Maude or to
perform deductions, e.g., by using inference rules to describe or
implement a logic, theorem prover or constraint solver. Mail clients and
mail servers use complex rules to help users organising their email and
sorting out spam. Language implementations use bottom-up rewrite systems
for code generation (as in the BURG family of tools.)
Constraint-handling rules (CHRs) are used to specify and implement
constraint-based algorithms and applications. Rule-based programming
idioms also give rise to multi-paradigm languages like Claire.

The purpose of this workshop is to bring together researchers from the
various communities working on rule-based programming to foster advances
in the theory of rule-based programming, cross-fertilization between
theory and practice, research on rule-based programming methods, and the
exploration of important application domains of rule-based programming.

RULE 2006 will be a one-day satellite event of RTA 2006 at FLoC.

Topics of interest

* Languages for rule-based programming
  - Expressive power, Idioms, Design patterns
  - Semantics, Type systems
  - Implementation techniques
  - System descriptions

* Other foundations
  - Complexity results
  - Advances on rewriting logic
  - Advances on rewriting calculus
  - Static analyses of rule-based programs
  - Transformation of rule-based programs

* Applications of rule-based programming, e.g.:
  - Program transformation
  - Software analysis and generation
  - System Control
  - Work-flow control
  - Knowledge engineering
  - System descriptions

* Combination with other paradigms
  - Functional programming
  - Logic programming
  - OO programming
  - Biocomputing
  - Language extensions
  - Language embeddings

Submissions and Publication:

Papers (of at most 15 pages) should be submitted electronically via the
submission page: http://www.easychair.org/RULE2006 Any problems with the
submission procedure should be reported to one of the PC chairs:
Maribel.Fernandez <at> kcl.ac.uk, Ralf.Lammel <at> microsoft.com 

Accepted papers will be published in the preliminary proceedings volume,
which will be available during the workshop. The final proceedings will
be published in Electronic Notes in Theoretical Computer Science
(ENTCS), Elsevier.

- 14th May 2006: Deadline for electronic submission of papers
- 15th June 2006: Notification of acceptance of papers
- 30th June 2006: Deadline for final versions of accepted papers
- 11th August 2006: Workshop

Programme Committee:

- Mark van den Brand (TU Eindhoven, Netherlands)
- Horatiu Cirstea (LORIA, France)
- Pierre Deransart (INRIA Rocquencourt, France)
- Michael L. Collard (Kent State University, USA)
- Martin Erwig (Oregon State University, USA)
- Francois Fages (INRIA Rocquencourt, France)
- Maribel Fernandez (Co-Chair, King's College London, UK)
- Jean-Pierre Jouannaud (LIX, Ecole Polytechnique, France)
- Oleg Kiselyov (FNMOC, USA)
- Ralf Laemmel (Co-Chair, Microsoft, USA )
- Ugo Montanari (Universita di Pisa, Italy)
- Pierre-Etienne Moreau (LORIA, France)
- Tobias Nipkow (Technical University Munich, Germany)
- Tom Schrijvers (K.U.Leuven, Belgium)
- Martin Sulzmann (National University of Singapore, Singapore) 
- Victor Winter (University of Nebraska at Omaha, USA)
Wolfgang Jeltsch | 2 Feb 23:11 2006

Re: Type synonyms in the instance head

Am Donnerstag, 2. Februar 2006 21:48 schrieb Mads Lindstrøm:
> [...]

> Also what the type synonym is synonym for, may not have any name and
> thus properly not be telling at all, as in:
> type TellingName a = \a -> String

What is \a -> String?

> /Mads Lindstrøm

Best wishes,
oleg | 3 Feb 07:42 2006

Class-parameterized classes, and the type-level logarithm

We show invertible, terminating, 3-place addition, multiplication, and
exponentiation relations on type-level 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 inverting method can work with any
representation of (type-level) numerals, binary or decimal.

Furthermore, the inverter itself is generic: it is a type-class
function, that is, a type-class parameterized by the type-class to
`invert'.  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
quite easily define (potentially, higher-order) type functions on type

Ashley Yakeley wrote:
] I know for the usual Peano representation of natural numbers, at least,
] it's possible to represent addition and subtraction with a single class
] with two fundeps (because classes represent relations between types
] rather than functions on them).

That can be done even for decimal type numerals,
cf. number-parameterized-types paper. But we can do better: we can
have _three_ functional dependencies, so that any two operands of the
type class determine the third. The key insight was the result of a
conversation with Chung-chieh Shan and Gregory Price in the evening of
Nov 10, 2003.

Despite what the extension says, the arithmetic relations in this file
are all decidable.

> {-# OPTIONS -fglasgow-exts #-}
> {-# OPTIONS -fallow-undecidable-instances #-}
> module PeanoArithm where
> data Z
> data S a
> __ = __

First we define a semi-sum relation, with only two functional

> class Sum2 a b c | a b -> c, a c -> b
> instance Sum2 Z a a
> instance Sum2 a b c => Sum2 (S a) b (S c)

Now we add the third dependency. It is that simple.

> class Sum a b c | a b -> c, a c -> b, b c -> a
> instance (Sum2 a b c, Sum2 b a c) => Sum a b c

After defining a few numbers,

> add:: Sum a b c => a -> b -> c
> add = __
> type One = S Z
> type Two = S (S Z)
> zero = __ :: Z
> one = __ :: One
> two = __ :: Two
> three = add one two
> n4    = add two two

we see that the typechecker can indeed add and subtract:

> ta1 = \x -> (add three x `asTypeOf` three)
> ta2 = \x -> (add x two `asTypeOf` three)
> -- ta3 = \x -> (add three x `asTypeOf` two)  -- fails

	*PeanoArithm> :t ta1
	ta1 :: Z -> S (S (S Z))
	*PeanoArithm> :t ta2
	ta2 :: S Z -> S (S (S Z))

Before we move to products, we introduce a few utilities

> class NLE x y
> instance Sum2 x a y => NLE x y
> class Mul a b c | a b -> c  -- a single-dependency multiplication
> instance Mul Z b Z
> instance (Mul a b c', Sum c' b c) => Mul (S a) b c  -- (a+1)*b = a*b + b

The relation |NLE x y| holds if |x| is less or equal to |y|, that is,
there exists a numeral |a| that in sum with |x| gives |y|.

We now introduce the generic inverter of an arithmetic function defined
on the whole set of natural numbers. The inverter is parameterized by
the numeric function (that is, a type class) to invert. We define
the type of these classes by the following class. It maps types to
classes (see also the HList paper):

> class Registry clas a b c | clas a b -> c

The inverter, the type-class function, is so trivial that I'm ashamed 
to discuss it. It is a simple for-loop.

> class Inv clas init limit a b c | clas init a b -> c
> instance (NLE x limit, Registry clas x b a', Sum2 a' r a,  
> 	    Inv' r clas x limit a b c)
>     => Inv clas x limit a b c
> class Inv' r clas x limit a b c | r clas x a b -> c
> instance Inv' Z clas x limit a b x		-- Found it
> instance Inv clas (S x) limit a b c           -- try next x
>     => Inv' (S r) clas x limit a b c

Division is defined as an inverse of multiplication:

> data RegMul
> instance Mul a b c => Registry RegMul a b c
> class Div m n q | m n -> q          -- m = n * q
> instance Inv RegMul Z m m n q => Div m n q

We partially apply Inv to the right operands, and get the Div relation
in return.

> pdiv :: Div a b c => a -> b -> c
> pdiv = __
> -- Only where all dependencies exist...
> class Product a b c | a b -> c, a c -> b, b c -> a
> instance (Mul a b c, Div c b a, Div c a b) => Product a b c
> prod:: Product a b c => a -> b -> c
> prod = __

Now the typechecker can multiply and divide

> n6 = prod two three
> tm1 = \x -> (prod three x `asTypeOf` n6)
> tm2 = \x -> (prod x two `asTypeOf` n6)
> -- tm3 = \x -> (prod x n4 `asTypeOf` n6)
> tm4 = \x -> (prod x n6 `asTypeOf` n6)
> -- tm5 = \x -> (prod x zero `asTypeOf` n6)
> tm6 = \x -> (prod x zero `asTypeOf` zero)

The inferred types are

	tm1 :: S (S Z) -> S (S (S (S (S (S Z)))))
	tm2 :: S (S (S Z)) -> S (S (S (S (S (S Z)))))
	tm4 :: S Z -> S (S (S (S (S (S Z)))))

The commented-out tests raise type errors.

The exponentiation is trivial:

> class Raise b e c | b e -> c  -- c = b ^ e
> instance Raise a Z (S Z)
> instance (Raise b e c', Mul b c' c) => Raise b (S e) c

The logarithm and the n-th root are two inverses of
(partially-applied) exponentiation. It takes a couple of lines to
define each

> data RegRaiseI
> instance Raise b a c => Registry RegRaiseI a b c
> class Log n b e | n b -> e  -- e = log_b n
> instance Inv RegRaiseI Z n n b e => Log n b e
> data RegRaise
> instance Raise a b c => Registry RegRaise a b c
> class Root a b c | a b -> c  -- c = b-th root of a
> instance Inv RegRaise Z a a b c => Root a b c

We introduce the full exponentiation relation

> class Exp b e c | b e -> c, b c -> e, e c -> b
> instance (Raise b e c, Log c b e, Root c e b) => Exp b e c
> pexp:: Exp a b c => a -> b -> c
> pexp = __

and test it

> n8 = add n4 n4
> n9 = prod three three
> te1 = pexp three two
> te2 = \x -> (pexp two x `asTypeOf` (add n8 n8))
> te3 = \x -> (pexp x three `asTypeOf` n8)
> -- te4 = \x -> (pexp x three `asTypeOf` n6)
> te5 = \x -> (pexp three x `asTypeOf` three)

*PeanoArithm> :t te2
te2 :: S (S (S (S Z)))
       -> S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))
*PeanoArithm> :t te3
te3 :: S (S Z) -> S (S (S (S (S (S (S (S Z)))))))

Indeed, 4 is the binary logarithm of 16, and two is the cubic root of 8.

Having gone that far, it is impossible to avoid factorial and its
inverse (as an evidence of further evolution of the Haskell programmer)

> class FactF a b | a -> b
> instance FactF Z (S Z)
> instance (FactF a b', Mul (S a) b' b) => FactF (S a) b
> data RegFact
> instance FactF a c => Registry RegFact a b c
> class FactR a c | a -> c    -- Inverse of Fact
> instance Inv RegFact (S Z) a a Z c => FactR a c
> class Fact a b | a -> b, b -> a
> instance (FactF a b, FactR b a) => Fact a b
> fact :: Fact a b => a -> b
> fact = __

-- :t fact n4

*PeanoArithm> :t \x -> (fact x  `asTypeOf` (prod n4 n6))
\x -> (fact x  `asTypeOf` (prod n4 n6)) :: S (S (S (S Z)))
	   -> S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))))))))))

Indeed, 4 is the inverse factorial of 24. It took only a split second.

The practical outcome of this exercise is the creation of a benchmark
suite for Haskell typecheckers, e.g., computing the inverse factorial
of 720. Perhaps there should be a shoot-out entry for the speed of

The implementation of RSA on type level is left for future work.