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

Make assertions nonexpansive #1142

Merged
merged 2 commits into from Jun 4, 2017

Conversation

Projects
None yet
8 participants
@stedolan
Contributor

stedolan commented Apr 7, 2017

Currently, while assert false has polymorphic type, its type does not generalise:

let f  (type a) :  a -> a list = assert false
=>
val f : '_a -> '_a list
let f : type a . a -> a list = assert false
=>
Error: This definition has type 'a -> 'a list which is less general than
         'a0. 'a0 -> 'a0 list

I ran into this issue when I was prototyping some polymorphic code, and got errors when I wrote assert false as a placeholder for an implementation.

I think it's sound to mark assert e as a nonexpansive expression whenever e is. With this patch, both of the definitions above typecheck with type scheme 'a -> 'a list.

Make assertions nonexpansive.
This allows the type of 'assert false' to generalise.
@damiendoligez

This comment has been minimized.

Show comment
Hide comment
@damiendoligez

damiendoligez Apr 7, 2017

Member

Note that assert false is a special case for typechecking. All other uses of assert have type unit anyway, so it would probably be better to special-case assert false here too.

Member

damiendoligez commented Apr 7, 2017

Note that assert false is a special case for typechecking. All other uses of assert have type unit anyway, so it would probably be better to special-case assert false here too.

@gasche

This comment has been minimized.

Show comment
Hide comment
@gasche

gasche Apr 7, 2017

Member

I am a bit skeptical. assert false dynamically raises an exception, so I would expect the same argument to apply for raise e when e is pure, but then it might seem natural to extend it to perform e (the effect-handling variant), and while I couldn't convince myself that generalizing raise e is wrong, generalizing perform e definitely sounds wrong because of the ability to resume the exception.

Besides, I found it fairly difficult to experiment with your problem given that defining a function as assert false, rather than an eta-expansion of it, results in the program or toplevel crashing. If you write let f x = assert false, then it all works fine.

I am not sure what is the use-case for making it easier for users to write eagerly-evaluated assert false in their code.

Member

gasche commented Apr 7, 2017

I am a bit skeptical. assert false dynamically raises an exception, so I would expect the same argument to apply for raise e when e is pure, but then it might seem natural to extend it to perform e (the effect-handling variant), and while I couldn't convince myself that generalizing raise e is wrong, generalizing perform e definitely sounds wrong because of the ability to resume the exception.

Besides, I found it fairly difficult to experiment with your problem given that defining a function as assert false, rather than an eta-expansion of it, results in the program or toplevel crashing. If you write let f x = assert false, then it all works fine.

I am not sure what is the use-case for making it easier for users to write eagerly-evaluated assert false in their code.

@stedolan

This comment has been minimized.

Show comment
Hide comment
@stedolan

stedolan Apr 7, 2017

Contributor

Marking cases other than assert false as nonexpansive is much less useful, but does have a minor effect:

let foo = ((fun x -> x), assert true)
=>
trunk: val foo : ('_a -> '_a) * unit
patch: val foo : ('a -> 'a) * unit

I think this behaviour is better than if assert false were special-cased, although I can't imagine many programs will notice the difference.

Contributor

stedolan commented Apr 7, 2017

Marking cases other than assert false as nonexpansive is much less useful, but does have a minor effect:

let foo = ((fun x -> x), assert true)
=>
trunk: val foo : ('_a -> '_a) * unit
patch: val foo : ('a -> 'a) * unit

I think this behaviour is better than if assert false were special-cased, although I can't imagine many programs will notice the difference.

@stedolan

This comment has been minimized.

Show comment
Hide comment
@stedolan

stedolan Apr 7, 2017

Contributor

I am a bit skeptical. assert false dynamically raises an exception, so I would expect the same argument to apply for raise e when e is pure, but then it might seem natural to extend it to perform e (the effect-handling variant), and while I couldn't convince myself that generalizing raise e is wrong, generalizing perform e definitely sounds wrong because of the ability to resume the exception.

I also think that raise e could safely be marked nonexpansive (when e is). I'm not sure either way about perform e, it seems more subtle.

