Quantifier in the type

Quantifier in the type

[Dawid Toton]

Just an elementary question.

I put 'a in the interface:
val fu : 'a -> 'a
and int in the implementation:
let fu x = x + 1

So I have universal quantification: for any type 'a function fu can 
consume the argument. So my implementation doesn't comply with that 
universal quatification. And the message I get is following:

Values do not match: val fu : int -> int is not included in val fu : 'a 
-> 'a

So the declaration of value in mli file is called simply a 'value'. Is 
it intentional?
I thought that value and it's declaration are separate notions?

My reading of " val fu : 'a -> 'a " is:
 some partiular value vvv that belongs to set of values that satisfy  
"forall 'a : (vvv can be used with ('a -> 'a) type)"

But if I write
let (bar : 'a -> 'a ) = (fun x -> x + 1)
I create a value that belongs to set "exists 'a : (vvv can be used with 
('a -> 'a) type)"
So it's the other quantifier.

I think that the quantifier has to be part of type, since a type is set 
of values (and the quantifier plays important role when describing some 
of such sets).
So my question is: since we see the same string " 'a -> 'a " that refers 
to different types in different contexts, what are the rules? How is 
type definition in OCaml translated to a type?

Dawid

Re: [Caml-list] Quantifier in the type

[Florent Monnier]

> I put 'a in the interface:
> val fu : 'a -> 'a
> and int in the implementation:
> let fu x = x + 1

this interface doesn't reflect the implementation, ocaml will reject it in any 
way

> So I have universal quantification: for any type 'a function fu can
> consume the argument.

No it is not universal, imagine all the types that a user can create, you 
cannot handle them all (except maybe with the Obj module, but it's another 
question)

Anyway if you handle different types, you still have to join them in a single 
type :

type generic =
  | Int of int
  | Float of float
  | Int64 of int64
  ... and so on

>                       So my implementation doesn't comply with that
> universal quatification. And the message I get is following:
>
> Values do not match: val fu : int -> int is not included in val fu : 'a
> -> 'a

Yes it doesn't match at all, the type of the implementation is int, nothing 
else.

> So the declaration of value in mli file is called simply a 'value'. Is
> it intentional?

It is just the word in the English language to designate this thing.

> I thought that value and it's declaration are separate notions?

a value is handle by a identifier and has a type
  let ident = some_value in
here ident and some_value are of some type

> My reading of " val fu : 'a -> 'a " is:
>  some partiular value vvv that belongs to set of values that satisfy
> "forall 'a : (vvv can be used with ('a -> 'a) type)"

here are some examples of functions with type ('a -> 'a) :

let id v = (v)
let return_sleep v = Unix.sleep 3; (v)
let feedback_kind v =
  let r = Obj.repr v in
  if Obj.is_int r then print_endline "value similar to int";
  (v)
;;

# let (duplicate : 'a -> 'a) = function v ->
    Obj.obj(Obj.dup(Obj.repr v)) ;;
val duplicate : 'a -> 'a = <fun>
# let str = "AAA" ;;
val str : string = "AAA"
# let str2 = duplicate str ;;
val str2 : string = "AAA"
# str.[0] <- 'B' ;;
- : unit = ()
# str, str2 ;;
- : string * string = ("BAA", "AAA")

________________________________


# let reminder = ref [] ;;
val reminder : '_a list ref = {contents = []}

# let remind_through v =
    if List.exists (fun this -> Obj.magic v = this) !reminder
    then failwith "allready processed" 
    else begin
      reminder := Obj.magic v :: !reminder;
      (v)
    end 
  ;;              
val remind_through : 'a -> 'a = <fun>

# let a, b, c, d =
  "Hello",
  4096,
  4.0 *. atan 1.0,
  None;;
val a : string = "Hello"
val b : int = 4096
val c : float = 3.14159265358979312
val d : 'a option = None

