Both Standard ML and Haskell (as well as many other languages) allow

the definition of type synonyms. Type synonyms seem pretty easy to

deal with, but there is one tricky case which has caused bugs (now

fixed) in at least two major implementations of these languages,

The tricky case is parameterized type synonyms which ignore some

of their arguments. Consider the following definition (I'll use SML

for examples but same issues arise in Haskell):

type 'a Bogus = int

When unifying two Bogus types (during type inference), one must be careful

not to unify their arguments. For instance, the unification of

bool Bogus and string Bogus should not cause the (attempted) unification of

bool and string.

I've long wondered whether real programmers actually write such

seemingly-silly types. However, I recently encountered a situation

where they turned out to be useful.

Consider writing a signature for functional parsers (as discussed frequently

in this newsgroup and mentioned in just about every book on functional

programming). It might look something like this:

signature PARSER =

sig

type ('a,'t) Parser

(* 'a is the type of object being parsed *)

(* 't is the type of tokens *)

...

val succeed : 'a -> ('a,'t) Parser

val fail : ('a,'t) Parser

val literal : ''t -> (''t,''t) Parser

val && : ('a,'t) Parser * ('b,'t) Parser -> ('a * 'b,'t) Parser

val || : ('a,'t) Parser * ('a,'t) Parser -> ('a,'t) Parser

...

val parse : ('a,'t) Parser -> 't list -> 'a option

end

This works well for many implementations. For instance, a simple

non-backtracking parser might have the type

type ('a,'t) Parser = 't list -> 'a * 't list

while a simple backtracking parser using lazy lists might have the type

type ('a,'t) Parser = 't list -> ('a * 't list) lazy_list

But now consider an implementation of backtracking parsers that passes

around explicit success and failure continuations (regular functions --

not continuations obtained from callcc). Its type might look

something like this

type FCont = unit -> Answer

type ('a,'t) SCont = 'a -> FCont -> 't list -> Answer

type ('a,'t) Parser = ('a,'t) SCont -> FCont -> 't list -> Answer

But what is Answer? Well, the initial success and failure continuations are

set up by the function parse. Looking at its result type, we see that

Answer should be something like 'a option, but this doesn't work. We

quickly come to the conclusion that each of these types should take an

extra parameter 'r for the type of Answer, e.g. ('a,'t,'r) Parser.

Then the types of some of the parsing functions would be

val && : ('a,'t,'r) Parser * ('b,'t,'r) Parser -> ('a * 'b,'t,'r) Parser

val parse : ('a,'t,'a option) Parser -> 't list -> 'a option

To do this of course requires adding this extra parameter everywhere in

the signature. But now there are many other implementations of parsers

which do not use this parameter! For instance, the simple non-backtracking

parser from earlier would now be

type ('a,'t,'r) Parser = 't list -> 'a * 't list

^

^ unused!

This same situation applies whereever you might naturally consider a

continuation-passing style implementation since such continuations always

seem to have this Answer type floating around. Either you include something

like 'r in the signature, or you disallow such implementations. (Note

that continuations obtained from callcc do not have this problem since

the type 'a cont does not mention the type of answers. However,

such continuations have other problems, such as weak polymorphism.)

Does anyone else know of other examples (not involving continuations)

which naturally lead to type synonyms with unused parameters?

Chris Okasaki

--

-------------------------------------------------------------------------------

| Chris Okasaki | Life is NOT a zero-sum game! |

-------------------------------------------------------------------------------