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
Comments
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). |
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. |
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. |
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 to: let elt = doc.getElementById "canvas" in |
Comment author: @trefis
I couldn't agree more
Except it's not equivalent. If invert had type "t -> M2.t" then name would have been fetched in M2 ("hopefully"). |
Comment author: @trefis
Didn't you mean:
? On a similar subject:
Should "similary" here be understood as "just as random and ad-hoc but happens to match perfectly well the example I have in mind"? 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. |
Comment author: @dbuenzli
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. |
Comment author: @lpw25
Consider:
The examples get worse when you start using functors. This is also the reason why we don't support higher-kinded It is also worth noting that this proposal only gives
A better approach (if an object-style syntax is really desired)
which was just short-hand for
|
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) = would translate into let x = |
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. 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. |
Comment author: @alainfrisch Re 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? |
Comment author: @alainfrisch Re trefis:
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 |
Comment author: @lpw25
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:
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. |
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. |
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. |
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. |
Comment author: @alainfrisch
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. |
Comment author: @lpw25
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.
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. |
Comment author: @alainfrisch
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 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. |
Comment author: @lpw25
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.
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. |
Comment author: @alainfrisch
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.
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. |
Comment author: @lpw25
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. |
Comment author: @alainfrisch
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:
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. |
Comment author: @lpw25
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. |
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 module M1_concrete Then which combinations of these modules can be declared as implicit together in order to allow "show X.x"? |
Comment author: @lpw25
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. |
Comment author: @alainfrisch
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)):
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. |
Comment author: @lpw25
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.
You've answered your own question there. 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
differently from
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. |
Comment author: @alainfrisch
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 )
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.
Thanks for clarifying your objection. |
Comment author: @lpw25
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. |
Comment author: @alainfrisch
I'm not actually suggesting the following, but do you confirm it would address (some of) your concerns:
|
Comment author: @lpw25
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.
|
Comment author: @lpw25
As a side-note, this is what I thought you were suggesting much earlier in the discussion when I said:
|
Comment author: @lpw25
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. |
Comment author: @lpw25
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? |
Comment author: @alainfrisch
It would be allowed.
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).
I don't see immediately why all uses all functors would be disallowed. Can you explain? |
Comment author: @lpw25
In this case, I don't think it addresses the problem, because:
would still be equivalent to:
Sorry, this was for if your proposal didn't allow objects to represent existing types (i.e. if it was equivalent to newtype). |
Comment author: @alainfrisch
Is it really the case? I thought that signature comparison required to add type equalities. |
Comment author: @lpw25
I think so. Going from the first signature to the second signature:
The other direction is symmetric. This is very similar to:
except with |
Comment author: @alainfrisch
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.) |
Comment author: @lpw25
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 |
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". |
Comment author: @lpw25
Yes |
Comment author: @yallop
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 = let f : (X.s, X.t) eql -> unit = fun Refl -> () |
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. |
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
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
The text was updated successfully, but these errors were encountered: