Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

typing of pattern bindings not general enough #3053

Closed
vicuna opened this issue Nov 23, 2001 · 5 comments
Closed

typing of pattern bindings not general enough #3053

vicuna opened this issue Nov 23, 2001 · 5 comments
Labels

Comments

@vicuna
Copy link

vicuna commented Nov 23, 2001

Original bug ID: 652
Reporter: administrator
Status: closed
Resolution: not a bug
Priority: normal
Severity: minor
Category: ~DO NOT USE (was: OCaml general)

Bug description

Hello,

the following program compiles fine:

let foo = function
| Some n -> Some (float n)
| None as none -> none

But the following:

let foo = function
| Some n -> Some (float n)
| none -> none

gives this type error:

File "foo.ml", line 3, characters 12-16:
This expression has type int option but is here used with type float option

This seems a bit inconsistent, though I understand the reason: in the
first case the compiler is explicitly told that this case (and therefore
the variable) matches "None" whereas in the second case we have a joker
variable.

However, the compiler has knowledge about the alternatives the joker
can take (otherwise it couldn't tell us about non-exhaustive matches)
and should therefore be capable of inferring that this is sound.

An example where this can be quite surprising to the unsuspecting user
is this:

let map_option f = function
| Some x -> Some (f x)
| none -> none

The compiler will infer this type, which is not the most general one:

val map_option : ('a -> 'a) -> 'a option -> 'a option

This may cause quite some confusion at the point of use...

Best regards,
Markus

--
Markus Mottl markus@oefai.at
Austrian Research Institute
for Artificial Intelligence http://www.oefai.at/~markus

@vicuna
Copy link
Author

vicuna commented Nov 26, 2001

Comment author: administrator

Hello,

the following program compiles fine:

let foo = function
| Some n -> Some (float n)
| None as none -> none

But the following:

let foo = function
| Some n -> Some (float n)
| none -> none

gives this type error:

File "foo.ml", line 3, characters 12-16:
This expression has type int option but is here used with type float option

This seems a bit inconsistent, though I understand the reason: in the
first case the compiler is explicitly told that this case (and therefore
the variable) matches "None" whereas in the second case we have a joker
variable.

I think I understand the problem (I have been bitten too). However I
also think this is a minor one. Unfortunatly, it is not easy to
correct in the compiler and easy to correct in users programs...

However, the compiler has knowledge about the alternatives the joker
can take (otherwise it couldn't tell us about non-exhaustive matches)
and should therefore be capable of inferring that this is sound.

Hahh, but the compiler is of schizoprenic nature. In some ideal world
the part that checks non-exhaustive matches does not give any
information to the part that types....
Altoutgh, this is not true anymore (typing of PM on polymorphic
variant), checking non-exhaustive matches takes place after typing
(because it needs types) and has no impact on it (because I saw no
reason why and rather keep away from the typer complexity).

Best regards,
Markus

--
Markus Mottl markus@oefai.at
Austrian Research Institute
for Artificial Intelligence http://www.oefai.at/~markus

--Luc

@vicuna vicuna closed this as completed Nov 26, 2001
@vicuna
Copy link
Author

vicuna commented Nov 26, 2001

Comment author: administrator

the following program compiles fine:

let foo = function
| Some n -> Some (float n)
| None as none -> none

But the following:

let foo = function
| Some n -> Some (float n)
| none -> none

gives this type error:

File "foo.ml", line 3, characters 12-16:
This expression has type int option but is here used with type float option

This seems a bit inconsistent

I agree with you that it is inconsistent, but would argue that both
examples should be rejected -- like they are in Caml Light.

The core ML typing discipline has a simple property: every variable
is monomorphic (has only one type throughout all its uses) except when
"let"-bound.

Now, we could argue whether variables bound by pattern-matching are
let-bound or not, e.g. if we think in terms of expanding
pattern-matching into elementary tests, the first example could be
viewed either as
let foo x = if x is a Some then ... else let none = None in none
or as
let foo x = if x is a Some then ... else let none = x in x
with the first translation giving "none" a polymorphic type, and the
second one giving it a monomorphic type.

Still, I'd argue that the natural typing rules for pattern-matching
are those that never generalize the type of the bound variables.

Now, OCaml doesn't follow this natural typing rule, and I believe this
has to do with polymorphic variants, where it was found useful to be
able to generalize the types of match-bound variables in some cases.
But this indeed leads to surprising behaviors like in your examples
above, and I miss the simplicity of the "classic" ML typing rules.

As to recognizing that your second example is indeed equivalent to
your first example, I'll go with Luc Maranget: yes, it can be done,
and this is more or less what the exhaustiveness checker does; no,
we'd rather not depend on the exhaustiveness checker during type
inference.

Cheers,

  • Xavier Leroy

@vicuna
Copy link
Author

vicuna commented Nov 26, 2001

Comment author: administrator

the following program compiles fine:

let foo = function
| Some n -> Some (float n)
| None as none -> none

But the following:

let foo = function
| Some n -> Some (float n)
| none -> none

gives this type error:

File "foo.ml", line 3, characters 12-16:
This expression has type int option but is here used with type float option

This seems a bit inconsistent

Now, OCaml doesn't follow this natural typing rule, and I believe this
has to do with polymorphic variants, where it was found useful to be
able to generalize the types of match-bound variables in some cases.
But this indeed leads to surprising behaviors like in your examples
above, and I miss the simplicity of the "classic" ML typing rules.

Well, I read the first example a bit quickly and I apologize.
Match bound whose type are generalized are the as bound'' variables. This is easy to do, since the typer locally knows that none'' is None.
(eg
The same applies to [] in
match l with
| x::xs -> f x :: map f xs
| [] as nil -> nil)
Already, one can argue against that, since it
complicates the typer.
I discovered it when I introducede variables in or-patterns
[consider (_::xs | [] as xs), should xs be generalized or not ???]

This extension was introduced for other reasons, related polymorphic
record types I guess.

--Luc

@vicuna
Copy link
Author

vicuna commented Nov 27, 2001

Comment author: administrator

On Mon, 26 Nov 2001, Luc Maranget wrote:

Hahh, but the compiler is of schizoprenic nature. In some ideal world
the part that checks non-exhaustive matches does not give any
information to the part that types....

I had feared that the OCaml-compiler might suffer from a split personality
here... ;)

On Mon, 26 Nov 2001, Xavier Leroy wrote:

I agree with you that it is inconsistent, but would argue that both
examples should be rejected -- like they are in Caml Light.

No problem for me! Reusing the matched value in a different typing context
immediately might also be somewhat interesting for efficiency purposes,
but the effect is probably too negligible to justify more complexity.

Still, I'd argue that the natural typing rules for pattern-matching
are those that never generalize the type of the bound variables.

I agree.

As to recognizing that your second example is indeed equivalent to
your first example, I'll go with Luc Maranget: yes, it can be done,
and this is more or less what the exhaustiveness checker does; no,
we'd rather not depend on the exhaustiveness checker during type
inference.

Understandable. I will just avoid this "feature" to be on the safe side
in case that you remove it again.

Regards,
Markus

--
Markus Mottl markus@oefai.at
Austrian Research Institute
for Artificial Intelligence http://www.oefai.at/~markus

@vicuna
Copy link
Author

vicuna commented Nov 27, 2001

Comment author: administrator

From: Luc Maranget luc.maranget@inria.fr

the following program compiles fine:

let foo = function
| Some n -> Some (float n)
| None as none -> none

But the following:

let foo = function
| Some n -> Some (float n)
| none -> none

gives this type error:

File "foo.ml", line 3, characters 12-16:
This expression has type int option but is here used with type float option

This seems a bit inconsistent

This is not. You were confused by the overloading on "as", which has
both the meaning of rebinding the value matched by a pattern and
(here) of specializing its type.

Note that the second meaning was introduced for polymorphic variants,
but in a way not directly relevant to this case: this was about
building a type containing only the constructors present in the
pattern, which has no meaning for classical variants. The typing rule
used in your example was introduced later, as the dual of introduction
of polymorphism for with-records, which was strongly requested by some
users. I'm not sure the dual for variants is that useful, but again it
was just an answer to a user request. (Give them something, ...)

As to whether the second example should be accepted as the first one,
I think this raises another question, namely whether typing can depend
on the order of rules in a pattern matching. Indeed, the first example
is still OK if you invert the rules, but the second one would fail
(both at typing and runtime).
Currently order is only relevant to unused case analysis, which is
only a warning, and has no impact on type inference.

Now, OCaml doesn't follow this natural typing rule, and I believe this
has to do with polymorphic variants, where it was found useful to be
able to generalize the types of match-bound variables in some cases.
But this indeed leads to surprising behaviors like in your examples
above, and I miss the simplicity of the "classic" ML typing rules.

The idea is indeed from polymorphic variants, but this specific case
is unrelated.

The same applies to [] in
match l with
| x::xs -> f x :: map f xs
| [] as nil -> nil)
Already, one can argue against that, since it
complicates the typer.
I discovered it when I introducede variables in or-patterns
[consider (_::xs | [] as xs), should xs be generalized or not ???]

I suppose you mean (_::xs | ([] as xs)).
This is a problem I did not consider, for evident chronological
reasons, but I would say that you can only generalize when all
occurences of xs are generalizable. This is what you would obtain if
you unify all types afterwards, but I should check the current
implementation.

Jacques Garrigue

@vicuna vicuna added the bug label Mar 19, 2019
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

No branches or pull requests

1 participant