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

Object-like notation for calling regular functions #6822

Closed
vicuna opened this issue Mar 26, 2015 · 45 comments
Closed

Object-like notation for calling regular functions #6822

vicuna opened this issue Mar 26, 2015 · 45 comments

Comments

@vicuna
Copy link

vicuna commented Mar 26, 2015

Original bug ID: 6822
Reporter: @alainfrisch
Status: acknowledged (set by @damiendoligez on 2015-06-15T15:12:55Z)
Resolution: open
Priority: normal
Severity: feature
Target version: later
Category: language features
Monitored by: @trefis @Drup @diml

Bug description

It is a common idiom to have a type defined in a module with a bunch of functions associated to it, all taking an object of that type as a first argument:

module Foo : sig

type t

val create: int -> t

val invert: t -> t
val name: t -> string
val set_name: t -> string -> unit

end

This is similar to OO-style and it is thus tempting to provide support for making this easier, in particular to avoid explicit reference to module Foo.

Now that the dot notation "e.l" has special support to rely on type information already known for "e" before resolving "l", one could very well support even more overloading for it, so as to allow writing:

(M.create 42).invert.name

When type-checking "e.l" and "e" is known to have a type M1....Mn.t which turns out to be abstract (or at least, something which is known not to be a record type), one could turn this automatically to a function application "M1.....Mn.l e", i.e. lookup for function with name "l" in the module that defines the type for "e".

Similarly, "e1.l <- e2" could be turned into "M1.....Mn.set_l e1 e2".

I'm attaching a very naive POC for this idea (error reporting is ugly and the expression "e.l" is type-checked twice, which should be avoided).

Alternatively, one could invent a different syntax.

(For the records, Fabrice Le Fessant came up with a similar suggestion which was briefly discussed on caml-devel in May 2013.)

File attachments

@vicuna
Copy link
Author

vicuna commented Mar 26, 2015

Comment author: @lpw25

I don't think this would be coherent -- the runtime semantics will depend on the whims of the type-checker. The idea of "the module that defines the type for e" is not well-defined and is going to depend on how type aliases are handled.

I would suggest a more principled approach to ad-hoc polymorphism (i.e. modular implicits).

@vicuna
Copy link
Author

vicuna commented Mar 26, 2015

Comment author: @alainfrisch

If we expand type-aliases until reaching an abstract type, are there cases where this is not well-defined?

In Fabrice's original proposal, the idea was rather to specify explicitly the module to which a given identifier "x" is attached to when resolving "x.f", but this is more heavy and doesn't allow to chain method calls.

@vicuna
Copy link
Author

vicuna commented Mar 26, 2015

Comment author: @dbuenzli

Personally I'm not in favour of multiplying notations for calling functions and/or overloading notations, it leads to less readable code. Your example can already be written:

M.(create 42 |> invert |> name)

which may not be as compact but almost as much without introducing any new notation.

@vicuna
Copy link
Author

vicuna commented Mar 26, 2015

Comment author: @alainfrisch

The style you propose works well when all objects live in the same module. Cf the current discussion on the ocsigen mailing list. The current proposals allows to reduce:

let elt = Document.getElementById doc "canvas" in
let ctx = Canvas.(getContext_2d (of_element elt)) in
Canvas.RenderingContext2D.(begin
set_fillStyle ctx "rgba(0,0,255,0.5)";
fillRect ctx 30 30 50 50
end);

to:

let elt = doc.getElementById "canvas" in
let ctx = (Canvas.of_element elt).getContext_2d in
ctx.set_fillStyle "rgba(0,0,255,0.5)";
ctx.fillRect 30 30 50 50

@vicuna
Copy link
Author

vicuna commented Mar 26, 2015

Comment author: @trefis

Personally I'm not in favour of multiplying notations for calling functions and/or overloading notations, it leads to less readable code.

I couldn't agree more

Your example can already be written:
M.(create 42 |> invert |> name)
which may not be as compact but almost as much without introducing any new notation.

Except it's not equivalent. If invert had type "t -> M2.t" then name would have been fetched in M2 ("hopefully").

@vicuna
Copy link
Author

vicuna commented Mar 26, 2015

Comment author: @trefis

ctx.set_fillStyle "rgba(0,0,255,0.5)";

Didn't you mean:

ctx.fillStyle <- "rgba(...)";

?

On a similar subject:

