From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by yquem.inria.fr (Postfix) with ESMTP id DA8C8BB83 for ; Tue, 4 Jul 2006 23:08:57 +0200 (CEST) Received: from smtp4-g19.free.fr (smtp4-g19.free.fr [212.27.42.30]) by concorde.inria.fr (8.13.6/8.13.6) with ESMTP id k64L8wN9006178 for ; Tue, 4 Jul 2006 23:08:58 +0200 Received: from localhost (gob75-2-81-56-65-67.fbx.proxad.net [81.56.65.67]) by smtp4-g19.free.fr (Postfix) with ESMTP id B11644F5E6; Tue, 4 Jul 2006 23:08:57 +0200 (CEST) Received: from boris by localhost with local (Exim 4.62) (envelope-from ) id 1Fxs8Z-0006wf-FK; Tue, 04 Jul 2006 23:08:51 +0200 Date: Tue, 4 Jul 2006 23:08:50 +0200 From: Boris Yakobowski To: brogoff Cc: caml-list@yquem.inria.fr Subject: Re: Petty complaint (Was Re: [Caml-list] Type from local module would escape its )scope? Message-ID: <20060704210850.GA25504@elrond.dynalias.net> Reply-To: Boris Yakobowski Mail-Followup-To: Boris Yakobowski , brogoff , caml-list@yquem.inria.fr References: <069A1F65-E50C-4363-9CCA-C6CC9A453D09@vub.ac.be> <20060703155131.7031cffa@is003364.intra.cea.fr> MIME-Version: 1.0 Content-Type: text/plain; charset=iso-8859-1 Content-Disposition: inline Content-Transfer-Encoding: 8bit In-Reply-To: X-Operating-System: Linux elrond 2.6.16.14 User-Agent: Mutt/1.5.11+cvs20060403 X-Miltered: at concorde with ID 44AAD8EA.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Spam: no; 0.00; yakobowski:01 yakobowski:01 ocaml:01 encodings:01 polymorphism:01 expressivity:01 inference:01 undecidable:01 hypothetical:01 abstractions:01 recursive:01 rec:01 forall:01 annotations:01 haskell:01 X-Spam-Checker-Version: SpamAssassin 3.0.3 (2005-04-27) on yquem.inria.fr X-Spam-Level: X-Spam-Status: No, score=0.0 required=5.0 tests=none autolearn=disabled version=3.0.3 On Mon, Jul 03, 2006 at 10:30:38AM -0700, brogoff wrote: > It makes me wonder, if OCaml is to be a functional language, why > functions are second class citizens of the language with regards > to typing? By various encodings you can get this higher rank > polymorphism, it's been there for years, but we can't write the function > directly. Is it because we'd have to write it's type? As Étienne Miret mentionned, what you're basically asking for is the expressivity of System F. Unfortunately, type inference in that system is undecidable, and its practicality as a programming langage is more than doubtful. Below is the map function on lists in an hypothetical F-based language. Notice that map must be fully annotated, incuding type abstractions and type applications; this is why the recursive call is map A B f q instead of map f q in ML. let rec map : forall A B. (A -> B) -> A list -> B list = fun A B (l : list A) -> match l with | [] -> [] | cons h q -> cons B (f h) (map A B f q) Numerous attempts at finding intermediary langages which would require less annotations exist. However, few of them have found their ways in mainstream programming languages. In fact, the only practical system I'm aware of is an extension of Haskell which can be found in Ghc ; see http://www.haskell.org/ghc/docs/latest/html/users_guide/type-extensions.html#universal-quantification for some examples. Annotations are quite light : you only need to annotate functions which have an F type (ML types are infered as usual). The only problem with this approach is that the system used is predicative: polymorphic instantiation is limited to simple types. Given a function with type forall A. \sigma -> \sigma', it can only be applied with a type t which is a monotype. For example, given the function app defined by app f x = f x, it is not always the case that app f x is typable, even if f x is. Hence, the system can sometimes lack compositionnality. Also, it is not possible to write lists of polymorphic functions without encapsulating the element inside polymorphic variants or records; this is similar to the current situation in OCaml. MLF is another attempt at taming the power of system F. The amount of type annotations is similar to the one required for the GHC extension: annotations on arguments which are used really polymorphically. On the plus side, MLF is impredicative, hence more expressive; in particular, none of the problems I mentionned above occur. Unfortunately, there are some downsides. Types of MLF are less readable than those of System F, although some solutions to mitigate this problem exist. Also, it was not obvious that the algorithms for type inference in MLF would scale to large-scale programs; this is on the verge of being resolved. More problematic is the fact that MLF does not yet support recursive types. Hence, adding it in OCaml would mean it would not be usable with objects, in which higher-order polymorphism is often useful. More generally, adding a new type feature to the OCaml compiler requires understanding its interactions with the myriad of existing extensions (objects, polymorphic variants, optional arguments, boxed polymorphism...), a non-trivial task. -- Boris