Besides, I found it fairly difficult to experiment with your problem given that defining a function as assert false, rather than an eta-expansion of it, results in the program or toplevel crashing. If you work let f x = assert false, then it all works fine.

I am not sure what is the use-case for making it easier for users to write eagerly-evaluated assert false in their code.

Unlike much of my use of OCaml, I ran into this issue when actually trying to write a program, rather than deliberately attempting to break the language!

I quite frequently write types for functions, stub out their implementations with assert false, then write some code that uses the function before later implementing it properly. While the stub is present, the program does indeed crash with an assertion failure. However, I can still use ocamlc -i (or, more often, look at whether merlin is complaining) to see if I've gotten the types right.

When developing in this style, it is surprising to see the compiler / merlin complain about a type error in assert false.

Contributor

stedolan commented Apr 7, 2017

I am a bit skeptical. assert false dynamically raises an exception, so I would expect the same argument to apply for raise e when e is pure, but then it might seem natural to extend it to perform e (the effect-handling variant), and while I couldn't convince myself that generalizing raise e is wrong, generalizing perform e definitely sounds wrong because of the ability to resume the exception.

I also think that raise e could safely be marked nonexpansive (when e is). I'm not sure either way about perform e, it seems more subtle.

Besides, I found it fairly difficult to experiment with your problem given that defining a function as assert false, rather than an eta-expansion of it, results in the program or toplevel crashing. If you work let f x = assert false, then it all works fine.

I am not sure what is the use-case for making it easier for users to write eagerly-evaluated assert false in their code.

Unlike much of my use of OCaml, I ran into this issue when actually trying to write a program, rather than deliberately attempting to break the language!

I quite frequently write types for functions, stub out their implementations with assert false, then write some code that uses the function before later implementing it properly. While the stub is present, the program does indeed crash with an assertion failure. However, I can still use ocamlc -i (or, more often, look at whether merlin is complaining) to see if I've gotten the types right.

When developing in this style, it is surprising to see the compiler / merlin complain about a type error in assert false.

@gasche

This comment has been minimized.

Show comment
Hide comment
@gasche

gasche Apr 7, 2017

Member

I would argue that asking you to write fun _ -> assert false instead is good because it makes sure that you will also be able to run your testsuite (or at least all parts that were not changed to use this new function).

Whether or not the type-checker should be the one telling you this, and whether the delivery could be different from a non-generalizable variable error, is another question where I would be tempted to agree with you. But the fact that the currently bad behavior is actually useful gives me pause in thinking harder about soundness of the proposal.

Member

gasche commented Apr 7, 2017

I would argue that asking you to write fun _ -> assert false instead is good because it makes sure that you will also be able to run your testsuite (or at least all parts that were not changed to use this new function).

Whether or not the type-checker should be the one telling you this, and whether the delivery could be different from a non-generalizable variable error, is another question where I would be tempted to agree with you. But the fact that the currently bad behavior is actually useful gives me pause in thinking harder about soundness of the proposal.

@stedolan

This comment has been minimized.

Show comment
Hide comment
@stedolan

stedolan Apr 7, 2017

Contributor

I would argue that asking you to write fun _ -> assert false instead is good because it makes sure that you will also be able to run your testsuite (or at least all parts that were not changed to use this new function).

This is an argument against accepting assert false at function types, or perhaps an argument in favour of being able to run OCaml programs containing type errors. It seems to have little to do with generalisation, and as you note "non-generalizable type variable" is a poor way of communicating that the error from an unimplemented function can be delayed with a lambda. Just because the current behaviour sometimes does something useful by coincidence, doesn't mean that it's right.

Besides, consider what happens if I'm replacing a function foo with an awkward interface, with bar which has a different type. I stub out bar as assert false, then change the uses of foo to use bar instead. The lack of type errors is a sanity check that my new interface is usable. I then implement bar, and run the tests. In this scenario, the tests can't run until I've implemented bar, so there's no value in writing fun _ -> assert false.

Contributor

stedolan commented Apr 7, 2017

I would argue that asking you to write fun _ -> assert false instead is good because it makes sure that you will also be able to run your testsuite (or at least all parts that were not changed to use this new function).