Similarly, "e1.l <- e2" could be turned into "M1.....Mn.set_l e1 e2".

Should "similary" here be understood as "just as random and ad-hoc but happens to match perfectly well the example I have in mind"?
Personnaly, I prefer to call my update functions "update_field" instead of "set_field". Maybe we could use attributes to help the type checker decide how the ast should be rewritten, e.g.

x.l <-[@name "update"] e1

would translate to

SomeM.update_l x e1

And in the absence of attribute a default prefix would be chosen.
Whether that default prefix is "set" or "update" should probably be discussed with the community, to see what people like most (or we could do some stats on published opam packages).

@vicuna
Copy link
Author

vicuna commented Mar 26, 2015

Comment author: @dbuenzli

The current proposals allows to reduce:

By which you haven't gained much w.r.t. to the obsfuscations the new syntax allows. Frankly I'm completely opposed to support JavaScript like programming in OCaml.

@vicuna
Copy link
Author

vicuna commented Mar 26, 2015

Comment author: @lpw25

If we expand type-aliases until reaching an abstract type, are there cases where this is not well-defined?

Consider:

module M : sig
  module B : sig
    type t = T
    val f : t -> int
  end
  module A : sig
    type t = B.t = T
    val f : t -> int
  end
  val x : A.t
end = struct
  module A = struct
    type t = T
    let f T = 1
  end
  module B = struct
    type t = A.t = T
    let f T = 0
  end

  let x = A.T

  let y1 = x.f
end

let y2 = M.x.f

The examples get worse when you start using functors.

This is also the reason why we don't support higher-kinded
polymorphism in the core language: it requires a notion of the
definition of a type, but such a notion does not exist.

It is also worth noting that this proposal only gives
you "first-order" ad-hoc polymorphism. For example, the following
does not work:

let f x = x.foo

A better approach (if an object-style syntax is really desired)
would be to add a syntax:

x##foo

which was just short-hand for foo x, then you can use implicits
to do the ad-hoc polymorphism part:

module type Invertable = sig
  type t
  val invert: t -> t
end

let invert (implicit I : Invertable) x = I.invert x

module type Named = sig
  type t
  val name: t -> string
end

let name (implicit N : Named) x = N.name x

implicit M

(M.create 42)##invert##name

@vicuna
Copy link
Author

vicuna commented Mar 26, 2015

Comment author: @lefessan

Alain used this notation for Javascript, but I proposed it for a totally different context (a binding to C++ for wxOCaml), and I am experiencing again these days with another similar context. Whoever is concerned a little about interactions between OCaml and other object-oriented languages will probably hit this problem one day or another...

My own proposition was purely syntactic: it was to associate a module with a variable name, and then prefix with the module name each time the variable is used with a specific notation:

let (x <- MODULE) =
x->f1 a;
x->f2 b;
()

would translate into

let x =
MODULE.f1 x a;
MODULE.f2 x b;
()

@vicuna
Copy link
Author

vicuna commented Mar 27, 2015

Comment author: @garrigue

There is already a long discussion, but I just wanted to mention that (although some people do not seem to think so) the use of type information to resolve record labels is not overloading. Namely, record labels behave in a uniform way: label x extracts the field x of the record, whatever this record is. This is certainly not the case with arbitrary functions.
So this proposal is not about adding more overloading, but about introducing overloading in a language which has none (intentionally).

By the way, I also know that some people dislike objects, but I think that LablGTK shows how one can use object wrappers without having the user get too much entangled with objects.
Here again, there is no overloading.

@vicuna
Copy link
Author

vicuna commented Mar 27, 2015

Comment author: @alainfrisch

Re lpw25:

Consider:

Well, yes, in different contexts, the "fully expanded type definition" associated to a type path can be different; is this fundamentally different from saying that in different contexts, a value path will be interpreted in different ways, which is obvious?

@vicuna
Copy link
Author

vicuna commented Mar 27, 2015

Comment author: @alainfrisch

Re trefis:

ctx.set_fillStyle "rgba(0,0,255,0.5)";
Didn't you mean:
ctx.fillStyle <- "rgba(...)";

Both would be equivalent. As you notice, supporting "<-" introduces some more ad hoc-ness (choice of a default naming convention), and it doesn't bring much since
"ctx.set_fillStyle xxx" is not really worse than "ctx.fillStyle <- xxx".

