From mboxrd@z Thu Jan 1 00:00:00 1970 Received: (from majordomo@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id DAA24737; Wed, 19 Nov 2003 03:57:19 +0100 (MET) X-Authentication-Warning: pauillac.inria.fr: majordomo set sender to owner-caml-list@pauillac.inria.fr using -f 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 DAA25125 for ; Wed, 19 Nov 2003 03:57:17 +0100 (MET) Received: from cgpsrv2.cis.mcmaster.ca (cgpsrv2.CIS.McMaster.CA [130.113.64.62]) by concorde.inria.fr (8.11.1/8.11.1) with ESMTP id hAJ2vG122447 for ; Wed, 19 Nov 2003 03:57:16 +0100 (MET) Received: from [65.48.130.10] (account ) by cgpsrv2.cis.mcmaster.ca (CommuniGate Pro WebUser 4.0.6) with HTTP id 9482517; Tue, 18 Nov 2003 21:57:14 -0500 From: "Jacques Carette" Subject: Re: Design by Contract, was Re: [Caml-list] GC and file descriptors To: Brian Hurt , Martin Berger Cc: skaller@ozemail.com.au, Caml Mailing List X-Mailer: CommuniGate Pro Web Mailer v.4.0.6 Date: Tue, 18 Nov 2003 21:57:14 -0500 Message-ID: In-Reply-To: MIME-Version: 1.0 Content-Type: text/plain; charset="ISO-8859-1"; format="flowed" Content-Transfer-Encoding: 8bit X-Loop: caml-list@inria.fr X-Spam: no; 0.00; jacques:01 caml-list:01 undecidable:01 decidable:01 decidable:01 haskell:01 polynomial:01 undecidable:01 jacques:01 ocaml:01 contracts:98 descriptors:01 complexity:02 harder:02 dependent:03 Sender: owner-caml-list@pauillac.inria.fr Precedence: bulk About contracts and dependent types: of course full dependent types are undecidable, but those are rarely needed? On the other hand, linear constraints over the integers are often needed, AND are not only fully decidable, there are both nice complexity results as well as practical algorithms [not both together :-( yet]. What puzzles me is that some decidable subset of dependent types is not part of any 'real' programming language (like Ocaml or Haskell). Certainly the Array code just posted is a nice example where having dependent types with only linear constraints over the integers as the 'extra' power is enough to resolve everything. In fact, it seems that almost all examples of dependent types that I have seen in the type theory litterature are of this kind; counter-examples typically use polynomial constraints, which are undecidable in general. Or am I missing something obvious that makes this much harder than it seems? Jacques ------------------- To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/ Beginner's list: http://groups.yahoo.com/group/ocaml_beginners