bizarre type

bizarre type

[Julien Verlaguet]

I would like to know if the following behavior is normal :

type 'a t=string ;;

# let g (x : 'a t) (y : 'a)=();;
val g : 'a t -> 'a -> unit = <fun>

# g ("hello" : int t);;
- : '_a -> unit = <fun>

I was expecting: (int -> unit).

J

Re: [Caml-list] bizarre type

[Andreas Rossberg]

Julien Verlaguet wrote:
> I would like to know if the following behavior is normal :
> 
> type 'a t=string ;;
> 
> # let g (x : 'a t) (y : 'a)=();;
> val g : 'a t -> 'a -> unit = <fun>
> 
> # g ("hello" : int t);;
> - : '_a -> unit = <fun>
> 
> I was expecting: (int -> unit).

Since

   int t = string = '_a t

or more generally,

   x t = y t

for any x and y, your type annotation does not induce anything about the 
instantiation of g's variable 'a. The following is perfectly legal:

   g ("hello" : int t) true

The compiler just infers the most general type.

Cheers,

   - Andreas

-- 
Andreas Rossberg, rossberg@ps.uni-sb.de

Let's get rid of those possible thingies!  -- TB

Re: [Caml-list] bizarre type

[Julien Verlaguet]

> The compiler just infers the most general type.

Ok.

But if I write :

# type 'a t;;
type 'a t

# let g (x : 'a t list) (y : 'a)=();;
val g : 'a t list -> 'a -> unit = <fun>

# g ([] : int t list);;
- : int -> unit = <fun>

If I understood well what you just said the inferred type should be :

'_a -> unit

Or is there something I missed there ?

J

Re: [Caml-list] bizarre type

[Stephane Glondu]

On Thursday 30 June 2005 09:58, Julien Verlaguet wrote:
> # g ([] : int t list);;
> - : int -> unit = <fun>

I still get '_a -> unit here (I'm using v3.08.3)... However, I also believe 
that in both cases, it should be int -> unit.

Stephane Glondu.

Re: [Caml-list] bizarre type

[Andreas Rossberg]

Julien Verlaguet wrote:
> 
> But if I write :
> 
> # type 'a t;;
> type 'a t
> 
> # let g (x : 'a t list) (y : 'a)=();;
> val g : 'a t list -> 'a -> unit = <fun>
> 
> # g ([] : int t list);;
> - : int -> unit = <fun>
> 
> If I understood well what you just said the inferred type should be :
> 
> '_a -> unit

In this case, t is fully abstract. So int t is only equivalent to 
itself, and not to arbitrary x t.

-- 
Andreas Rossberg, rossberg@ps.uni-sb.de

Let's get rid of those possible thingies!  -- TB

Re: [Caml-list] bizarre type

[Julien Verlaguet]

> for any x and y, your type annotation does not induce anything about the 
> instantiation of g's variable 'a. The following is perfectly legal:
>
>  g ("hello" : int t) true
>
> The compiler just infers the most general type.

two things :

first

# type 'a t=string;;
type 'a t = string
# let g (x : 'a) (y : 'a t)=();;
val g : 'a -> 'a t -> unit = <fun>
# g 3;;
- : int t -> unit = <fun>

here we should have int t=string='_a t ...

second :

I strongly disaggree with the fact that the compiler infered the most 
general type in this case.

Because I specified it.

when you write (let f=fun (x : 'a) (y : 'a) -> (x,y)), you force the type 
of x 
and y to be equal.
It would be a problem if one could write (f true 3).

J

PS : The behavior with abstract types is the one expected and my example 
in the previous mail was irrelevant (sorry about that).

Re: [Caml-list] bizarre type

[Andreas Rossberg]

From: "Julien Verlaguet" <Julien.Verlaguet@pps.jussieu.fr>
>
> # type 'a t=string;;
> type 'a t = string
> # let g (x : 'a) (y : 'a t)=();;
> val g : 'a -> 'a t -> unit = <fun>
> # g 3;;
> - : int t -> unit = <fun>
>
> here we should have int t=string='_a t ...

Well, since '_a t = int t the compiler can freely choose either for
printing. Or bool t, for that matter.

> I strongly disaggree with the fact that the compiler infered the most
> general type in this case.
>
> Because I specified it.
>
> when you write (let f=fun (x : 'a) (y : 'a) -> (x,y)), you force the type
> of x
> and y to be equal.

Yes, but that's not what you did in the other example. You wrote (x : 'a
t) - and because of the way t was defined this was as good as writing (x :
string) and hence did not induce any additional constraint.

Cheers,

  - Andreas

Re: [Caml-list] bizarre type

[Julien Verlaguet]

> Well, since '_a t = int t the compiler can freely choose either for
> printing. Or bool t, for that matter.

agreed.

> Yes, but that's not what you did in the other example. You wrote (x : 'a
> t) - and because of the way t was defined this was as good as writing (x :
> string) and hence did not induce any additional constraint.

Ok, I have to aggree.

In fact it prevents me from writting this :

type 'a marshalled=string

let make (x : 'a)=(Marshal.to_string x [] : 'a marshalled);;