@vicuna
Copy link
Author

vicuna commented Mar 27, 2015

Comment author: @lpw25

Well, yes, in different contexts, the "fully expanded type definition" associated to a type path can be different; is this fundamentally different from saying that in different contexts, a value path will be interpreted in different ways, which is obvious?

They are fundementally very different. In different contexts two syntactically equivalent expressions may refer to different values with the same names, and so have different behaviour. Here we have two expressions which refer to the same value, but their behaviour is different based on which of two equivalent types some value has.

This is already quite bad, because seemingly innocuous changes like exposing a previously abstract type's definition can silently change the program's behaviour.

However, if the type-checker gets involved in the decision about which of the equivalent types is chosen then it gets even worse -- we have incoherence.

For example:

module type S = sig
  module rec A : sig
    type t
    val f : t -> int
    val x : t
  end and B : sig
    type t = A.t
    val f : t -> int
    val x : t
  end
end

module type T = sig
  module rec A : sig
    type t = B.t
    val f : t -> int
    val x : t
  end and B : sig
    type t
    val f : t -> int
    val x : t
  end
end

let f (x : (module S)) (y : (module T)) =
  if true then x else y;;

module M = struct
  module rec A : sig
    type t = B.t
    val f : t -> int
    val x : t
  end = struct
    type t = B.t
    let f _ = 1
    let x = B.x
  end and B : sig
    type t
    val f : t -> int
    val x : t
  end = struct
    type t = T
    let f _ = 0
    let x = T
  end
end

module N = (val f (module M) (module M))

N.B.x.f

I believe similar examples can be created using GADTs. In the future we may wish to add other cases where a module type is inferred, and each of these would also cause incoherence with this proposal.

@vicuna
Copy link
Author

vicuna commented Mar 27, 2015

Comment author: @Drup

As other people mentioned in this thread, and it has been proven multiple time in various other (mainstream) programming languages, having multiple notations for function call is a very bad idea.

@vicuna
Copy link
Author

vicuna commented Mar 30, 2015

Comment author: @alainfrisch

Thanks Leo for the example. I forget, indeed, that the unpacking type for first-class modules can now be inferred. I'm wondering, mostly out of curiosity -- because the proposal will be discarded anyway -- if/how one could define restrictions to ensure that the definition of "the type definition corresponding to the type inferred for a given expression" would be well-defined (this would reject the example you give, for instance). It's unfortunate when type inference has the effect of preventing features that would enable lighter code.

@vicuna
Copy link
Author

vicuna commented Mar 30, 2015

Comment author: @lpw25

Personally, I think that the idea of a type having a single specific definition is essentially incompatible with the idea of modular abstraction. It exists in languages, such as Haskell, which forgo modular abstraction in exchange for easier implementations of language features such as type classes and higher-kinded types. However, I think that this is fundamentally wrong -- modular abstraction is paramount and anything which doesn't fit with it should be considered suspect as a language feature.

Even with enough restrictions to ensure that using the "fully expanded type definition" did not depend on inference, it would still be a very unstable concept, since revealing the definition of an abstract type can silently change it. If your run-time semantics depends on this concept then revealing an abstraction can silently change the semantics. This really should not happen in a language that takes abstraction seriously, revealing an abstraction should not change a program's meaning -- at worst it should cause a new compilation error.

@vicuna
Copy link
Author

vicuna commented Mar 31, 2015

Comment author: @alainfrisch

If your run-time semantics depends on this concept then revealing an abstraction can silently change the semantics.

I'm used to that: runtime types also share this property, and I don't see how you can provide compiler support for them without indeed breaking the property that revealing the definition of an abstract type can change the semantics of the program.

The alternative to compiler support can be, for instance, to rely on external tools (e.g. to generate value representation for type definitions). For the user, this doesn't change much: revealing the definition of an abstract type will in practice (because of the external tools) change the semantics.

That said, I think it would be interesting to keep track of which types (base and module level) have been explicitly defined or propagated with well-defined rules. This would allow to introduce features such as this object notation without breaking modular abstraction.

@vicuna
Copy link
Author

vicuna commented Mar 31, 2015

Comment author: @lpw25

I'm used to that: runtime types also share this property, and I don't see how you can provide compiler support for them without indeed breaking the property that revealing the definition of an abstract type can change the semantics of the program.

