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

Value restriction is applied on covariant function types, but not if the type definition is hidden #7154

Closed
vicuna opened this issue Feb 20, 2016 · 4 comments
Assignees

Comments

@vicuna
Copy link

vicuna commented Feb 20, 2016

Original bug ID: 7154
Reporter: nore
Assigned to: @garrigue
Status: closed (set by @xavierleroy on 2017-09-24T15:31:52Z)
Resolution: not a bug
Priority: normal
Severity: minor
Version: 4.01.0
Category: typing
Monitored by: @Drup @gasche @yallop

Bug description

Defining type 'a t to be ('a -> int) -> int, in which type 'a is covariant, applying the identity function on an object of type 'a t gives an object of type '_a t. However, if the definition of type 'a t is hidden in a module, with the signature showing 'a to be covariant in t, then the result is of type 'a t. Thus, hiding the definition of the type makes a more general type to be inferred.

Steps to reproduce

let id r = r;;

val id : 'a -> 'a =

type 'a t = ('a -> int) -> int;;

type 'a t = ('a -> int) -> int

let u : 'a t = fun x -> 0;;

val u : 'a t =

id u;;

  • : '_a t =

module X : sig type +'a t val u : 'a t end = struct type 'a t = ('a -> int) -> int let u x = assert false end;;

module X : sig type +'a t val u : 'a t end

id X.u;;

  • : 'a X.t =
@vicuna
Copy link
Author

vicuna commented Feb 21, 2016

Comment author: @garrigue

This is a feature:
Since ('a -> int) -> int is an instance of 'b -> int (where 'b is contravariant), it would not be principal to allow generalizing it. So the precise definition is that a type variable is generalizable if it doesn't appear under a negative position (simply stated, inside the left side of an arrow, or as inside the parameter of a contravariant or invariant type).
There is no such problem with 'a X.t, as X.t is covariant, and 'a is its direct parameter.

If we were to document this, I'm not sure where it would go: there is no statement about the value restriction in the reference manual, as far as I know. Maybe we should add a section about typing somewhere, but we cannot write down all the specification there...

@vicuna
Copy link
Author

vicuna commented Feb 21, 2016

Comment author: @lpw25

IIUC this is because contravariant variables cannot be generalised, which is because OCaml doesn't have a uniform value representation, which is because of the float array hack. So if in the future the float array hack were removed then this issue could be addressed.

@vicuna
Copy link
Author

vicuna commented Feb 21, 2016

Comment author: @Drup

this is because contravariant variables cannot be generalised, which is because OCaml doesn't have a uniform value representation

Can you explain that part ?

@vicuna
Copy link
Author

vicuna commented Feb 21, 2016

Comment author: @gasche

Can you explain that part ?

You should have a look at Jacques' article on the value restriction:

Relaxing the Value Restriction
Jacques Garrigue, 2004
http://caml.inria.fr/pub/papers/garrigue-value_restriction-fiwflp04.pdf

this question is discussed in the Conclusion section.

The intuition for the argument is as follows: to justify that generalizing variables occurring in positive solutions is sound (generalizing T('_a)), one may consider unifying them with the bottom type (no inhabitant, subtype of everything), and using subtyping to argue that T(bottom) is a subtype of T('a) for any 'a, and thus (forall 'a . T('a)) is a valid type.

To work on types that occur in negative positions, we would need to instantiate with T(top). But the current OCaml implementation admits no top type, as is suggest by the following segfault (example from the article):

let t = Array.create 2 (Obj.repr 0.0);;
t.(1) <- Obj.repr 1;; (* segfault *)

(With GADTs or first-class modules we can pack any value in an existential, but this always implies the use of a boxing construction. A top type would require subtyping, that is cast to a universal type without change to the value representation.)

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

No branches or pull requests

2 participants