From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: 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 1414DBC48 for ; Wed, 6 Apr 2005 21:19:30 +0200 (CEST) Received: from pauillac.inria.fr (pauillac.inria.fr [128.93.11.35]) by concorde.inria.fr (8.13.0/8.13.0) with ESMTP id j36JJTFV023833 for ; Wed, 6 Apr 2005 21:19:29 +0200 Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id VAA16277 for ; Wed, 6 Apr 2005 21:19:29 +0200 (MET DST) Received: from cgpsrv2.cis.mcmaster.ca (cgpsrv2.CIS.McMaster.CA [130.113.64.62]) by concorde.inria.fr (8.13.0/8.13.0) with ESMTP id j36JJSBW023828 for ; Wed, 6 Apr 2005 21:19:28 +0200 Received: from [24.43.193.126] (account carette@univmail.cis.mcmaster.ca) by cgpsrv2.cis.mcmaster.ca (CommuniGate Pro WebUser 4.1.8) with HTTP id 88285897; Wed, 06 Apr 2005 15:19:26 -0400 From: "Jacques Carette" Subject: Re: [Caml-list] ambitious proposal: polymorphic arithmetics To: Richard Jones Cc: caml-list@inria.fr X-Mailer: CommuniGate Pro WebUser Interface v.4.1.8 Date: Wed, 06 Apr 2005 15:19:26 -0400 Message-ID: In-Reply-To: <20050406185901.GA6338@furbychan.cocan.org> MIME-Version: 1.0 Content-Type: text/plain; charset="ISO-8859-1"; format="flowed" Content-Transfer-Encoding: 8bit X-Miltered: at concorde with ID 42543641.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Miltered: at concorde with ID 42543640.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Spam: no; 0.00; caml-list:01 constructors:01 non-uniform:01 simulate:01 non-uniform:01 ocaml:01 ocaml:01 statically:01 semantics:01 integers:01 compilation:01 ...:98 wrote:01 polymorphic:01 polymorphic:01 X-Spam-Checker-Version: SpamAssassin 3.0.2 (2004-11-16) on yquem.inria.fr X-Spam-Status: No, score=0.0 required=5.0 tests=none autolearn=disabled version=3.0.2 X-Spam-Level: Richard Jones wrote: > > Pardon my ignorance, but how are GADTs are going to help in this regard? > > I thought GADTs are basically data types with constructors that have > > non-uniform "return type". > > Pardon _my_ ignorance. I read something about using GADTs to simulate > class types in the paper, and assumed that they are equivalent, but > I'm probably wrong. GADTs have non-uniform input *and* output types. But the non-uniformity still has enough regularity to it that this does not give full sub-typing or dependent types (both of which are much harder). They are a really beautiful extension of algebraic types in the 'dependent types' direction without introducing anything harder than what is already present in the type system. The chapter by Pottier and Re'my in ATTAPL pretty much admits that in writing ;-) So maybe the Ocaml developers have been working hard on this for ocaml 3.09, they just didn't want to tip their hats quite yet... Certainly GADTs are sufficient for statically typing an embedded language *and* [the important part] its 'cannot go wrong' interpreter that follows purely from the operational semantics. The leap from that to controlled, non ad hoc polymorphic + seems quite small. So if the types on which you are working are tagged, then GADTs could well help. Of course, for performance and historical reasons, int are not tagged in Ocaml, so that is a definite problem. But perhaps the 'untagging' of integers is done late enough in the compilation process (I don't know!) that it is not a real problem. Jacques