Re: Typing of patterns

From: Pierre Weis (Pierre.Weis@inria.fr)
Date: Tue Jun 06 2000 - 09:24:39 MET DST

  • Next message: Jacques Garrigue: "Re: Typing of patterns"

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



    This archive was generated by hypermail 2b29 : Tue Jun 06 2000 - 09:26:58 MET DST