By using a system that ensures that if you reveal an abstraction, such that there are now two possible semantics you get a compile-time error. This is how implicits work, and it is how a proper implementation of runtime types would have to work as well.

That said, I think it would be interesting to keep track of which types (base and module level) have been explicitly defined or propagated with well-defined rules. This would allow to introduce features such as this object notation without breaking modular abstraction.

The only "well-defined" approach to this is to have linear type system for type definitions. Considering how OCaml's module system is path-based, it is hard to see how this would work in OCaml.

@vicuna
Copy link
Author

vicuna commented Mar 31, 2015

Comment author: @alainfrisch

and it is how a proper implementation of runtime types would have to work as well.

I'd be interested to see such a proposal, and how it would be usable (for our current use cases). I don't believe this is possible but I'd love to be proven wrong.

The only "well-defined" approach to this is to have linear type system for type definitions.

I don't think so. Perhaps the definition of such a system would look very procedural and not very declarative, but this doesn't mean it doesn't exist nor that it would be difficult to understand by users.

Basically, the definition could be something like: "apply a brain-dead propagation algorithm (with black boxes to represent type parts which remain unknown), and see what you get". The algorithm would propagate explicit type annotation from function parameters to their use site, would deal at least with applying a function with a known non-polymorphic type, etc.

@vicuna
Copy link
Author

vicuna commented Mar 31, 2015

Comment author: @lpw25

I'd be interested to see such a proposal, and how it would be usable (for our current use cases). I don't believe this is possible but I'd love to be proven wrong.

I think that it is probably possible (and it felt like Gregoire might have been getting close), but it is certainly a difficult problem.

It is also not clear to me that it offers any substantial advantages over an implicits-style system.

I don't think so. ...

Sorry I misunderstood what you meant. As I said earlier, even if you know which types have not required inference it only ensures systems which rely on anti-modular concepts (e.g. idea of a type having a single definition) coherent -- it doesn't make them any less fragile.

@vicuna
Copy link
Author

vicuna commented Mar 31, 2015

Comment author: @alainfrisch

I think that it is probably possible

At least for the way we use our runtime types, it is a desired property that the runtime semantics is different between abstract and transparent types.

even if you know which types have not required inference it only ensures systems which rely on anti-modular concepts

Yes, my claim is that some language features are both anti-modular and useful. You can decide to reject by principle any anti-modular feature, it's certainly a valid design decision. Another one is to accept anti-modular features, in a controlled way, and let people decide whether to use them or not.

@vicuna
Copy link
Author

vicuna commented Mar 31, 2015

Comment author: @lpw25

Yes, my claim is that some language features are both anti-modular and useful.

Sure, just like some language features are both type unsound and useful. But you don't put those in the language, you either find sound modular features that address the same use-cases, or you provide extra-linguistic workarounds (e.g. Obj.magic).

@vicuna
Copy link
Author

vicuna commented Mar 31, 2015

Comment author: @alainfrisch

But you don't put those in the language

Language design is an art of compromises and trade-offs, taking into account the current state of knowledge, contradictory design principles and even goals, and pragmatic considerations. OCaml is full of trade-offs that could be considered "dangerous", such as:

  • Side-effects are difficult to reason about and have bad parallelization properties. OCaml encourages a more side-effect free style than most languages, yet it allows side-effects.

  • Recursion is the natural way to express many problems and is a natural fit for a functional programming language. Yet OCaml relies on the system stack and puts arbitrary limits on the recursion depth, forcing library authors to document non tail-recursiveness of their functions and programmers to think about this problem and adapt their code accordingly. Stack overflows result in segfaults on some supported architecture.

  • Type soundness is important, yet OCaml's standard library, even Pervasives, contain functions that break it.

  • Memory management should be automatic and transparent, yet OCaml includes ways to have your program's behavior depend on when the GC runs (finalizers, weak arrays).

  • OCaml has both thread libraries and a thread-unsafe standard library, which is a huge risk in terms of code robustness (even "Lazy" is not thread-safe).

  • A language should come with a formal definition of its static and dynamic semantics, yet OCaml is far from having one.

  • Whitespace-insensitivity can be considered as a good property of a language syntax, yet it's being considered to drop this for docstrings.