# remind_through a ;;
- : string = "Hello"
# remind_through b ;;
- : int = 4096
# remind_through c ;;
- : float = 3.14159265358979312
# remind_through d ;;
- : 'a option = None

# remind_through a ;;
Exception: Failure "allready processed".



> But if I write
> let (bar : 'a -> 'a ) = (fun x -> x + 1)
> I create a value that belongs to set "exists 'a : (vvv can be used with
> ('a -> 'a) type)"
> So it's the other quantifier.

int can be used for a function which takes 'a, but this opposite is not true:
a function that implements with ints can not take 'a parameters.

> I think that the quantifier has to be part of type, since a type is set
> of values (and the quantifier plays important role when describing some
> of such sets).
> So my question is: since we see the same string " 'a -> 'a " that refers
> to different types in different contexts, what are the rules? How is
> type definition in OCaml translated to a type?

type definition in OCaml are translated to actual types by inference.
http://en.wiktionary.org/wiki/inference

(fun x -> x + 1) will be easily infered to (int -> int)

The only way to do a generic function to make addition on generic types as 
float, int, or a number in a string, is like the example below.
But those kind of things are HIGHLY discouraged !
Please consider each Obj.magic as a hammer hit,
you will understand that programming with a hammer is discouraged :-)

# let gen_add v =
    let r = Obj.repr v in
    let tag = Obj.tag r in
    if tag = Obj.int_tag then
      (Obj.magic((Obj.magic v) + 1))
    else if tag = Obj.double_tag then
      (Obj.magic((Obj.magic v) +. 1.0))
    else
    try if tag = Obj.string_tag then
      (Obj.magic(Scanf.sscanf (Obj.magic v) "%f"
                   (fun v -> string_of_float(v +. 1.0))))
    else
      (v)
    with Scanf.Scan_failure _ -> (v) 
  ;;
val gen_add : 'a -> 'a = <fun>

# gen_add 3 ;;
- : int = 4
# gen_add 3.0 ;;
- : float = 4.
# gen_add "3" ;;
- : string = "4."

-- 
Florent

Re: [Caml-list] Quantifier in the type

[Dawid Toton]

Thanks for your answer; now I'll try to sate my point in a clear way,
since you misunderstood all my questions.

>> I put 'a in the interface:
>> val fu : 'a -> 'a
>> and int in the implementation:
>> let fu x = x + 1
> 
> this interface doesn't reflect the implementation, ocaml will reject it in any 
> way

OK, it's all about this rejection, e.g. what does precisely mean 'to
reflect the implementation'.

> 
>> So I have universal quantification: for any type 'a function fu can
>> consume the argument.
> 
> No it is not universal, imagine all the types that a user can create, you 
> cannot handle them all (except maybe with the Obj module, but it's another 
> question)

I wanted this my sentence to be about the declatation in mli interface.
My point is: the type in the declaration in mli implicitly contains
universal quantifier.


>>                       So my implementation doesn't comply with that
>> universal quatification. And the message I get is following:
>>
>> Values do not match: val fu : int -> int is not included in val fu : 'a
>> -> 'a
> 
> Yes it doesn't match at all, the type of the implementation is int, nothing 
> else.

The error message uses plural: 'Value*s* do not match'.
So this raises few questions:
1) Is (fun x -> x + 1) a value?
2) Is (x + 1) a value?
3) Is the whole line " val fu : 'a -> 'a " a value?
4) How many values are in my example?

We have to find at least two, to understand the error message!

An my conlcusion is that this is just silly, unimportant mistake:

>> So the declaration of value in mli file is called simply a 'value'. Is
>> it intentional?
> 
> It is just the word in the English language to designate this thing.

What do you mean saying 'this thing'?
The point is: *which thing*?

>> I thought that value and it's declaration are separate notions?

Are they separate in OCaml or not?
(Of course, everybody knows they have to be separate, that's why I'm
asking about the word 'value'.)

> a value is handle by a identifier and has a type
>   let ident = some_value in
> here ident and some_value are of some type

So - according to your point of view - in my example there is only one
value, which has identifier 'fu' and its type would be " 'a -> 'a " if
the implementation was corrent.
But, you remember, the error message was about *two* values.


> 
>> My reading of " val fu : 'a -> 'a " is:
>>  some partiular value vvv that belongs to set of values that satisfy
>> "forall 'a : (vvv can be used with ('a -> 'a) type)"
> 
>> But if I write
>> let (bar : 'a -> 'a ) = (fun x -> x + 1)
>> I create a value that belongs to set "exists 'a : (vvv can be used with
>> ('a -> 'a) type)"
>> So it's the other quantifier.
> 
>> I think that the quantifier has to be part of type, since a type is set
>> of values (and the quantifier plays important role when describing some
>> of such sets).
>> So my question is: since we see the same string " 'a -> 'a " that refers
>> to different types in different contexts, what are the rules? How is
>> type definition in OCaml translated to a type?
> 
> type definition in OCaml are translated to actual types by inference.
> (fun x -> x + 1) will be easily infered to (int -> int)

My question was what are the rules for putting universal and
existential quantifers into types. So we have some type definition:
'a -> ('b -> 'c)
How is it translated to a type?

I have an idea that this piece of code can sometimes be not a type
definition, but rather part of type equation.
Let's take my previous example:
let (bar : 'a -> 'a ) = ...

This " 'a -> 'a " whould not define any type (so the problem of
quantifiers would be irrelevant here), but RHS of some type equation.
Still I'm not sure about what does this RHS contais (precisely).

So: was I wrong thinking that existnetial quantifier is involved in this
example?

Dawid

Re: [Caml-list] Quantifier in the type

[Florent Monnier]

Yes you are right my first answer was totally out of scope,
I will try to make it forgive and forget with this new one :)
Still take it with care while it seems you are far more knowledged than me
to answer to your own question ;-)

> Just an elementary question.
>
> I put 'a in the interface:
> val fu : 'a -> 'a
> and int in the implementation:
> let fu x = x + 1
>
> So I have universal quantification: for any type 'a function fu can
> consume the argument. So my implementation doesn't comply with that
> universal quatification. And the message I get is following:
>
> Values do not match: val fu : int -> int is not included in val fu : 'a
> -> 'a
>
> So the declaration of value in mli file is called simply a 'value'. Is
> it intentional?

in the same way, in the mli, it is not a "declaration of value" but "a 
declaration of the type of a value" :p

> I thought that value and it's declaration are separate notions?

doen't this declaration define a value?
Anyway doesn't the declaration and the value have the same type? (which do not 
match, and this is the real important piece, it do not match!)

Well if the error message was made this way, maybe it was more for clarity and 
simplicity, more than to be fully accurate to the theory.
Maybe it should rather say "the type of the implementation of the value does 
not match the type declared for this same value in the implementation"
but it's shorter to just say "values do not match"

> My reading of " val fu : 'a -> 'a " is:
>  some partiular value vvv that belongs to set of values that satisfy
> "forall 'a : (vvv can be used with ('a -> 'a) type)"

My reading of " val fu : 'a -> 'a " is that, as this 'a thing first appears in 
the ocaml manual which refers to it with "any type" or "arbitrary type" so 
"fu takes any type and returns this same arbitrary type"

Sorry for the joke, more serious attempts below

> But if I write
> let (bar : 'a -> 'a ) = (fun x -> x + 1)
> I create a value that belongs to set "exists 'a : (vvv can be used with
> ('a -> 'a) type)"
> So it's the other quantifier.

would this be a clue about the Gral you're looking for?

# let bar = ref (None : ('a -> 'a) option) ;;
val bar : ('_a -> '_a) option ref = {contents = None}
# bar := Some (fun x -> x + 1) ;;
- : unit = ()
# !bar ;;
- : (int -> int) option = Some <fun>

