
      A technical summary of the new features in Hugs 1.3c

                      Mark P. Jones
                  University of Nottingham
                        March 1998

There have been many changes between Hugs 1.3b and Hugs 1.3c.
This technical note summarizes the most significant of these
new features.


MULTIPLE PARAMETER CLASSES:  Hugs 1.3c now allows the definition and
use of multiple parameter constructor classes.  Early experience with
this kind of facility in Gofer suggested that it would often result
in ambiguity.  However, users of Gofer have subsequently discovered
a number of important applications for multiple parameter type classes
that do not cause ambiguities or other problems with overloading.

The following example shows one possible application for a two parameter
class:

   class Collection c a where
       empty  :: c a
       insert :: a -> c a -> c a
       enum   :: c a -> [a]


RESTRICTIONS ON INSTANCES HAVE BEEN RELAXED: Unlike previous versions
of Hugs, there are no syntactic restrictions on the forms of type
expressions or class constraints that can be used in an instance
declaration.  For example, the following definitions are all
acceptable:

    instance (Eq [Tree a], Eq a) => Eq (Tree a) where ...
    instance Eq a => Eq (Bool -> a) where ...
    instance Num a => Num (String,[a]) where ...

Because there are restrictions, it is possible to code up arbitrarily
complex instance entailments, and in fact, this means that checking
entailments, and hence calculating principal types, is, in the general
case, undecidable.  We do not expect this to cause problems in practice,
but if it does, then we can introduce restrictions later once we have
had a chance to see how the extra flexibility is used in practice.


OVERLAPPING INSTANCES ARE SUPPORTED:  If the command line argument +o
is given, then Hugs 1.3c will accept overlapping instances, provided
that one of each overlapping pair of instances is strictly more
specific than the other.  This facility has been introduced in a way
that does not compromise the coherence of the type system.  However,
its semantics differs slightly from the semantics of overlapping
instances in Gofer, so users may sometimes be surprised with the
results.  This is why we have decided to allow this feature to be
turned on or off by a command line option (the default is off).
If practical experience with overlapping instances is positive then
we may change the current default, or even remove the option.


RESTRICTIONS ON CONTEXTS HAVE BEEN RELAXED: There are no longer any
restrictions on the form of types that can appear in a context.
For example, the principal type of an expression (\x -> x==[])
is  Eq [a] => [a] -> Bool, reflecting the fact that the equality
function is used to compare lists of type [a].  In previous versions
of Hugs, an inferred type of  Eq a => [a] -> Bool  would have been
produced for this term.  The latter type can still be used if an
explicit type signature is provided for the term, assuming that
an instance declaration of the form: 

    instance Eq a => Eq [a] where ...

is in scope.  For example, the following program is valid:

    f  :: Eq a => [a] -> Bool
    f x = x==[]

Indeed, a program that was accepted by the previous version of
the Hugs type checker should still be accepted in the new version.
However, contexts are not reduced by default because this gives
more general types (and potentially more efficient handling of
overloading).  For example, the term (\xs ys -> map id xs == ys)
has no principal type in Haskell 1.3, but will be assigned a type
(Eq (f a), Functor f) -> f a -> f a -> Bool  in Hugs 1.3c.


POLYMORPHIC RECURSION:  Hugs 1.3c now supports full polymorphic
recursion, even for functions with overloaded types.  This means
that Hugs will accept definitions like the following:

   p  :: Eq a => a -> Bool
   p x = x==x && p [x]

(Note that the type signature here is *not* optional.)  In fact,
Hugs 1.3c goes beyond the treatment of polymorphic recursion in
Haskell 1.3 and Haskell 1.4 by looking at dependencies within
individual binding groups.  For example, the following definitions
are acceptable, even though there is no explicit type signature
for the function q:

   p  :: Eq a => a -> Bool
   p x = x==x && q [x]

   q x = x==x && p [x]