And then do all type of operations in a type safe way on strings.

I have to aggree though that I wrote 'a t=string and therefore one should
be able to exchange them.

The only tiny thing that disturbs me is that in my previous example :

let g (x : 'a t) (y : 'a)

the type of y depends on the 'a present in 'a t.
It is odd. But I have to admit it's correct.

Thanks for your help.

J

Re: [Caml-list] bizarre type

[Jacques Garrigue]

From: Julien Verlaguet <Julien.Verlaguet@pps.jussieu.fr>
> 
> > Well, since '_a t = int t the compiler can freely choose either for
> > printing. Or bool t, for that matter.
> 
> agreed.

Nice to see that everybody agrees that the current behaviour is
reasonable :-)
And thanks to Andreas for explaining things so well.

Yet, these useless parameters are a rather weak part of the compiler,
so there may be some bugs left there. I.e. it is hard to guarantee
that "a t" will alway be equivalent to "b t" for any use, while they
should be so in the intended semantics. Bugs report are welcome.

In general, I would suggest avoiding non-abstract phantom types, as
they are useless... except when you're going to abstract them at the
next module boundary.

> In fact it prevents me from writting this :
> 
> type 'a marshalled=string
> 
> let make (x : 'a)=(Marshal.to_string x [] : 'a marshalled);;
> 
> And then do all type of operations in a type safe way on strings.

What you want seems to be the Graal: a type that is more than a
string, but can be implicitly coerced to one. Of course the opposite
direction would not be allowed.
A standard way to do that is to make [marshalled] abstract, and provide
a function [to_string] when you need to recover the string.
In ocaml 3.09, you will have another possibility: using a private type
for that, with the extra advantage of having pattern-matching (this
doesn't work with private types in 3.08, as they are not handled as
abstract.)
But not yet the Graal, which requires to combine implicit subtyping
with type inference in a non-trivial way...

> The only tiny thing that disturbs me is that in my previous example :
> 
> let g (x : 'a t) (y : 'a)
> 
> the type of y depends on the 'a present in 'a t.
> It is odd. But I have to admit it's correct.

The point here is that ['a t] is not the type of [x] itself, but a
type that can be unified with it. And useless parameters are discarded
during unification. At a more theoretical level, ['a t] is only
required to be equivalent to the type of [x], not identical.

Jacques Garrigue

Re: [Caml-list] bizarre type

[Damien Doligez]

On Jun 30, 2005, at 23:42, Julien Verlaguet wrote:

> In fact it prevents me from writting this :
>
> type 'a marshalled=string
>
> let make (x : 'a)=(Marshal.to_string x [] : 'a marshalled);;
>
> And then do all type of operations in a type safe way on strings.

If I understand correctly, this is your problem:

         Objective Caml version 3.08.3+4 (2005-06-21)

# type 'a marshalled=string;;
type 'a marshalled = string
# let make (x : 'a)=(Marshal.to_string x [] : 'a marshalled);;
val make : 'a -> 'a marshalled = <fun>
# make 1 = make "foo";; (* int marshalled is the same as string 
marshalled *)
- : bool = false

It works better you use a concrete type instead of an abbreviation:

# type 'a marsh2 = Marsh of string;;
type 'a marsh2 = Marsh of string
# let make2 (x : 'a) = (Marsh (Marshal.to_string x []) : 'a marsh2);;
val make2 : 'a -> 'a marsh2 = <fun>
# make2 1 = make2 "foo";; (* int marsh2 is not the same as string 
marsh2 *)
             ^^^^^^^^^^^
This expression has type string marsh2 but is here used with type int 
marsh2
#

-- Damien

Re: [Caml-list] bizarre type

[Jacques Garrigue]

From: Damien Doligez <damien.doligez@inria.fr>

> If I understand correctly, this is your problem:
> 
>          Objective Caml version 3.08.3+4 (2005-06-21)
> 
> # type 'a marshalled=string;;
> type 'a marshalled = string
> # let make (x : 'a)=(Marshal.to_string x [] : 'a marshalled);;
> val make : 'a -> 'a marshalled = <fun>
> # make 1 = make "foo";; (* int marshalled is the same as string 
> marshalled *)
> - : bool = false
> 
> It works better you use a concrete type instead of an abbreviation:
> 
> # type 'a marsh2 = Marsh of string;;
> type 'a marsh2 = Marsh of string
> # let make2 (x : 'a) = (Marsh (Marshal.to_string x []) : 'a marsh2);;
> val make2 : 'a -> 'a marsh2 = <fun>
> # make2 1 = make2 "foo";; (* int marsh2 is not the same as string 
> marsh2 *)
>              ^^^^^^^^^^^
> This expression has type string marsh2 but is here used with type int 
> marsh2

Actually this is not a very good suggestion from the point of view of
safety, as this useless parameter can still be modified by subtyping:

# make2 1 = (make2 "foo" :> _ marsh2);;
- : bool = false

If you care about safety, you must either use an abstract type, or a
private type in ocaml-3.09 (not 3.08!).

On the other, if you want to keep the possibility of overriding the
parameter, while detecting non-annotated cases, this may actually be a
good approach.

Jacques Garrigue