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 7ACE5BBAF for ; Wed, 15 Oct 2008 20:14:48 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AioBAFDP9UjVJFBbmmdsb2JhbACTYAEBAQEBCAsKBxEDrXuBaw X-IronPort-AV: E=Sophos;i="4.33,417,1220220000"; d="scan'208";a="30380386" Received: from mx-out.libertysurf.net (HELO mail.libertysurf.net) ([213.36.80.91]) by mail4-smtp-sop.national.inria.fr with ESMTP; 15 Oct 2008 20:14:47 +0200 Received: from [192.168.1.2] (91.168.190.6) by mail.libertysurf.net (7.3.118.8) id 48BBB44D00C6029B; Wed, 15 Oct 2008 21:13:09 +0200 From: Florent Monnier To: caml-list@yquem.inria.fr Subject: Re: [Caml-list] Quantifier in the type Date: Wed, 15 Oct 2008 20:18:26 +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: <200810152018.26396.fmonnier@linux-nantes.fr.eu.org> Cc: Dawid Toton X-Face: #L_Y84Xu>Uii")W[x~M|kDXQ"7%\'1D_ybO)a'+{"'/%k9)|Sp|OcG`x0rzWb/Z[]^2=YjB 4BVs.BzlQt]}bW<3(}hEogE*O^~7>gK"-|G[HjY{[/SO5S'hf\aNcc?<[$bSq.2o>Lw dp43:s|Qwm-9JBS1~J45M sh,'|6.4>3o4BI>+dH(5B47Cz6/cX3NZ^TG{ES Content-Type: text/plain; charset="iso-8859-1" Content-Transfer-Encoding: 7bit X-Spam: no; 0.00; quantifier:01 val:01 ocaml:01 val:01 mli:01 intentional:01 forall:01 endline:01 dup:01 baa:01 failwith:01 atan:01 4096:01 4096:01 quantifier:01 > 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 = # 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 = # 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 = # gen_add 3 ;; - : int = 4 # gen_add 3.0 ;; - : float = 4. # gen_add "3" ;; - : string = "4." -- Florent