This is made possible by the observation that we can calculate a
type for q, without needing to calculate the type of p at the same
time because the type of p is already specified.


RANK 2 POLYMORPHISM:  Hugs now allows the definition of functions
that take polymorphic arguments.  This includes functions defined
at the top-level, in local definitions, in class members, and in
primitive declarations.  In addition, Hugs allows the definition of
datatypes with polymorphic and qualified types.  The following examples
illustrate the syntax that is used:

   amazed :: (forall a. a -> a) -> (Bool,Char)
   amazed i = (i True, i 'a')

   twice    :: (forall b. b -> f b) -> a -> f (f a)
   twice f   = f . f

Note that:

  - forall is now a reserved word.

  - quantified variables may be of any kind, including * (types) or
    * -> * (unary type constructors) as in the examples above.

  - variables quantified in a forall type must appear in the scope of
    the quantifier.

  - quantified variables are not allowed to have the same name as a
    variable that is used in the enclosing scope.

  - nested quantifiers are not allowed, and quantifiers can only appear
    in the types of function arguments, not in the results.

  - functions can only take polymorphic arguments if an explicit type
    signature is provided for that function.  Any call to such a function
    must have at least as many arguments as are needed to include the
    rightmost argument with a quantified type.

  - It is not necessary for all polymorphic arguments to appear at the
    beginning of a type signature.  For example, the following type
    signature is perfectly valid:

      eg :: Int -> (forall a. [a] -> [a]) -> Int -> [Int]

    However, as a consequence of the rules given above, the eg function
    defined here must always be applied to at least two arguments, even
    though the first of these does not have a polymorphic type.

  - In the definition of a function, there must be at least as many
    arguments on the left hand side of the definition as are needed to
    included the rightmost argument with a quantified type.  Only
    variables (or the wildcard character, _) can be used as arguments
    on the left hand side of a function definition where a value of
    polymorphic type is expected.

  - Arbitrary expressions can be used for polymorphic arguments in a
    function call, provided that they can be assigned the necessary
    polymorphic type.  For example, all of the following expressions
    are valid calls to the amazed function defined above:

         amazed (let i x = x in i)
         amazed (\x -> x)
         amazed (id . id . id . id)
         amazed (id id id id id)

A similar syntax can be used to include polymorphic components in
datatypes, as illustrated by the following examples:

   data Monad1 m = MkMonad1 {
                    unit1 :: (forall a. a -> m a),
                    bind1 :: (forall a, b. m a -> (a -> m b) -> m b)
                   }

   data Monad2 m = MkMonad2 (forall a. a -> m a)
                            (forall a, b. m a -> (a -> m b) -> m b)

   listMonad1 = MkMonad1 {unit1 = \x->[x],
                          bind1 = \x f -> concat (map f x)}

   listMonad2 = MkMonad1 (\x->[x]) (\x f -> concat (map f x))

In this case, MkMonad1 and MkMonad2 have types:

   (forall b. b -> m b) -> (forall b,c. m b -> (b->m c) -> m c) -> Monad1 m
   (forall b. b -> m b) -> (forall b,c. m b -> (b->m c) -> m c) -> Monad2 m

respectively, while listMonad1 and listMonad2 have types:

   Monad1 []
   Monad2 []

Note that an expression like (MkMonad2 (\x->[x])) will not be allowed
because, by the rules above, the constructor MkMonad2 can only be used
when both arguments are provided.  An attempt to correct this problem
by eta-expansion, such as (\b -> MkMonad2 (\x->[x]) b), will fail because
the new variable, b, that this introduces is now lambda-bound and hence
the type that we obtain for it will not be as general as the MkMonad2
constructor requires.  We can, however, use an auxiliary function with
an explicit type signature to achieve the desired effect:

   halfListMonad  :: (forall a,b. [a] -> (a -> [b]) -> [b]) -> Monad2 []
   halfListMonad b = MkMonad2 (\x -> [x]) b

In the current implementation of Hugs, the named update syntax for Haskell
datatypes (in expressions like exp{field=newValue}) cannot be used with
datatypes that include polymorphic components.

The runST primitive that is used in work with lazy state threads is
now handled using the facilities described here.  As a result, it is
no longer necessary to build the ST type into the interpreter; to make
use of these facilities, a program should instead import the ST library
from the libhugs directory.


EXPLICITLY SCOPED TYPE VARIABLES:  Hugs 1.3c allows patterns of the
form (pat :: type) to be used as type annotations (in the style of
Standard ML).  The type specified here must be a monotype (no forall
part or class constraints are allowed), but may include variables,
which have the same scope as the pattern in which they appear.  For
example, the term  \(x::Int) -> x  has type Int -> Int, while the
expression  \(x::a) (xs::[a]) -> xs ++ [x]  has type a -> [a] -> [a].

  - It is an error for a variable to be used in a type where a more
    specific type is inferred.  For example, (\(x::a) -> not x) is
    not a valid expression.

  - It is an error for two distinct variables to be used where the
    two types concerned are the same.  For example, the expression
    (\(x::a) (y::b) -> [x,y]) is not valid.

  - Type variables bound in a pattern may be used in type signatures
    or further pattern type annotations within the scope of the
    binding.  For example:

       f (x::a) = let g   :: a -> [a]
                      g y  = [x,y]
                  in  g x

    In current versions of Haskell, there is no way to write a type
    for the local function g in this example because of the convention
    that free type variables are implicitly bound by a universal
    quantifier.  In this example, the variable is instead bound in
    the pattern (x::a) and so the type assigned to g is actually
    monomorphic.

  - Type signatures do not introduce bindings for type variables,
    but may involve type variables bound in an enclosing scope.
    For example, there is no direct relation between the variable t
    appearing in the type signature and the variable t appearing in
    the pattern annotation in the following code:

       pair         :: t -> s -> (t,s)
       pair x (y::t) = (x,y::t)

    The explanation for this is that the type signature for pair
    (which might, in practice, be separated from the definition)
    is not in the scope of the binding of the variables x and y.

  - In the current implementation, pattern type annotations that
    include variables are not allowed on the left hand side of a
    pattern binding.   For example, ((x::a):xs) = [1..]  will not
    be accepted.


EXISTENTIAL TYPES:  Hugs 1.3c supports a form of existential types in
datatype definition in the style originally suggested by Perry and by
Laufer.  Type variables appearing free on the right hand side of a
datatype definition are treated as being bound by an implicit existential
quantifier.  For example, the definition:

   data Appl = MkAppl (a -> Int) a (a -> a)

introduces a fully a polymorphic constructor function:

   MkAppl :: (a -> Int) -> a -> (a -> a) -> Appl.

Because the variable a does not appear in the result type, the choice
of a in any particular use of MkAppl will be hidden.  As a result,
when a MkAppl constructor is used in a pattern match, we must be
careful that the hidden type does not `escape' into the result type
or into the enclosing assumptions.  For example, the following
definitions are acceptable:

   good1 (MkAppl f x i) = f x
   good2 (MkAppl f x i) = map f (iterate i x)

but the next two definitions are not:

   bad1 (MkAppl f x i) = x
   bad3 y              = let g (MkAppl f x i) = length [x,y] + 1
                         in  True

The facilities for explicitly scoped type variables described above
can be used in conjunction with existentials, as in the example:

   good (MkAppl f (x::a) i) = map f (iterate i x :: [a])

In this case, the typing annotations are redundant, although they do
still provide potentially useful information for the programmer.


EXTENSIBLE RECORDS:  Trex is a flexible system of extensible records,
documented in docs/Trex.  The implementation of Trex in Hugs 1.3c is
an extension of the facilities in previous releases, and now supports
both derived "show" and equality over record values (in programs that
import the Trex module from the libhugs directory).