But:
# let (bar : '_a -> '_a) = (fun x -> x + 1) ;;
The type variable name '_a is not allowed in programs

is disallowed


> >> I think that the quantifier has to be part of type, since a type is set
> >> of values (and the quantifier plays important role when describing some
> >> of such sets).
> >> So my question is: since we see the same string " 'a -> 'a " that refers
> >> to different types in different contexts, what are the rules? How is
> >> type definition in OCaml translated to a type?
> >
> > type definition in OCaml are translated to actual types by inference.
> > (fun x -> x + 1) will be easily infered to (int -> int)
>
> My question was what are the rules for putting universal and
> existential quantifers into types. So we have some type definition:
> 'a -> ('b -> 'c)
> How is it translated to a type?
>
> I have an idea that this piece of code can sometimes be not a type
> definition, but rather part of type equation.
> Let's take my previous example:
> let (bar : 'a -> 'a ) = ...
>
> This " 'a -> 'a " whould not define any type (so the problem of
> quantifiers would be irrelevant here), but RHS of some type equation.
> Still I'm not sure about what does this RHS contais (precisely).

Is this example an illustration of what you mean ?

# let id v = v ;;
val id : 'a -> 'a = <fun>

# Scanf.sscanf "34" "%d" id ;;
- : int = 34

# Scanf.sscanf "4578.218" "%f" id ;;
- : float = 4578.218


and related to the quantifier kind, maybe noticing this will interest you:

# Scanf.sscanf ;;
- : string -> ('a, 'b, 'c, 'd) Scanf.scanner = <fun>

# Scanf.sscanf "34" ;;
- : ('_a, '_b, '_c, '_d) Scanf.scanner = <fun>

and finally, as you told, the complementary part of the 'a -> 'a:

