signature and 'a generic types

signature and 'a generic types

[Damien Bobillot]

[-- Attachment #1: Type: text/plain, Size: 983 bytes --]

Hello,

Look at the following code :

     module Module : (sig val func : 'a -> 'b end) =
     struct let func a = a end

Here Module.func's type is 'a -> 'a. According to me 'a -> 'a is a  
subtype of 'a -> 'b, it's 'a -> 'b with 'a = 'b. Nevertheless ocamlc  
give the following error :

     Values do not match:
       val func : 'a -> 'a
     is not included in
       val func : 'a -> 'b

Why ?

I also try to use the reverse match :

     module Module : (sig val func : 'a -> 'a end) = struct
         let l = ref []
         let func a = List.assoc a !l
     end

Where Module.func is of type 'a -> 'b. Ocamlc also give me an error,  
but I completely understand it here : 'a -> 'b is really not a  
subtype of 'a -> 'a.

In this case I also don't understand why neither " 'a -> 'b is  
included in 'a -> 'a " nor " 'a -> 'a is included in 'a -> 'b " are  
true. To my mind, one should be true.

Is it a caml limitation/bug, or am I wrong somewhere ?

-- 
Damien Bobillot


[-- Attachment #2: smime.p7s --]
[-- Type: application/pkcs7-signature, Size: 2375 bytes --]

Re: [Caml-list] signature and 'a generic types

[Virgile Prevosto]

Hi,
Le 06/20/2005, à 05:20:40 PM, Damien Bobillot a écrit:
> Look at the following code :
> 
>      module Module : (sig val func : 'a -> 'b end) =
>      struct let func a = a end

>      Values do not match:
>        val func : 'a -> 'a
>      is not included in
>        val func : 'a -> 'b
> 
> Why ?

because the implementation of func is less general than what the
signature expects: if this was accepted, then you could use Module.func
in a context where 'a and 'b would get different instantiations.

> 
> I also try to use the reverse match :
> 
>      module Module : (sig val func : 'a -> 'a end) = struct
>          let l = ref []
>          let func a = List.assoc a !l
>      end

This is not the "reverse" match, which would rather be
module Module: (sig val func: 'a -> 'a end) = 
struct
  let l = [] 
  let func a = List.assoc a l
end;;

which is a perfectly well defined module. In your case, problems come
from the ref: the type of l (hence of func) is not really polymorphic:
it uses what is called weak type variables (that you recognize because
of the '_' prefix in '_a and '_b), that on the contrary to normal
type variables can not be generalized. Otherwise, it would be possible
to add to l pairs of different types, such as in the following example:
module Module = 
struct
  let l = ref [] (* type: ('_a * '_b) list *)
  let func a = List.assoc a !l
  let _ = l:= (0, "foo")::!l 
   (* after that '_a is bound to int and '_b to string. *)
  let _ = l:= ("bar", 1)::!l (* type error. *)
end
-- 
E tutto per oggi, a la prossima volta
Virgile

Re: [Caml-list] signature and 'a generic types

[Stephane Glondu]

On Monday 20 June 2005 08:20, Damien Bobillot wrote:
> Hello,
>
> Look at the following code :
>
>      module Module : (sig val func : 'a -> 'b end) =
>      struct let func a = a end
>
> Here Module.func's type is 'a -> 'a. According to me 'a -> 'a is a
> subtype of 'a -> 'b, it's 'a -> 'b with 'a = 'b.

It is not relevant. To write this, every 'a -> 'a object must be seeable as a 
'a -> 'b object, which is obviously wrong (otherwise, e.g. func 0 would have 
any type).

> I also try to use the reverse match :
>
>      module Module : (sig val func : 'a -> 'a end) = struct
>          let l = ref []
>          let func a = List.assoc a !l
>      end
>
> Where Module.func is of type 'a -> 'b. Ocamlc also give me an error,
> but I completely understand it here : 'a -> 'b is really not a
> subtype of 'a -> 'a.

Again, the explanation is not relevant. Here, func is not of type 'a -> 'b, 
but '_a -> '_b instead, that means that the first usage of func will freeze 
the type (you won't be able to use func 4, then func true). It happens every 
time you use references. Otherwise, you could write e.g. l := [(1,1)]; func 
true.

> In this case I also don't understand why neither " 'a -> 'b is
> included in 'a -> 'a " nor " 'a -> 'a is included in 'a -> 'b " are
> true. To my mind, one should be true.

'a -> 'b is included in 'a -> 'a, but not the contrary (intuitively, functions 
of the first type don't terminate properly, e.g. let f a = raise Exit).


Stephane Glondu.

Re: [Caml-list] signature and 'a generic types

[Marcin 'Qrczak' Kowalczyk]

Damien Bobillot <damien.bobillot@m4x.org> writes:

>      module Module : (sig val func : 'a -> 'b end) =
>      struct let func a = a end
>
> Here Module.func's type is 'a -> 'a. According to me 'a -> 'a is a
> subtype of 'a -> 'b, it's 'a -> 'b with 'a = 'b.

It's not a subtype because 'a -> 'b really means
   forall 'a 'b. 'a -> 'b
and not
   exists 'a 'b. 'a -> 'b

If identity function had type forall 'a 'b. 'a -> 'b, I could use it
to transform an integer to a string.

>      module Module : (sig val func : 'a -> 'a end) = struct
>          let l = ref []
>          let func a = List.assoc a !l

Here the type of func is
   '_a -> '_b
which means something like
   exists 'a 'b. 'a -> 'b
For details Google for "value polymorphism" or "imperative polymorphism".
(Why this is not explained in OCaml manual?)

This is not a subtype of forall 'a. 'a -> 'a.

-- 
   __("<         Marcin Kowalczyk
   \__/       qrczak@knm.org.pl
    ^^     http://qrnik.knm.org.pl/~qrczak/

Re: [Caml-list] signature and 'a generic types

[Michael Alexander Hamburg]

Quoting Damien Bobillot <damien.bobillot@m4x.org>:

> Hello,
>
> Look at the following code :
>
>      module Module : (sig val func : 'a -> 'b end) =
>      struct let func a = a end
>
> Here Module.func's type is 'a -> 'a. According to me 'a -> 'a is a
> subtype of 'a -> 'b, it's 'a -> 'b with 'a = 'b. Nevertheless ocamlc
> give the following error :
>
>      Values do not match:
>        val func : 'a -> 'a
>      is not included in
>        val func : 'a -> 'b
>
> Why ?
>

The module signature requires that the function have type 'a -> 'b for all 'a
and 'b, i.e. the declared type must be a subtype of the actual type, not vice
versa.  Imagine if the compiler let you use that module definition, someone
calling the module would be able to say "hello" ^ Module.func 1, and OCaml
would try to treat 1 as a string because func is declared to have type 'a ->
'b.

> I also try to use the reverse match :
>
>      module Module : (sig val func : 'a -> 'a end) = struct
>          let l = ref []
>          let func a = List.assoc a !l
>      end
>
> Where Module.func is of type 'a -> 'b. Ocamlc also give me an error,
> but I completely understand it here : 'a -> 'b is really not a
> subtype of 'a -> 'a.

Ah, but the function you declared is not of type 'a -> 'b but rather of type '_a
-> '_b, because ref [] does not refer to _every_type_ ('a ref), but rather
_one_single_type_ ('_a ref).  This is the infamous "value polymorphism
restriction".  Here's why it's there:

let l = ref [] (* type of l is '_a list ref, not 'a list ref *)
let () = l := ["hello"] (* if there were no VPR, l would still have type 'a list
ref here, but because it has one single type, it is now a string list ref *)
let x = 1+List.head !l (* if there were no VPR, this would be allowed, and try
to compute 1+"hello" *)
let () = l := [7] (* this is also disallowed by the type of l.  You can't get it
back to being an '_a list ref *)

In any case, 'a -> 'a is not a subtype of '_a -> '_b.  If your func had been
Obj.magic, or a -> List.assoc a [], or a -> failwith "Hello world", it would
have worked (I think, I don't have OCaml in front of me).

> In this case I also don't understand why neither " 'a -> 'b is
> included in 'a -> 'a " nor " 'a -> 'a is included in 'a -> 'b " are
> true. To my mind, one should be true.
>
> Is it a caml limitation/bug, or am I wrong somewhere ?

Sort of.  First, the VPR is somewhat more restrictive than it has to be for type
safety, but analyzing exactly how restrictive is has to be in a particular case
is hard (very hard in this case; it's hard for the compiler to know that a
particular piece of mutable state will never be mutated anywhere), and would
require extra notation to avoid breaking across module boundaries.  The current
restriction is sort of a happy medium.

Second, in OCaml, polymorphic types are abbreviated.  "'a -> 'a" is an
abbreviation of "for all types 'a, 'a -> 'a", whereas "'_a -> '_a" is an
abbrevation of "for one single arbitrary type 'a, 'a -> 'a".  These
abbreviations are somewhat confusing.  They also assume knowledge of a
restriction of so-called Hindley-Milner types, which is that all the "forall"s
go out in front.  This restriction is required for automatic type detection to
be computable, so it can be lifted only if the user specifies the type.  For
some reason, in OCaml the syntax only allows you to do this in record
declarations, which could probably be considered a "limitation/bug".

Mike Hamburg

> --
> Damien Bobillot
>
>