Now, one could at the end decide that features should be discarded as being too dangerous because the semantics of programs could depend on whether a type is kept abstract or not, and tell people to use even more dangerous alternatives instead (such as syntactic code preprocessing to compensate the lack of generic programming features). But (i) I don't think that breaking this property is more dangerous than other existing trade-offs, esp. if this only affect well defined features that people can easily choose not to use, (ii) simply saying "you don't put those in the language" (and putting that on the same level as type unsoundness) is a debatable axiom, not an argument, and it doesn't bring much to the discussion.

@vicuna
Copy link
Author

vicuna commented Mar 31, 2015

Comment author: @lpw25

OCaml is full of trade-offs that could be considered "dangerous", such as:

I would like to point out that none of the trade-offs listed are in the type-system (well I guess the side-effects point could be considered a type-system issue). The type-system has remained relatively clean in its design, and in particular it is about the only language (or a member of the only family of languages) which take modular abstraction seriously.

Personally, I think that this respect for modularity is one of the most important reasons that OCaml "works" as a lagnuage. Even though it supports many different language features, the emphasis on abstraction allows these features to coexist without interfering with each other (unlike certain languages I might mention cough C++ cough). I think that any shift away from this healthy respect for abstraction (by including type-system features which are anti-modular) would be a mistake.

@vicuna
Copy link
Author

vicuna commented Mar 31, 2015

Comment author: @alainfrisch

I should probably test it out myself, but can you clarify on how modular implicits preserve the property that exposing or not the definition of abstract types cannot change the semantics of programs (assuming they remain well-typed). In particular, consider the standard "Show" example, and the following definitions:

module X : sig
type t
val x: t
val f1: t -> string
val f2: t -> string
end = struct ... end

module M1_concrete
: sig type t = X.t val show: t -> string end
= struct type t = X.t let show = X.f1 end
module M1_abstract
: sig type t val show: t -> string end
= struct type t = X.t let show = X.f1 end
module M2_concrete
: sig type t = X.t val show: t -> string end
= struct type t = X.t let show = X.f2 end
module M2_abstract
: sig type t val show: t -> string end
= struct type t = X.t let show = X.f2 end

Then which combinations of these modules can be declared as implicit together in order to allow "show X.x"?
I would have assumed that M1_concrete+M2_abstract would work, and also M1_abstract+M2_concrete (but not M1_concrete+M2_concrete), using respectively X.f1 and X.f2 to print X.x, but this is certainly not the case.

@vicuna
Copy link
Author

vicuna commented Mar 31, 2015

Comment author: @lpw25

I should probably test it out myself, but can you clarify on how modular implicits preserve the property that exposing or not the definition of abstract types cannot change the semantics of programs

It is not about exposing or not the definition it is only about exposing a previously abstract definition that breaks abstraction. Revealing more information about a type should not change semantics. Choosing to hide previously known information is a different matter. So in your example trying to move from (concrete, abstract) or (abstract, concrete) to (concrete, concrete) will produce an ambiguity error.

It is important to distinguish between deciding to change an API by uncovering an abstraction -- which should always be a fundamentally safe operation, from deciding to change an API by abstracting a previously exposed definition -- which is always going to be a fundamentally risky operation.

That is why it is important to ensure that revealing additional information does not silently change semantics -- it should always be a safe operation because that is the nature of abstraction: hiding information means it is safe to choose any value for that information.

However, I take your point: it is certainly not ideal that abstracting a previously exposed definition (whilst simultaneously revealing a previously abstracted definition) can silently change semantics. I never said it was a perfect proposal -- the nature of ad-hoc polymorphism inevitably means giving you more rope -- but I would maintain that this is still a distinct and important improvement over proposals which break the notion of abstraction.

@vicuna
Copy link
Author

vicuna commented Apr 1, 2015

Comment author: @alainfrisch

It is not about exposing or not the definition it is only about exposing a previously abstract definition that breaks abstraction.

Sorry, I don't follow the asymmetry. Do you agree that the following properties are equivalent, and that (i) is the one you insist to keep?

(i) If P1 and P2 are well-typed programs, and P2 is obtained from P1 by making a type abstract, then P1 and P2 have the same semantics.

(ii) If P1 and P2 are well-typed programs, and P2 is obtained from P1 by revealing the definition of an type abstract, then P1 and P2 have the same semantics.

(iii) If P1, ..., Pn are well-typed programs, with each Pi+1 obtained from the previous Pi either by abstracting a concrete type or revealing an abstract type, then P1 and Pn have the same semantics.