This is an argument against accepting assert false at function types, or perhaps an argument in favour of being able to run OCaml programs containing type errors. It seems to have little to do with generalisation, and as you note "non-generalizable type variable" is a poor way of communicating that the error from an unimplemented function can be delayed with a lambda. Just because the current behaviour sometimes does something useful by coincidence, doesn't mean that it's right.

Besides, consider what happens if I'm replacing a function foo with an awkward interface, with bar which has a different type. I stub out bar as assert false, then change the uses of foo to use bar instead. The lack of type errors is a sanity check that my new interface is usable. I then implement bar, and run the tests. In this scenario, the tests can't run until I've implemented bar, so there's no value in writing fun _ -> assert false.

@xavierleroy

This comment has been minimized.

Show comment
Hide comment
@xavierleroy

xavierleroy Apr 7, 2017

Contributor

Here is a sensible programming idiom to select implementations depending on OS at program start-up time:

  let my_os_function =
    match Sys.os_type with
    | "Unix" -> (fun x -> ...)
    | "Cygwin" -> (fun x -> ...)
    | "Win32" -> (fun x -> ...)
    | _ -> assert false

The final case should never occur according to the documentation of Sys.os_type, so it makes sense to fail immediately, at start-up time. Currently, my_os_function cannot be polymorphic even if the three fun x -> ... functions are, because assert false prevents generalization. @gasche: do you find this example more convincing?

At any rate, if we decide to make assert false nonexpansive, we must make raiseexp nonexpansive as well. I am too lazy to write a proof but I have a feeling that it's type-safe.

Contributor

xavierleroy commented Apr 7, 2017

Here is a sensible programming idiom to select implementations depending on OS at program start-up time:

  let my_os_function =
    match Sys.os_type with
    | "Unix" -> (fun x -> ...)
    | "Cygwin" -> (fun x -> ...)
    | "Win32" -> (fun x -> ...)
    | _ -> assert false

The final case should never occur according to the documentation of Sys.os_type, so it makes sense to fail immediately, at start-up time. Currently, my_os_function cannot be polymorphic even if the three fun x -> ... functions are, because assert false prevents generalization. @gasche: do you find this example more convincing?

At any rate, if we decide to make assert false nonexpansive, we must make raiseexp nonexpansive as well. I am too lazy to write a proof but I have a feeling that it's type-safe.

@gasche

This comment has been minimized.

Show comment
Hide comment
@gasche

gasche Apr 7, 2017

Member

Yes, I find this example more convincing. thanks! (I prefer it when assert false occurs in code that is dead in reasonable runs of the program, at least some of them.)

Member

gasche commented Apr 7, 2017

Yes, I find this example more convincing. thanks! (I prefer it when assert false occurs in code that is dead in reasonable runs of the program, at least some of them.)

@yallop

This comment has been minimized.

Show comment
Hide comment
@yallop

yallop Apr 7, 2017

Member

generalizing perform e definitely sounds wrong because of the ability to resume the exception.

perform e should indeed be treated as expansive. While algebraic effects don't require a value restriction when considered in isolation¹, when combined with other features of OCaml such as reference cells they can perform expansive effects. For example, it's straightforward to implement an interface equivalent to the ref interface, as follows:

effect Ref : 'a -> 'a ref            (* ref *)
effect Assign : 'a ref * 'a -> unit  (* := *)
effect Bang : 'a ref -> 'a            (* ! *)

then implement those effects in terms of ref and reconstruct the standard value restriction examples.

Regarding the proposal in this PR, I think it's worth noting a funny interaction with the relaxed value restriction. While @stedolan's example

let f  (type a) :  a -> a list = assert false
(* ↝ val f : '_a -> '_a list *)

is not generalized, a program that assigns f a more general scheme is generalized:

let f  (type a) :  a = assert false
(* ↝ val f : 'a *)

because the type variable only appears in a covariant position, and so the relaxed value restriction kicks in.

Since the accepted scheme is more general than the rejected scheme, OCaml will accept a variant of the original program that first generalizes, and then instantiates, like this:

let f  (type a) :  a = assert false
let g (type a) : a -> a list = f
(* ↝ val f : 'a
     val g : 'a -> 'a list *)

A similar arrangement works for raise: one can first generalize to the most-general scheme 'a.'a using the relaxed value restriction, and then instantiate to an arbitrary scheme:

let f  (type a) :  a = raise Not_found
let g (type a) (type b) : a -> b = f
(* ↝ val f : 'a
     val g : 'a -> 'b *)

¹No value restriction is needed for algebraic effects and handlers, O. Kammar and M. Pretnar, Journal of Functional Programming, January 2017

Member

yallop commented Apr 7, 2017

generalizing perform e definitely sounds wrong because of the ability to resume the exception.

perform e should indeed be treated as expansive. While algebraic effects don't require a value restriction when considered in isolation¹, when combined with other features of OCaml such as reference cells they can perform expansive effects. For example, it's straightforward to implement an interface equivalent to the ref interface, as follows:

effect Ref : 'a -> 'a ref            (* ref *)
effect Assign : 'a ref * 'a -> unit  (* := *)
effect Bang : 'a ref -> 'a            (* ! *)

then implement those effects in terms of ref and reconstruct the standard value restriction examples.

Regarding the proposal in this PR, I think it's worth noting a funny interaction with the relaxed value restriction. While @stedolan's example

let f  (type a) :  a -> a list = assert false
(* ↝ val f : '_a -> '_a list *)

is not generalized, a program that assigns f a more general scheme is generalized:

let f  (type a) :  a = assert false
(* ↝ val f : 'a *)

because the type variable only appears in a covariant position, and so the relaxed value restriction kicks in.

Since the accepted scheme is more general than the rejected scheme, OCaml will accept a variant of the original program that first generalizes, and then instantiates, like this:

let f  (type a) :  a = assert false
let g (type a) : a -> a list = f
(* ↝ val f : 'a
     val g : 'a -> 'a list *)

A similar arrangement works for raise: one can first generalize to the most-general scheme 'a.'a using the relaxed value restriction, and then instantiate to an arbitrary scheme:

let f  (type a) :  a = raise Not_found
let g (type a) (type b) : a -> b = f
(* ↝ val f : 'a
     val g : 'a -> 'b *)

¹No value restriction is needed for algebraic effects and handlers, O. Kammar and M. Pretnar, Journal of Functional Programming, January 2017

@murmour

This comment has been minimized.

Show comment
Hide comment
@murmour

murmour Apr 7, 2017

Contributor

A slight off-topic:

I've always found the assert false idiom distasteful, even though I often use it myself. Isn't it nonsensical to assert that false is true? Perhaps it would be better to have a specialized operator for this occasion, like assert_failure? With such an operator, there would be no need at all to make assert false a special case with peculiar typing rules.

Contributor

murmour commented Apr 7, 2017

A slight off-topic:

I've always found the assert false idiom distasteful, even though I often use it myself. Isn't it nonsensical to assert that false is true? Perhaps it would be better to have a specialized operator for this occasion, like assert_failure? With such an operator, there would be no need at all to make assert false a special case with peculiar typing rules.

@gasche

This comment has been minimized.

Show comment
Hide comment
@gasche

gasche Apr 7, 2017

Member

@yallop very elegant -- as usual. In particular, locally replacing assert false with let absurd (type a) : a = assert fase in absurd should always allow generalization. This proves that considering assert false and raise non-expansive is sound.

I wondered why the same argument would not apply to perform; the answer is that the return type of perform is not a polymorphic type variable like raise, it comes from the operation's signature. Exception-like operations have the empty return type that can be turned into forall a . a, but resumable operations have an inhabited return type that cannot.

Member

gasche commented Apr 7, 2017

@yallop very elegant -- as usual. In particular, locally replacing assert false with let absurd (type a) : a = assert fase in absurd should always allow generalization. This proves that considering assert false and raise non-expansive is sound.

I wondered why the same argument would not apply to perform; the answer is that the return type of perform is not a polymorphic type variable like raise, it comes from the operation's signature. Exception-like operations have the empty return type that can be turned into forall a . a, but resumable operations have an inhabited return type that cannot.

@xavierleroy

This comment has been minimized.

Show comment
Hide comment
@xavierleroy

xavierleroy Apr 8, 2017

Contributor

Isn't it nonsensical to assert that false is true?

Not if you're familiar with Hoare logic and similar specification frameworks. A "false" assertion on a program point is the usual way to express that the program point should not be reachable.

Likewise, assert(0) is a pretty common idiom in C and C++.

Contributor

xavierleroy commented Apr 8, 2017

Isn't it nonsensical to assert that false is true?

Not if you're familiar with Hoare logic and similar specification frameworks. A "false" assertion on a program point is the usual way to express that the program point should not be reachable.

Likewise, assert(0) is a pretty common idiom in C and C++.

@stedolan

This comment has been minimized.

Show comment
Hide comment
@stedolan

stedolan Apr 9, 2017

Contributor

Incidentally, this patch isn't the first to make raising an exception count as non-expansive. Partial matches are currently non-expansive, even though they may raise Match_failure:

# let f  (type a) :  a -> a list = match 1 with 1 -> fun x -> [x];;
Warning 8: this pattern-matching is not exhaustive.
Here is an example of a value that is not matched:
0
val f : 'a -> 'a list = <fun>
Contributor

stedolan commented Apr 9, 2017

Incidentally, this patch isn't the first to make raising an exception count as non-expansive. Partial matches are currently non-expansive, even though they may raise Match_failure:

# let f  (type a) :  a -> a list = match 1 with 1 -> fun x -> [x];;
Warning 8: this pattern-matching is not exhaustive.
Here is an example of a value that is not matched:
0
val f : 'a -> 'a list = <fun>
@stedolan

This comment has been minimized.

Show comment
Hide comment
@stedolan

stedolan Apr 9, 2017

Contributor

@xavierleroy

At any rate, if we decide to make assert false nonexpansive, we must make raiseexp nonexpansive as well. I am too lazy to write a proof but I have a feeling that it's type-safe.

@yallop and @gasche have now provided the proof :)

Making raise e nonexpansive seems to be a trickier change, since to detect raise correctly an environment is needed (to see whether %raise is being referred to, since Pervasives.raise may be shadowed), at which point nonexpansiveness ceases to be a purely syntactic property. Perhaps it would be better to make raise a keyword?

Contributor

stedolan commented Apr 9, 2017

@xavierleroy

At any rate, if we decide to make assert false nonexpansive, we must make raiseexp nonexpansive as well. I am too lazy to write a proof but I have a feeling that it's type-safe.

@yallop and @gasche have now provided the proof :)

Making raise e nonexpansive seems to be a trickier change, since to detect raise correctly an environment is needed (to see whether %raise is being referred to, since Pervasives.raise may be shadowed), at which point nonexpansiveness ceases to be a purely syntactic property. Perhaps it would be better to make raise a keyword?

@lpw25

This comment has been minimized.

Show comment
Hide comment
@lpw25

lpw25 Apr 9, 2017

Contributor

Perhaps it would be better to make raise a keyword?

Note that this would cause problems at Jane St., where raise is redefined to be reraise. Not an insurmountable problem, but I just wanted to point out that people do redefine raise in practice.

Contributor

lpw25 commented Apr 9, 2017

Perhaps it would be better to make raise a keyword?

Note that this would cause problems at Jane St., where raise is redefined to be reraise. Not an insurmountable problem, but I just wanted to point out that people do redefine raise in practice.

@gasche

This comment has been minimized.

Show comment
Hide comment
@gasche

gasche Apr 9, 2017

Member

I think it is now clear that the feature proposed in the PR is desirable, and that we cannot easily extend the scope of the current implementation. Unless somebody objects, I'm tempted to merge the current proposal as-is.

(I was tempted to ask for an assert false special casing, but in fact given that the type of the other cases is already non-polymorphic the type-checker behavior would be the same in both cases as far as I can tell, and semantically/operationally the reason why assert false is non-expansive also applies to the general construction.)

Member

gasche commented Apr 9, 2017

I think it is now clear that the feature proposed in the PR is desirable, and that we cannot easily extend the scope of the current implementation. Unless somebody objects, I'm tempted to merge the current proposal as-is.

