Version française
Home     About     Download     Resources     Contact us    
Browse thread
Quantifier in the type
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: -- (:)
From: Dawid Toton <dawid.toton@u...>
Subject: Quantifier in the type
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