Browse thread
Quantifier in the type
[
Home
]
[ Index:
by date
|
by threads
]
[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
[ 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