(I was tempted to ask for an assert false special casing, but in fact given that the type of the other cases is already non-polymorphic the type-checker behavior would be the same in both cases as far as I can tell, and semantically/operationally the reason why assert false is non-expansive also applies to the general construction.)

@mshinwell

This comment has been minimized.

Show comment
Hide comment
@mshinwell

mshinwell Apr 10, 2017

Contributor

I think perhaps some of the discussion in this pull request should be documented as a comment in the code.

Contributor

mshinwell commented Apr 10, 2017

I think perhaps some of the discussion in this pull request should be documented as a comment in the code.

@gasche

This comment has been minimized.

Show comment
Hide comment
@gasche

gasche Apr 10, 2017

Member

Excellent idea; Jeremy's soundness proof would make for an excellent comment. @stedolan would you rebase?

Member

gasche commented Apr 10, 2017

Excellent idea; Jeremy's soundness proof would make for an excellent comment. @stedolan would you rebase?

@yallop

This comment has been minimized.

Show comment
Hide comment
@yallop

yallop May 10, 2017

Member

Making raise e nonexpansive seems to be a trickier change, since to detect raise correctly an environment is needed

Since primitives are resolved before is_nonexpansive, it's possible to detect raise reliably (i.e. handling shadowing correctly) without the need for an additional environment, by matching against something like this:

Texp_ident (_,_,{val_kind= Val_prim{Primitive.prim_name = "%raise"}})
Member

yallop commented May 10, 2017

Making raise e nonexpansive seems to be a trickier change, since to detect raise correctly an environment is needed

Since primitives are resolved before is_nonexpansive, it's possible to detect raise reliably (i.e. handling shadowing correctly) without the need for an additional environment, by matching against something like this:

Texp_ident (_,_,{val_kind= Val_prim{Primitive.prim_name = "%raise"}})
@stedolan

This comment has been minimized.

Show comment
Hide comment
@stedolan

stedolan May 12, 2017

Contributor

Apologies for the delay. I played with Jeremy's example a bit, and realised that the interactions between raise and nonexpansiveness are a lot more subtle than I thought. In particular, current trunk (without this patch) generalises the following:

let f =
  let thunk = lazy (raise (E (ref None)); ()) in
  fun () ->
    try Lazy.force thunk with E r -> ... r ...

So, it is possible to allocate and share a reference cell and yet count as "nonexpansive", but the communication across the lambda binding must happen at type exn. I think this is still sound, since there is no way of creating a new exn class that refers to the polymorphic type variable, and so there should be no way for different instantiations of f to instantiate the type of the reference in incompatible ways.

Still, this means that the soundness argument for the nonexpansiveness check is more complicated than I had imagined. On the other hand, I'm convinced by Jeremy's argument that the behaviour introduced here is no worse than what's already allowed (and besides, it's the same as pattern-match failure, which already generalises), so I'll add some comments and update the pull request.

Contributor

stedolan commented May 12, 2017

Apologies for the delay. I played with Jeremy's example a bit, and realised that the interactions between raise and nonexpansiveness are a lot more subtle than I thought. In particular, current trunk (without this patch) generalises the following:

let f =
  let thunk = lazy (raise (E (ref None)); ()) in
  fun () ->
    try Lazy.force thunk with E r -> ... r ...

So, it is possible to allocate and share a reference cell and yet count as "nonexpansive", but the communication across the lambda binding must happen at type exn. I think this is still sound, since there is no way of creating a new exn class that refers to the polymorphic type variable, and so there should be no way for different instantiations of f to instantiate the type of the reference in incompatible ways.

Still, this means that the soundness argument for the nonexpansiveness check is more complicated than I had imagined. On the other hand, I'm convinced by Jeremy's argument that the behaviour introduced here is no worse than what's already allowed (and besides, it's the same as pattern-match failure, which already generalises), so I'll add some comments and update the pull request.

@stedolan

This comment has been minimized.

Show comment
Hide comment
@stedolan

stedolan May 12, 2017

Contributor

In fact, the relaxed value restriction is not needed to justify generalising raise e. First, define a diverging function and a lazy application of it:

let rec diverge () = diverge ()
let ldiv = lazy (diverge ())

Then, under the definition of "nonexpansive" in trunk, the following is nonexpansive and has semantics equivalent to raise e:

(raise e; let lazy a = ldiv in a)

Oddly, this is nonexpansive regardless of whether e is nonexpansive.

Contributor

stedolan commented May 12, 2017

In fact, the relaxed value restriction is not needed to justify generalising raise e. First, define a diverging function and a lazy application of it:

let rec diverge () = diverge ()
let ldiv = lazy (diverge ())

Then, under the definition of "nonexpansive" in trunk, the following is nonexpansive and has semantics equivalent to raise e:

(raise e; let lazy a = ldiv in a)

Oddly, this is nonexpansive regardless of whether e is nonexpansive.

Make (raise e) nonexpansive.
Test in typing-poly/poly.ml.
@stedolan

This comment has been minimized.

Show comment
Hide comment
@stedolan

stedolan May 12, 2017

Contributor

I've updated the pull request with Jeremy's check for raise e, so this now marks raise e as nonexpansive as well as assert e.

Any other changes requested?

Contributor

stedolan commented May 12, 2017

I've updated the pull request with Jeremy's check for raise e, so this now marks raise e as nonexpansive as well as assert e.

Any other changes requested?

@yallop

This comment has been minimized.

Show comment
Hide comment
@yallop

yallop May 12, 2017

Member

[Not intended to delay merging; just continuing the discussion!]

In fact, the relaxed value restriction is not needed to justify generalising raise e. First, define a diverging function and a lazy application of it:

let rec diverge () = diverge ()
let ldiv = lazy (diverge ())

For what it's worth, this still relies on the relaxed value restriction; it won't generalize if you give it an invariant type:

let rec diverge () = diverge ()
let ldiv : ('a -> 'a) Lazy.t = lazy (diverge ())

Perhaps counterintuitively, even though lazy e doesn't reduce, it can't be treated as a value for the purposes of generalization, because it introduces observable sharing. Put another way, for generalization call-by-need should be treated like call-by-value, which needs a value restriction, not like call-by-name, which doesn't¹.

¹ See, e.g. @xavierleroy's "Polymorphism by name for references and continuations" from POPL 1993

Member

yallop commented May 12, 2017

[Not intended to delay merging; just continuing the discussion!]

In fact, the relaxed value restriction is not needed to justify generalising raise e. First, define a diverging function and a lazy application of it:

let rec diverge () = diverge ()
let ldiv = lazy (diverge ())

For what it's worth, this still relies on the relaxed value restriction; it won't generalize if you give it an invariant type:

let rec diverge () = diverge ()
let ldiv : ('a -> 'a) Lazy.t = lazy (diverge ())

Perhaps counterintuitively, even though lazy e doesn't reduce, it can't be treated as a value for the purposes of generalization, because it introduces observable sharing. Put another way, for generalization call-by-need should be treated like call-by-value, which needs a value restriction, not like call-by-name, which doesn't¹.

¹ See, e.g. @xavierleroy's "Polymorphism by name for references and continuations" from POPL 1993

@stedolan

This comment has been minimized.

Show comment
Hide comment
@stedolan

stedolan May 12, 2017

Contributor

For what it's worth, this still relies on the relaxed value restriction; it won't generalize if you give it an invariant type.

Ah, you're right. Here's an alternative version, using pattern-match failure instead of divergence. Define:

type t = A | B of { magic : 'a . 'a }

Then, raise e is equivalent to:

(raise e; match A with B { magic } -> magic)

which is accepted as nonexpansive, even without this patch.

Perhaps counterintuitively, even though lazy e doesn't reduce, it can't be treated as a value for the purposes of generalization, because it introduces observable sharing. Put another way, for generalization call-by-need should be treated like call-by-value, which needs a value restriction, not like call-by-name, which doesn't¹.

Yes, that makes sense (Thanks for the reference, btw!). The bit that I'm finding odd is how this interacts with the expansiveness check for sequencing, which states that e1; e2 is nonexpansive iff e2 is, regardless of what's in e1. That means that lazy (raise e; ()) is nonexpansive, regardless of what e is.