It seems that modular implicits maintain these properties, but break:

(iii') If P1 and Pn are well-typed programs, and Pn is obtained from P1 by applying N "changes" simultaneously (each change being a switch from abstract to concrete or the opposite), then P1 and Pn have the same semantics.

Now, I don't see why (iii) should be considered much more important than (iii'): what does it bring in practice?

=======================================

Moreover, let me point out that (i) is not formally satisfied by the current OCaml implementations:

module X : sig 
  type t = false
  val x: t
end  =
struct
  type t = float
  let x = 1.
end

type t = {x: X.t}

let () = Printf.printf "%b\n%!" ({x = X.x}.x == X.x)

Making X.t abstract changes the result of this program. (Yes, I know that the semantics of ( == ) is not completely specified.)

=======================================

Finally, I'd also like to mention other properties that people might consider very important (more than (i)-(ii)-(iii)):

  • There is a natural untyped semantics for the language (i.e. an untyped language obtained by erasing all type information;
    in this "semantics", record fields are identified by names, so type-based resolution doesn't break this property).

  • Consequently, if two well-typed programs differ only by a type annotation, they have the same semantics.

If I understand correctly, modular implicits break these properties.

Note that I've nothing against breaking these properties, as long as the reasons for the breakage are well identified and it remains trivial to program in a subset of the language where the properties still hold. In my opinion, it's the exact same kind of trade-offs one would have to do to accept runtime types: by definition, if we reflect static type definitions at runtime (including the fact that a type is abstract or not), then we somehow "break abstraction". This is well understood, extremely useful in some cases, and can easily be avoided by programmers who don't like that.

Coming back to the original proposal, the "error" is probably to overload an existing language constructions. It'd be better to introduce a new syntatic form, to make it easy to avoid the feature, if desired.

@vicuna
Copy link
Author

vicuna commented Apr 1, 2015

Comment author: @lpw25

Now, I don't see why (iii) should be considered much more important than (iii'): what does it bring in practice?

It is not (iii) that I am saying is more important, but the missing (iv):

(iv) If P1 and Pn are well-typed programs, and Pn is obtained from P1 by revealing the definition of N types simultaneously, then P1 and Pn have the same semantics.

Making X.t abstract changes the result of this program. (Yes, I know that the semantics of ( == ) is not completely specified.)

You've answered your own question there. == is not specified on immutable types, precisely so that the compiler can make optimizations which copy immutable types without it being considered changing the semantics of the program.


Anyway, I have not phrased my objections at all well (rather lazily referring to the problem as "breaking the notion abstraction"). So I will try again.

The aim of ad-hoc polymorphism is to take a program which has multiple possible semantic meanings (some of which are ill-typed) and to use type information to choose one particular meaning.

This interacts with abstraction because abstracting or revealing type information changes the number of programs which are well typed. Revealing an abstraction can only increase the number of programs which are well-typed, and adding a new abstraction can only reduce the number of programs that are well-typed. Without any ad-hoc polymorphism, this means that revealing an abstraction will never break a program, whilst adding an abstraction might make the program ill-typed. Also, without ad-hoc polymorphism adding and removing abstractions cannot affect the semantics of a program.

When faced with multiple well-typed programs to select from, modular implicits will always give an ambiguity error. Whereas Haskell's type-classes (with overlapping instances turned on) and Scala's implicits will use a stable ordering on types to choose from amongst the options. The proposal in this issue uses an unstable ordering to choose from amongst the options. This ordering essentially treats

sig type a type b = a end

differently from

sig type b type a = b end

even though OCaml considers these types as equivalent, which makes the ordering unstable.

I think that allowing ambiguity at all is dangerous and makes it harder to reason about program behaviour. I think having the ordering between choices be unstable and explicitly based on whether a type is abstract or not, is very dangerous and makes reasoning about program behaviour even harder.

One of the reasons I dislike solutions which allow ambiguity is because I think that they make the interaction between abstraction and ad-hoc polymorphism worse, since they allow revealing a type's definition to silently change the semantics of the program. So an operation, which could previously always be made without even risking a program failing to compile, can now silently cause bugs (which support for ambiguity then makes hard to track down).

However, the proposal in this issue doesn't just interact with abstraction by supporting ambiguity -- the ordering with which it decides that ambiguity is itself determined by whether types are abstract. It is this second form of interaction which I was originally complaining about as being anti-modular. It seems very fragile, and quite likely to cause subtle bugs.

