<pdhborges>
milanst says the compyler couldn't equate
<pdhborges>
'a t and readonly t as the same type
<pdhborges>
to satisfy the interface
<thelema>
okay
<pdhborges>
however I created a function with signature 'a -> 'a -> 'a
<pdhborges>
and a polymofic record type
<pdhborges>
and I could use for example
<pdhborges>
and 'a record and an int record with that function
<pdhborges>
no problems
<thelema>
sure
<pdhborges>
but hwo can the compiler equate the types in this case
<pdhborges>
but not on the other case
<thelema>
the problem is not exactly in the type inference in the other case, but in whether a module type matches the inferred type
<thelema>
and a subtlety about phantom types makes it not do this
<pdhborges>
but
<thelema>
in your case, everything is perfectly normal type inference, ('a) unifies with anything
<pdhborges>
yes
<pdhborges>
but it has to unify
<pdhborges>
'a with 'b recor
<pdhborges>
and at the same time
<pdhborges>
'a with int record
<dark>
(so 'b = int)
<thelema>
actually, most likely in your case, it unifies 'a with int record, and then the other 'a forces 'b = int
<thelema>
and then there's no variables left after unification
<thelema>
but in the given example, the inferred type is 'a -> 'a
<thelema>
but the desired signature is 'a t -> readonly t
<thelema>
and there's nothing that (the first) 'a can be set to to unify the two
<pdhborges>
why not set 'a to 'a t?
<dark>
pdhborges, oh i got what you asked. readonly t is more specific than 'a t. if you have a function with a more general type you can apply it with a more specific type, but not vice versa. that's why the types are incompatible
<dark>
so a function that expects 'a t will work with readonly t, but a function that expects readonly t won't work with 'a t
<dark>
and 'a works with everything :)
<thelema>
pdhborges: setting 'a = 'a t fails to unify the right side
<thelema>
if you go one step further and set 'a = readonly t, that fails to unify the left side
<pdhborges>
I think I'm mixing to diferent things in my head hence the confusion
<dark>
pdhborges, ocaml has a type called '_a that is like 'a, but once you use it for some type (like say int) you can't use it for other type
<pdhborges>
I know
<pdhborges>
it's a monomorphic type
<dark>
yes, i thought you were thinking of 'a as being like '_a :)
<pdhborges>
no thats no it
<pdhborges>
not*
<pdhborges>
thelema so in the first case the problem is signature mathing
<pdhborges>
In my case It's just type inference
<pdhborges>
s/mathing/matching
<dark>
if f : ('a -> 'a -> 'a), let q = f (x : 'a record) (y : int record) works and q has type int record (because it is the most specific type from those 3 that were unified)
<dark>
'a record and int record are compatible but not equal; if you think them as sets, int record is a subset of 'a record
<thelema>
They're related. In this example, the signature matching requires the left hand side to stay polymorphic, while your example works as long as all the 'a can be resolved satisfactorily
<pdhborges>
what does the compiler infer for the readonly function?
<thelema>
yes, k is properly polymorphic, not monomorphic
<thelema>
z?
<pdhborges>
yes
<pdhborges>
type z = { mutable r : int } type 'a t = z
<thelema>
oh yes..
<pdhborges>
initially the compiler infered 'a -> 'a
<thelema>
z -> z
<pdhborges>
a so it's the inference for the signature that changes
<pdhborges>
not the inference for the struct
<pdhborges>
'a -> 'a is more general than z -> z so it won't complain
<thelema>
yes, once it's got z -> z, it can unify each of the z's separately with 'a t and readonly t
<thelema>
z -> z is different from 'a t -> 'a t
<thelema>
even though 'a t = z
<kaustuv>
dark: OCaml does *not* have a type '_a. You can never write it in signatures, for instance. It is a feature of the OCaml implementation only.
<pdhborges>
thelema: so the compilers looks at
<pdhborges>
'a t and figures it's z
<pdhborges>
then at readonly t which is also z
<thelema>
kaustuv: that's a fine line, splitting the OCaml implementation from the lanaguge, considering that since there's only one implementation of the language, many aspects of the language are defined by that implementation
<thelema>
pdhborges: yup
<pdhborges>
the signature becomes z -> z
<pdhborges>
the implementations still
<pdhborges>
'a -> 'a
<thelema>
well, the implementation is untyped - once typechecking is done, types are erased
<pdhborges>
for implementation I mean't the struct
<pdhborges>
s/'//
mnabil has quit [Read error: Operation timed out]
<thelema>
the struct is still 'a -> 'a? the record? the readonly function?
<pdhborges>
the readonyl function
<thelema>
the readonly function is z -> z
<pdhborges>
that's the signature but the type checker must match that signature with the infered signature for the readonly implementation no?
<thelema>
sure, the inferred signature for "readonly t = t" is 'a -> 'a
<pdhborges>
\o/ thanks guys. Today I learned quite a bit about ocaml's subtleties.
<thelema>
n/p
<kaustuv>
Is the issue here that this works:
<kaustuv>
let f : 'a -> 'a = fun x -> x + 1
<kaustuv>
but this doesn't:
<kaustuv>
module M : sig val f : 'a -> 'a end = struct let f x = x + 1 end
oriba_ has joined #ocaml
<kaustuv>
?
<thelema>
kaustuv: kind of.
<thelema>
although more subtle.
<thelema>
type 'a t = {mutable r: int}
<thelema>
module M : sig val ro : 'a t -> readonly t end = struct let readonly t = t end
<thelema>
this doesn't work
<thelema>
but if you define the type 'a t as:
<thelema>
type z = {mutable r: int}
<thelema>
type 'a t = z
<thelema>
then it works
oriba has quit [Ping timeout: 240 seconds]
<pdhborges>
kaustuv let f : 'a. 'a -> 'a = fun x -> x + 1;; ^^
philtor has joined #ocaml
<kaustuv>
Ah, the issue is that the type checker expands abbreviations before unification
<thelema>
maybe. maybe the non-polymorphic type z allows it to break the dependence of 'a t on the left side from 'a t on the right side
mnabil has joined #ocaml
myu2 has joined #ocaml
<kaustuv>
This works though:
<kaustuv>
module M : sig type 'a t type ro val ro : 'a t -> ro t end = struct type 'a t = A type ro let ro x = (x :> ro t) end ;;
<mrvn>
# let f : 'a -> 'a = fun x -> x + 1;;
<mrvn>
val f : int -> int = <fun>
<thelema>
yes, this changes the inferred type from 'a -> 'a to 'a t -> ro t
<mrvn>
The reason why that works is that the signature you give is more a hint of the shape of type f needs to have and the type inference figures out it actually is int -> int which is the right shape.
<mrvn>
On the other hand in a module signature you need exact type equality.
<thelema>
mrvn: yup, 'a -> 'a is able to unify with the inferred type, so everything is okay.
<thelema>
umm, not really - one can restrict types with a module signature
<kaustuv>
the problem seems to be that in order for ('x -> 'x) to unify with ('a t -> 'b t) the type checker will need to prove that 'a t = 'b t, i.e. that the type parameter is a phantom. I guess the type checker doesn't have a phantomness detector
<thelema>
i.e. inferred: 'a -> 'a, spec: int -> int is okay
<mrvn>
true. Ok. In a module the relationship is the other way around. The function gives the looser type.
<thelema>
kaustuv: that matches my mental model of what's going on more than the order of unification and type abbreviation expansion
tauntaun has joined #ocaml
joewilliams_away is now known as joewilliams
<mrvn>
That 'type z = {mutable r: int} type 'a t = z' makes a difference doesn't really make sense but it has some reason somewhere in the implementation.
<thelema>
mrvn: doens't kaustuv's last message clarify it?
<kaustuv>
I am guessing the reason the type checker doesn't detect phantomness is that that would drastically reduce their usefulness. It would suck if the typechecker didn't complain when I tried to coerce a readonly t to a writable t.
<thelema>
kaustuv: ah, yes.
<mrvn>
not really. ['a] {mutable r: int} == ['b] {mutable r: int}. But it only sees that with the intermittant z type.
<mrvn>
kaustuv: it only complain when the phantom type is abstract/private
<thelema>
because it doesn't know about (or care about) the definition for the type at this point
<thelema>
mrvn: it only sees 'a -> 'a and 'a t -> readonly t and can't unify the two
oriba_ has left #ocaml []
oriba has joined #ocaml
<thelema>
the type checker doesn't substitute all the way down to basic types and then unify
<mrvn>
good thing too
<Lor>
What's the current recommended approach to naming modules in a library?
<Lor>
Just add a package prefix to all the top-level module names?
<thelema>
Lor: packing them into a top-level module is recommended as long as you don't have any problems with executable size
<Lor>
Or use -pack and try to avoid module names that conflict with existing ones?
<thelema>
batteries doesn't follow this good advice because of executable size issues
<Lor>
Ah, the entire top-level module is always linked in?
agarwal1975 has quit [Read error: Connection reset by peer]
<thelema>
yes, that's the semantics for modules
agarwal1975 has joined #ocaml
<Lor>
The problem with -pack is that it's very fragile since the modules being defined must not conflict with top-level modules.
<Lor>
thelema, that's implementation, not semantics.
<Lor>
If a submodule is never ever used, the semantics don't change even if it's removed.
<thelema>
almost - the semantics of program execution are that each phrase in each module is executed in link order
<thelema>
modules can have side effects just from being linked in
<thelema>
and the ocaml compiler doesn't test for this, so can't eliminate anything
<Lor>
True enough.
<kaustuv>
In fact it is impossible to test for it because of the halting problem
<Lor>
Still an implementation issue, but a more complicated one.
<Lor>
rice's theorem, you mean. Yes, but there are always conservative approximations.
<thelema>
kaustuv: there's some pretty good approximations - function declarations are guaranteed to have no side effects
<mrvn>
thelema: let f = incr foo; functiion () -> ()
<thelema>
that's not what I meant
<thelema>
that isn't a function according to the ocaml compiler, otherwise it would be polymorphic instead of monomorphic
<thelema>
(ignoring that it's unit -> unit)
<mrvn>
and wasn't there a bug that the compiler eliminates modules with side effects when none of it is used?
agarwal1975 has quit [Read error: Connection reset by peer]
agarwal1975 has joined #ocaml
<mrvn>
# let f = incr foo; function () -> ();;
<mrvn>
val f : unit -> unit = <fun>
<mrvn>
How is that not a function?
<mrvn>
# let f = incr foo; function x -> x;;
<mrvn>
val f : 'a -> 'a = <fun>
<mrvn>
works polymorphic too
<thelema>
hmmm...
<mrvn>
More common is probably let f = let x = ref something in function ....
<thelema>
# let f = let r = ref 0 in function x -> x;;
<thelema>
# Warning Y: unused variable r.
<thelema>
val f : '_a -> '_a = <fun>
<thelema>
yes, once mutables come into play...
<Lor>
All right, so I should use -pack and just hope that ocaml gets real namespaces one day?
<thelema>
n/m then, my mistake
<thelema>
Lor: yes, that's the best we've got.
<mrvn>
thelema: yes. if you create a ref you loose the polymorphism.
<kaustuv>
OCaml has real namespaces. What you want is dead code elimination.
<Lor>
I'm still not sure it's a good idea.
<Lor>
Then in code it becomes difficult to see where exactly a top-level module is.
<f[x]>
Lor, complain on that ticket!
<Lor>
kaustuv, did you read the above bug report?
<f[x]>
kaustuv, nope
<pdhborges>
mrvn you example is correct
<pdhborges>
incr increments the ref
<Lor>
It's much clearer to open PackagePrelude than Prelude in the source code of the package, even if Prelude would eventually get packed into Package.Prelude.
<pdhborges>
but the value of the expression is function () -> ()
<pdhborges>
which is then bound to f
<thelema>
mrvn: in any case, those kinds of "functions" can be syntactically eliminated
<kaustuv>
By real namespaces I mean -for-pack
<kaustuv>
which doesn't have name collisions
<mrvn>
thelema: they are possible so the compiler has to consider them
<Lor>
Right, the different module structures for native and bytecode compilation results even in observable runtime differences.
<kaustuv>
take the bytecode compiler behind the shed and put a bullet between its eyes already
<thelema>
mrvn: yes, they can't be easily eliminated by dead code elim, and have to be treated as possible "actually-evaluating" functions
* thelema
would be kinda happy to deprecate the bytecode compiler
<kaustuv>
(unless you use some crazy platform that doesn't have a native backend)
* pdhborges
would be kind of happy to support dynamic linking in native code
<kaustuv>
You have issues with Dynlink in native code?