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 mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by yquem.inria.fr (Postfix) with ESMTP id 7B2E2BC37 for ; Sun, 28 Feb 2010 12:07:24 +0100 (CET) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AnoBAF/diUtV2gB4nGdsb2JhbACDBZgtAQEBAQEICwgJEyKpZY8ygTSCXWoEiXI X-IronPort-AV: E=Sophos;i="4.49,554,1262559600"; d="scan'208";a="45627790" Received: from emailfrontal1.citycable.ch ([85.218.0.120]) by mail2-smtp-roc.national.inria.fr with SMTP; 28 Feb 2010 12:07:24 +0100 Received: from [192.168.0.12] (unknown [85.218.92.99]) (Authenticated sender: guillaume.yziquel@citycable.ch) by emailfrontal1.citycable.ch (Postfix) with ESMTPA id 4C01912C1CF; Sun, 28 Feb 2010 12:07:22 +0100 (CET) Message-ID: <4B8A4E94.3030307@citycable.ch> Date: Sun, 28 Feb 2010 12:08:04 +0100 From: Guillaume Yziquel Reply-To: guillaume.yziquel@citycable.ch User-Agent: Mozilla-Thunderbird 2.0.0.22 (X11/20090707) MIME-Version: 1.0 To: Goswin von Brederlow Cc: Andreas Rossberg , OCaml List Subject: Re: [Caml-list] Recursive subtyping issue References: <4B887AED.3090005@citycable.ch> <4B88F32C.3050701@citycable.ch> <87k4tyoq3m.fsf@frosties.localdomain> <4B891A0C.604@citycable.ch> <87tyt1r8hk.fsf@frosties.localdomain> In-Reply-To: <87tyt1r8hk.fsf@frosties.localdomain> Content-Type: text/plain; charset=UTF-8; format=flowed Content-Transfer-Encoding: quoted-printable X-Spam: no; 0.00; guillaume:01 guillaume:01 recursive:01 subtyping:01 inference:01 type-checked:01 bindings:01 subtyping:01 bindings:01 ocaml:01 ocaml:01 node:01 val:01 val:01 foo:01 Goswin von Brederlow a =C3=A9crit : >> >> Doing 'a t =3D private underlying allows you to create a type inferenc= e >> barrier. However, you also want to be able to cast from underlying to >> 'a t, when you get the result of a function in R or Python, for >> instance. >> >> So that's exactly the use case you mentionned above. >> >>> Why not supply conversion functions that do any additional checks to >>> ensure the conversion is a valid one? Consider the following: >> >> Because that's exactly what I try to avoid. R and Python are already >> slow enough and dynamically type-checked at every corner. I'm not >> happy to add another type-checking layer. >=20 > But if you do not check then someone can convert a float q into w and > back into int q. That would hide the error in the conversion until such > a time as the type is later used in some function that does check the > type. I would rather have those checks than go hunting for the real > error for hours. Yes and no. In some sense, when you do bindings of C code, you do have to be=20 careful. There's no reason that it should be different for binding=20 Python code or R code. I mean, having a slick binding without dynamic type checks is, from my=20 point of view, a good thing. But this subtyping is for the person binding R or Python code. The user of the binded code should not see any subtyping. That's the=20 goal: having a good framework to do the bindings. Not exposing low level=20 R or Python details the the OCaml coder using the bindings. >> I've been looking all over at this issue, but simply cannot find a way >> out. While experimenting on this, I've stumbled on a number of quirky >> issues with the type system. >> >> First one: http://ocaml.janestreet.com/?q=3Dnode/26 >> >> Second one: >> >>> # type 'a q =3D ;; >>> type 'a q =3D < m : 'a > >>> # let f : 'a q -> 'a q =3D fun x -> x;; >>> val f : 'a q -> 'a q =3D >>> # let o =3D object method m : 'a. 'a -> 'a =3D fun x -> x end;; val o= : >>> < m : 'a. 'a -> 'a > =3D >>> # f o;; >>> Error: This expression has type < m : 'a. 'a -> 'a > >>> but an expression was expected of type 'b q >>> The universal variable 'a would escape its scope >>> # >> All these issues seem to be somehow related, in a way I'm not yet able >> to articulate clearly. >=20 > # class ['a] foo =3D object method map (f : 'a -> 'b) =3D ((Obj.magic 0= ) : 'b foo) end;; > class ['a] foo : object method map : ('a -> 'a) -> 'a foo end >=20 > As I recently learned there seems to be no way to make that actualy > produce a 'b foo. I think that hits the same problem. >=20 > MfG > Goswin Will have a look at that when I find the time. --=20 Guillaume Yziquel http://yziquel.homelinux.org/