type synonyms 
Author Message
 type synonyms

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! |

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



Wed, 15 Nov 1995 03:40:19 GMT  
 type synonyms
|> [...] type 'a Bogus = int [...]
|> 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.
|>
|> Does anyone else know of other examples (not involving continuations)
|> which naturally lead to type synonyms with unused parameters?

For some collection types, you can view the key type and the value type
as identical (e.g., 'a list), and hence only need one type variable for
a polymorphic type, while for others, keys and values can have
different types, and you need two type variables (e.g., ('a,'b)
hash_table).

If you want to write functors that generate polymorphic functions for
either kind of collection class, you must come up with a signature that
is compatible with both of them.  To do this, even the collection types
that only need one polymorphic type variable need to include another
dummy type variable (e.g., ('a,'b) list).

I view this mainly as a "problem" with the SML module system.  It seems
fixable, but, then, it's not clear that it's worth the effort: the
module system is geared more towards explicit parameterization via
functors than towards generating polymorphic functions.

                                        Thomas.



Wed, 15 Nov 1995 09:07:05 GMT  
 
 [ 2 post ] 

 Relevant Pages 

1. common type synonyms (haskell)

2. Looking for a short SYNONYM

3. X86 opcode synonyms

4. english synonyms

5. Synonyms

6. Suggestion: = as synonym for == in expr

7. Hi all - new to smalltalk [type services and type-safety]

8. statically Typed vs dinamically typed

9. Strongly Typed and Weakly Typed Languages

10. Difference between a type system and a type constraint system

11. The notions of type and of type constraint

12. Types, types: static vs. dynamic -- classification

 

 
Powered by phpBB® Forum Software