Re: Typing of patterns

[Pierre Weis <Pierre.Weis@inria.fr>]

[...]
> 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"

Exactly.

[...]
> 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).

There is nothing special with references here: restriction for
references is just for generalization of types in let binding (roughly
speaking, when typing let x = e, x is monomorphic if e is an
application of the form f y). Here the restriction is just to be
correct: fun x -> x should have type 'a -> 'a, not 'a -> 'b; however
in case of complex pattern matching the rule is a bit too restrictive,
and can be relaxed in some cases as we saw.

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

I don't know if it is an implementation of the relaxed type-checking of
as identifiers or a special feature... Jacques will tell us...

[...]

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

In some sense the problem is similar, since it is a problem of type
sharing. However it is a bit simpler in this case:

{ x with foo = "bla" } should be simply treated as a macro and typechecked
exactly as its equivalent unsuggared expression :

{foo = "bla"; bar = x.bar}

This would be more general and regular.

Best regards,

Pierre Weis

INRIA, Projet Cristal, Pierre.Weis@inria.fr, http://cristal.inria.fr/~weis/