Contributor

stedolan commented May 12, 2017

For what it's worth, this still relies on the relaxed value restriction; it won't generalize if you give it an invariant type.

Ah, you're right. Here's an alternative version, using pattern-match failure instead of divergence. Define:

type t = A | B of { magic : 'a . 'a }

Then, raise e is equivalent to:

(raise e; match A with B { magic } -> magic)

which is accepted as nonexpansive, even without this patch.

Perhaps counterintuitively, even though lazy e doesn't reduce, it can't be treated as a value for the purposes of generalization, because it introduces observable sharing. Put another way, for generalization call-by-need should be treated like call-by-value, which needs a value restriction, not like call-by-name, which doesn't¹.

Yes, that makes sense (Thanks for the reference, btw!). The bit that I'm finding odd is how this interacts with the expansiveness check for sequencing, which states that e1; e2 is nonexpansive iff e2 is, regardless of what's in e1. That means that lazy (raise e; ()) is nonexpansive, regardless of what e is.

@yallop

This comment has been minimized.

Show comment
Hide comment
@yallop

yallop May 12, 2017

Member

The bit that I'm finding odd is how this interacts with the expansiveness check for sequencing, which states that e1; e2 is nonexpansive iff e2 is, regardless of what's in e1.

The way I rationalize this is that

let y = e1; e2 in
 e3

is equivalent to

let x = e1 in
let y = e2 in
 e3

where x is fresh for e2 and e3. Then the only way for the types of e1 and e2 to interact is via variables already in the environment, which won't be generalized in any case.

Member

yallop commented May 12, 2017

The bit that I'm finding odd is how this interacts with the expansiveness check for sequencing, which states that e1; e2 is nonexpansive iff e2 is, regardless of what's in e1.

The way I rationalize this is that

let y = e1; e2 in
 e3

is equivalent to

let x = e1 in
let y = e2 in
 e3

where x is fresh for e2 and e3. Then the only way for the types of e1 and e2 to interact is via variables already in the environment, which won't be generalized in any case.

@stedolan

This comment has been minimized.

Show comment
Hide comment
@stedolan

stedolan May 12, 2017

Contributor

Then the only way for the types of e1 and e2 to interact is via variables already in the environment, which won't be generalized in any case.

Ah, I think I understand better now. So, are you saying that it is safe to treat let x : t = e1 in e2 as a "value", regardless of what computation e1 does, as long as no type variable to be generalised appears free in t? So e1 can allocate polymorphic references, etc, and even pass them to e2, as long as e2 doesn't know that they are polymophic references.

Contributor

stedolan commented May 12, 2017

Then the only way for the types of e1 and e2 to interact is via variables already in the environment, which won't be generalized in any case.

Ah, I think I understand better now. So, are you saying that it is safe to treat let x : t = e1 in e2 as a "value", regardless of what computation e1 does, as long as no type variable to be generalised appears free in t? So e1 can allocate polymorphic references, etc, and even pass them to e2, as long as e2 doesn't know that they are polymophic references.

@yallop

This comment has been minimized.

Show comment
Hide comment
@yallop

yallop May 15, 2017

Member

Right, I think the same argument works for let x: t = e1 in v.

Member

yallop commented May 15, 2017

Right, I think the same argument works for let x: t = e1 in v.

@gasche gasche merged commit 93c087a into ocaml:trunk Jun 4, 2017

2 checks passed

continuous-integration/appveyor/pr AppVeyor build succeeded
Details
continuous-integration/travis-ci/pr The Travis CI build passed
Details
@gasche

This comment has been minimized.

Show comment
Hide comment
@gasche

gasche Jun 4, 2017

Member

The discussion has quieted down on a consensus that the feature is useful and sound, and a nicer implementation (thanks to Jeremy's review and comments), so I went ahead and merged. Thanks!

Member

gasche commented Jun 4, 2017

The discussion has quieted down on a consensus that the feature is useful and sound, and a nicer implementation (thanks to Jeremy's review and comments), so I went ahead and merged. Thanks!

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment