[Haskell-cafe] Re: [Haskell] MR details (was: Implicit type of numeric constants)

[Bernie Pope]

My understanding of the MR is heavily influenced by the work I did on  
Hatchet, which is based
directly on Mark Jones' paper (and code) "Typing Haskell in Haskell".

I thought I would go back to that paper and see how he defines  
"simple" pattern bindings
and the MR.

I now quote directly from the relevent sections of the paper:

He represents function bindings with the Alt type, which is defined  
on page 9:

> "The representation of function bindings in following sections
> uses alternatives, represented by values of type Alt :
>
>    type Alt = ([Pat], Expr)
>
> An Alt specifies the left and right hand sides of a function
> definition."

On page 12 he defines what simple means with repsect to the Alt type  
and the MR:

> "A single implicitly typed binding is described by a pair con-
> taining the name of the variable and a list of alternatives:
>
>    type Impl = (Id , [Alt])
>
> The monomorphism restriction is invoked when one or more
> of the entries in a list of implicitly typed bindings is simple,
> meaning that it has an alternative with no left-hand side
> patterns.
>
> restricted :: [Impl] -> Bool
> retricted bs
>    = any simple bs
>    where
>    simple (i, alts) = any (null . fst) alts
> "

Curiously, his Alt type does not offer any way to represent pattern  
bindings where
the lhs is a non-variable pattern. But he addresses this point later  
on page 13:

> "In addition to the function bindings that we have seen al-
> ready, Haskell allows variables to be defined using pattern
> bindings of the form pat = expr . We do not need to deal di-
> rectly with such bindings because they are easily translated
> into the simpler framework used in this paper. For example,
> a binding:
>    (x,y) = expr
> can be rewritten as:
>    nv = expr
>    x = fst nv
>    y = snd nv
> where nv is a new variable. The precise definition of the
> monomorphism restriction in Haskell makes specific refer-
> ence to pattern bindings, treating any binding group that
> includes one as restricted. So, at first glance, it may seem
> that the definition of restricted binding groups in this pa-
> per is not quite accurate. However, if we use translations as
> suggested here, then it turns out to be equivalent: even if
> the programmer supplies explicit type signatures for x and
> y in the original program, the translation will still contain
> an implicitly typed binding for the new variable nv."

It is not obvious that this is consistent with the Report; I'll have to
think about it more.

Cheers,
Bernie.