So, in summary, the property we have been discussing for the last few messages is one of the reasons that I dislike ad-hoc polymorphism solutions which support ambiguity. My original complaint about this proposal was that the ordering it uses to decide ambiguity is itself explicitly based on whether types are abstract or not, making its interaction with abstraction even harder to reason about.

@vicuna
Copy link
Author

vicuna commented Apr 1, 2015

Comment author: @alainfrisch

(iv) If P1 and Pn are well-typed programs, and Pn is obtained from P1 by revealing the definition of N types simultaneously, then P1 and Pn have the same semantics.

But (iv) is again equivalent to (i), to (ii), and to (iii), no? ( (iv) => (ii) with n=2, and (ii) => (iv) by applying (ii) several times )

Without any ad-hoc polymorphism, this means that revealing an abstraction will never break a program

This doesn't hold anymore since GADT, right? Revealing an abstraction can allow the type-checker to learn that two types are incompatible, which can be necessary to type-check other code.

However, the proposal in this issue doesn't just interact with abstraction by supporting ambiguity -- the ordering with which it decides that ambiguity is itself determined by whether types are abstract.

Thanks for clarifying your objection.

@vicuna
Copy link
Author

vicuna commented Apr 1, 2015

Comment author: @lpw25

This doesn't hold anymore since GADT, right? Revealing an abstraction can allow the type-checker to learn that two types are incompatible, which can be necessary to type-check other code.

That is an interesting point. I think this can only produce new exhaustivity warnings, but I might be wrong. Any errors it reveals are almost certainly bugs, or at least unnecessary code, so it is useful that they are reported to the user. However, I think you're right that they are probably breaking the guarantee I mentioned above.

@vicuna
Copy link
Author

vicuna commented Apr 1, 2015

Comment author: @alainfrisch

the ordering with which it decides that ambiguity is itself determined by whether types are abstract.

I'm not actually suggesting the following, but do you confirm it would address (some of) your concerns:

  • As already said, let's not reuse the existing "." construction, but let's rather introduce a new construction, say "expr..f" for now.

  • Let's also introduce a new kind of types (in addition to "abstract", "sum", "record", "open"):

    type t = object

  • Such a type is intended to be used in signatures, and it matches an arbitrary type (as for an abstract type).

  • Contrary to abstract types, such a type is not allowed to come with a manifest ("type t = tyexpr = object" is not allowed).

  • "expr..f" is well-typed only if the "fully expanded type" inferred for "expr" is such an "object" type. (We use the same notion of inferred type as for resolving record fields.)

@vicuna
Copy link
Author

vicuna commented Apr 1, 2015

Comment author: @lpw25

I'm not actually suggesting the following, but do you confirm it would address (some of) your concerns:

I do not believe that your object type can be made to work with OCaml's module system. The module system relies in many places on being able to add manifests to all types, this breaks that property.

  • How does include work with them?

  • How does functor application work with them?

  • How do applicative functors work with them?

  • How do module aliases work with them?

  • Does

    module M = (N : sig type t = object end)

    work?

  • What about

    module M = (N : module type of N)

    when N contains an "object" definition.

@vicuna
Copy link
Author

vicuna commented Apr 1, 2015

Comment author: @lpw25

I'm not actually suggesting the following, but do you confirm it would address (some of) your concerns:

As a side-note, this is what I thought you were suggesting much earlier in the discussion when I said:

The only "well-defined" approach to this is to have linear type system for type definitions. Considering how OCaml's module system is path-based, it is hard to see how this would work in OCaml.

@vicuna
Copy link
Author

vicuna commented Apr 1, 2015

Comment author: @lpw25

I do not believe that your object type can be made to work with OCaml's module system.

To be fair, this is not just related to OCaml's module system. The very idea of "newtype" -- which is what you are suggesting -- is really anti-modular, and any feature which relies on it (e.g. typeclasses and higher-kinded types in Haskell) basically cannot be used with functors.

This is one of the fundamental reasons that Haskell does not have functors. Similarly it is one of the reasons why the attempts to add some modularity to Haskell through the Backpack project are proving very difficult.

@vicuna
Copy link
Author

vicuna commented Apr 1, 2015

Comment author: @lpw25

The very idea of "newtype" -- which is what you are suggesting

Actually, perhaps your suggestion is slightly different. Is

module S : sig type t = object end = struct type t = int end

allowed or disallowed by your proposal?

@vicuna
Copy link
Author

vicuna commented Apr 1, 2015

Comment author: @alainfrisch

module S : sig type t = object end = struct type t = int end

It would be allowed.

The module system relies in many places on being able to add manifests to all types, this breaks that property.

All operations that would need to do that would fail (I did not think about all implications). It is precisely the idea: make this feature incompatible with all "advanced" module-level features to avoid bad interaction with them. What's probably bad is that you could get a program to type-check by turning an "object" type into an abstract one (on which a manifest can be added), but this is the same property that is already broken by GADTs (at least if we consider non-exhaustive pattern matches as errors).

basically cannot be used with functors.

I don't see immediately why all uses all functors would be disallowed. Can you explain?

@vicuna
Copy link
Author

vicuna commented Apr 1, 2015

Comment author: @lpw25

module S : sig type t = object end = struct type t = int end

It would be allowed.

In this case, I don't think it addresses the problem, because:

sig type a = object type b = a end

would still be equivalent to:

sig type b = object type a = b end

I don't see immediately why all uses all functors would be disallowed. Can you explain?

Sorry, this was for if your proposal didn't allow objects to represent existing types (i.e. if it was equivalent to newtype).

@vicuna
Copy link
Author

vicuna commented Apr 1, 2015

Comment author: @alainfrisch

sig type a = object type b = a end
would still be equivalent to:
sig type b = object type a = b end

Is it really the case? I thought that signature comparison required to add type equalities.

@vicuna
Copy link
Author

vicuna commented Apr 1, 2015

Comment author: @lpw25

Is it really the case?

I think so. Going from the first signature to the second signature:

  • type b = object is allowed since any type can be made into an "object".

  • type a = b is allowed because b is equal to a in the first signature.

The other direction is symmetric.

This is very similar to:

module F (X : sig type a type b = a end) : sig type b type a = b end = X;;

except with = object instead of abstract types, and that does indeed type-check.

@vicuna
Copy link
Author

vicuna commented Apr 2, 2015

Comment author: @alainfrisch

  • type b = object is allowed since any type can be made into an "object".

Well, no, the types than can be made into an "object" are those which don't have a manifest (and in the first signature, you have "type b = a").

(A slightly different definition would be, instead of introducing a new kind of types, to consider three possible cases for the "manifest" of a type: None and Some as currently, and a third "object" case. This would allow to specify this marker while still exposing the concrete definition of a sum/record type.)

@vicuna
Copy link
Author

vicuna commented Apr 2, 2015

Comment author: @lpw25

  • type b = object is allowed since any type can be made into an "object".

Well, no, the types than can be made into an "object" are those which don't have a manifest (and in the first signature, you have "type b = a").

This still doesn't fix the issue, because you can still go:

sig type a = object type b = a end

to

sig type a type b = a end

to

sig type b type a = b end

to

sig type b = object type a = b end

@vicuna
Copy link
Author

vicuna commented Apr 2, 2015

Comment author: @alainfrisch

Yes, you're right, this make the equivalence non-transitive, which is quite bad. I'm wondering about the idea of considering "object" to be in "manifest" position, and ensuring such a type in a signature can only match a type with already this manifest. I assume this would be very similar to "newtype".

@vicuna
Copy link
Author

vicuna commented Apr 2, 2015

Comment author: @lpw25

I assume this would be very similar to "newtype".

Yes

@vicuna
Copy link
Author

vicuna commented Apr 3, 2015

Comment author: @yallop

Without any ad-hoc polymorphism, this means that revealing an abstraction will never break a program

This doesn't hold anymore since GADT, right?

Right. For example, the following code compiles as written, but it's rejected if X's signature is removed.

type (_, _) eql = Refl : ('a, 'a) eql

module X : sig type s and t end =
struct type s = S and t = T end

let f : (X.s, X.t) eql -> unit = fun Refl -> ()

@github-actions
Copy link

This issue has been open one year with no activity. Consequently, it is being marked with the "stale" label. What this means is that the issue will be automatically closed in 30 days unless more comments are added or the "stale" label is removed. Comments that provide new information on the issue are especially welcome: is it still reproducible? did it appear in other contexts? how critical is it? etc.

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

1 participant