Re: Typing of patterns

[Markus Mottl <mottl@miss.wu-wien.ac.at>]

On Mon, 05 Jun 2000, Pierre Weis wrote:
> > But isn't this a bit strange that an identifier cannot be used in a context
> > where replacing it syntactically with its bound value would be perfectly
> > ok?
> 
> Yes it is strange, but this is exactly what ML polymorphism specifies:
> polymorphism is introduced by the let-binding construct, and only
> occurrences of let-bound identifiers can be used with different
> types. Since your ``num'' above is not let-bound it is monomorphic and
> constraints are accumulating.

Ah - I think I see now: I was fooled by the syntactic "disguise" of the
problem! So this is similar to:

This does not work:

  fun id -> id 42, id "foo"

This works:

  let id x = x in id 42, id "foo"

> For instance, in fun [] as l -> e, the type of l is 'a list, and it
> can be generalized to all 'a. 'a list during the type-checking of e.
> In contrast, in fun x :: l as mylist -> e,
> the type 'a list of identifier mylist cannot be generalized, since 'a
> is the type of x and also occurs in the type of l. 

So the restriction is required to prevent problems with references, I
think, but those cannot occur if the type parameter is not used by any of
the parameters of the constructor, i.e. they are monomorphic (or there are
no parameters as in our case).

> Jacques may explain us if the above suggested generalization scheme is
> used for identifiers bound in as clauses of patterns (and if not,
> which scheme is used ?)...

I first thought it was some strange "special feature" of polymorphic
variants, but as it seems then, it is just that the corresponding typing
rule is obviously implemented differently...

> Conclusion: this strongly suggests to generalize the typing of
> synonymous identifiers in patterns, in order to obtain the same typing
> assignments for pattern matching on ``closed'' polymorphic variants
> and pattern matching on their (semantically equivalent) sum data types
> counterparts.
>
> Thank you for your interesting remark and question.

Thanks for your interesting explanations!

Since we are at it, there is another sometimes annoying type restriction,
this time with record updates, that comes to my mind, e.g.:

  type 'a t = { foo : 'a; bar : int };;

  let x = { foo = "foo"; bar = 3 };;

  let ok = { x with foo = "bla" };;
  let not_ok = { x with foo = 7 };;

Here the updated record "x" could have a less rigidly typed "foo"-field -
or should we rather say it has a "default" type if the field is not
updated? It can be a bit painful to do updates without such a
generalisation if there are many record names that one would have to
mention explicitely to create the wanted value as in:

  let now_ok = { foo = 7; bar = x.bar }

Best regards,
Markus Mottl

-- 
Markus Mottl, mottl@miss.wu-wien.ac.at, http://miss.wu-wien.ac.at/~mottl