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 ED299BBAF for ; Fri, 17 Oct 2008 01:00:55 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AjgBAMdk90jVJFBbmmdsb2JhbACTZgEBAQEBCAsKBxEDsA2DbA X-IronPort-AV: E=Sophos;i="4.33,427,1220220000"; d="scan'208";a="30434336" Received: from mx-out.libertysurf.net (HELO mail.libertysurf.net) ([213.36.80.91]) by mail4-smtp-sop.national.inria.fr with ESMTP; 17 Oct 2008 01:00:39 +0200 Received: from [192.168.1.2] (91.168.189.240) by mail.libertysurf.net (7.3.118.8) id 48BBB55800CBB789; Fri, 17 Oct 2008 02:01:07 +0200 From: Florent Monnier To: caml-list@yquem.inria.fr Subject: Re: [Caml-list] Quantifier in the type Date: Fri, 17 Oct 2008 01:06:15 +0200 User-Agent: KMail/1.9.7 References: <48F60638.6040101@uj.edu.pl> In-Reply-To: <48F60638.6040101@uj.edu.pl> MIME-Version: 1.0 Content-Disposition: inline Message-Id: <200810170106.15327.fmonnier@linux-nantes.fr.eu.org> Cc: Dawid Toton X-Face: 3;O!c1{)~4&_jb2r*-$UNg~[=@Ut{y*A[h'l(O;X)m^!3CP.]0'qf8C^\R_K;x^qwV(eZm3 oc"o+EnX+gJ-@Ypf0UiiE"?|:(<|=}Z=~ 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 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 = # 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 = # Scanf.sscanf "34" ;; - : ('_a, '_b, '_c, '_d) Scanf.scanner = and finally, as you told, the complementary part of the 'a -> 'a: # Scanf.sscanf "34" "%d" ;; - : (int -> '_a) -> '_a = > 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? --