# Scanf.sscanf "34" "%d" ;;
- : (int -> '_a) -> '_a = <fun>


> So: was I wrong thinking that existnetial quantifier is involved in this
> example?

as far as I understand now no, you was right on this point,
but you should have understood that you are more knowledged than me about this 
subject. I'm far from a guru and while there are many talented ones arround, I 
don't know why you didn't get an anwser from one of them, maybe because we 
don't really see what is the real problem behind your question?

-- 

Re: [Caml-list] Quantifier in the type

[Tiphaine Turpin]

Hi,

I will try to expose my understanding anout your worries.

First, an interface (say I), also called a module type, is something 
whose semantics is a set of fields, which can be of several kinds: type, 
module, module type, etc., and, of course, value. In this last case, the 
statement val v : t declares that I has a "value" field v of type t, 
with the intuitive semantics that "any module of type I must export a 
value v which satisfies the type t". Then, when you compile your 
implementation m.ml and interface m.mli files together (they both have 
the same name but belong to different name spaces), it's like doing:

module M = (M : M)

i.e., it expresses a subtyping. So, module M must match module type M 
(their respective fields must match, including "value" fields in 
particular) and then, module M is "redifined" so that its type is only 
assumed to be the module type M (even if the module M had a more precise 
type, for example had more fields), for subsequent use.

So, I think the word value refers to the kind of field in your error 
message. You have exactly two fields of type value, one in the module 
type, and the other one in the module. Of course, the fields of a module 
type are given a type, but no implementation.

Second, in interfaces, type variables appearing in a value declaration 
are implicitely universally quantified (at the beginning of the 
declaration). In implementations, (at least for value definitions) they 
are existentially quantified, unless (explicitely) otherwise stated.

Hope this helps,

Tiphaine


Dawid Toton a écrit :
> Thanks for your answer; now I'll try to sate my point in a clear way,
> since you misunderstood all my questions.
>
>>> I put 'a in the interface:
>>> val fu : 'a -> 'a
>>> and int in the implementation:
>>> let fu x = x + 1
>>
>> this interface doesn't reflect the implementation, ocaml will reject 
>> it in any way
>
> OK, it's all about this rejection, e.g. what does precisely mean 'to
> reflect the implementation'.
>
>>
>>> So I have universal quantification: for any type 'a function fu can
>>> consume the argument.
>>
>> No it is not universal, imagine all the types that a user can create, 
>> you cannot handle them all (except maybe with the Obj module, but 
>> it's another question)
>
> I wanted this my sentence to be about the declatation in mli interface.
> My point is: the type in the declaration in mli implicitly contains
> universal quantifier.
>
>
>>>                       So my implementation doesn't comply with that
>>> universal quatification. And the message I get is following:
>>>
>>> Values do not match: val fu : int -> int is not included in val fu : 'a
>>> -> 'a
>>
>> Yes it doesn't match at all, the type of the implementation is int, 
>> nothing else.
>
> The error message uses plural: 'Value*s* do not match'.
> So this raises few questions:
> 1) Is (fun x -> x + 1) a value?
> 2) Is (x + 1) a value?
> 3) Is the whole line " val fu : 'a -> 'a " a value?
> 4) How many values are in my example?
>
> We have to find at least two, to understand the error message!
>
> An my conlcusion is that this is just silly, unimportant mistake:
>
>>> So the declaration of value in mli file is called simply a 'value'. Is
>>> it intentional?
>>
>> It is just the word in the English language to designate this thing.
>
> What do you mean saying 'this thing'?
> The point is: *which thing*?
>
>>> I thought that value and it's declaration are separate notions?
>
> Are they separate in OCaml or not?
> (Of course, everybody knows they have to be separate, that's why I'm
> asking about the word 'value'.)
>
>> a value is handle by a identifier and has a type
>>   let ident = some_value in
>> here ident and some_value are of some type
>
> So - according to your point of view - in my example there is only one
> value, which has identifier 'fu' and its type would be " 'a -> 'a " if
> the implementation was corrent.
> But, you remember, the error message was about *two* values.
>
>
>>
>>> My reading of " val fu : 'a -> 'a " is:
>>>  some partiular value vvv that belongs to set of values that satisfy
>>> "forall 'a : (vvv can be used with ('a -> 'a) type)"
>>
>>> But if I write
>>> let (bar : 'a -> 'a ) = (fun x -> x + 1)
>>> I create a value that belongs to set "exists 'a : (vvv can be used with
>>> ('a -> 'a) type)"
>>> So it's the other quantifier.
>>
>>> I think that the quantifier has to be part of type, since a type is set
>>> of values (and the quantifier plays important role when describing some
>>> of such sets).
>>> So my question is: since we see the same string " 'a -> 'a " that 
>>> refers
>>> to different types in different contexts, what are the rules? How is
>>> type definition in OCaml translated to a type?
>>
>> type definition in OCaml are translated to actual types by inference.
>> (fun x -> x + 1) will be easily infered to (int -> int)
>
> My question was what are the rules for putting universal and
> existential quantifers into types. So we have some type definition:
> 'a -> ('b -> 'c)
> How is it translated to a type?
>
> I have an idea that this piece of code can sometimes be not a type
> definition, but rather part of type equation.
> Let's take my previous example:
> let (bar : 'a -> 'a ) = ...
>
> This " 'a -> 'a " whould not define any type (so the problem of
> quantifiers would be irrelevant here), but RHS of some type equation.
> Still I'm not sure about what does this RHS contais (precisely).
>
> So: was I wrong thinking that existnetial quantifier is involved in this
> example?
>
> Dawid
>
> _______________________________________________
> Caml-list mailing list. Subscription management:
> http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
> Archives: http://caml.inria.fr
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs
>

Re: [Caml-list] Quantifier in the type

[Dawid Toton]

> Hope this helps,

Exactly what I wanted to know! Thanks!
Dawid