From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.1.3 (2006-06-01) on yquem.inria.fr X-Spam-Level: X-Spam-Status: No, score=0.0 required=5.0 tests=none autolearn=disabled version=3.1.3 X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by yquem.inria.fr (Postfix) with ESMTP id 152EABBB7 for ; Thu, 16 Oct 2008 17:37:40 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AtUCAID89kiVnFmTlmdsb2JhbACTZgEBAQEJCwoYqEiGP1+DbA X-IronPort-AV: E=Sophos;i="4.33,424,1220220000"; d="scan'208";a="30418359" Received: from mail.uj.edu.pl ([149.156.89.147]) by mail4-smtp-sop.national.inria.fr with ESMTP; 16 Oct 2008 17:37:39 +0200 MIME-version: 1.0 Content-transfer-encoding: 7BIT Content-type: text/plain; charset=ISO-8859-1; format=flowed Received: from [137.73.5.196] by mail.uj.edu.pl (Sun Java(tm) System Messaging Server 6.3-5.02 (built Oct 12 2007; 32bit)) with ESMTPA id <0K8U00BQE8KLSS30@mail.uj.edu.pl> for caml-list@yquem.inria.fr; Thu, 16 Oct 2008 17:33:58 +0200 (CEST) Message-id: <48F75EE5.6030009@uj.edu.pl> Date: Thu, 16 Oct 2008 16:33:57 +0100 From: Dawid Toton User-Agent: Thunderbird 1.5.0.12 (X11/20080804) To: caml-list@yquem.inria.fr Subject: Re: [Caml-list] Quantifier in the type References: <48F60638.6040101@uj.edu.pl> <200810152018.26396.fmonnier@linux-nantes.fr.eu.org> In-reply-to: <200810152018.26396.fmonnier@linux-nantes.fr.eu.org> X-Spam: no; 0.00; quantifier:01 val:01 ocaml:01 mli:01 mli:01 quantifier:01 val:01 plural:01 intentional:01 ocaml:01 forall:01 translated:01 translated:01 inference:01 existential:01 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