From: "Jacques Carette" <carette@mcmaster.ca>
To: Brian Hurt <bhurt@spnz.org>, Martin Berger <martinb@dcs.qmul.ac.uk>
Cc: skaller@ozemail.com.au, Caml Mailing List <caml-list@inria.fr>
Subject: Re: Design by Contract, was Re: [Caml-list] GC and file descriptors
Date: Tue, 18 Nov 2003 21:57:14 -0500 [thread overview]
Message-ID: <web-9482517@cgpsrv2.cis.mcmaster.ca> (raw)
In-Reply-To: <Pine.LNX.4.44.0311182109210.5009-100000@localhost.localdomain>
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
next prev parent reply other threads:[~2003-11-19 2:57 UTC|newest]
Thread overview: 92+ messages / expand[flat|nested] mbox.gz Atom feed top
2003-11-13 0:50 Dustin Sallings
2003-11-13 1:18 ` David Fox
2003-11-13 4:09 ` Dustin Sallings
2003-11-14 13:42 ` Damien Doligez
2003-11-14 14:57 ` Christophe Raffalli
2003-11-14 20:24 ` Dmitry Bely
2003-11-14 20:54 ` Eric Dahlman
2003-11-14 22:21 ` Brian Hurt
2003-11-14 21:36 ` John J Lee
2003-11-14 21:48 ` Brian Hurt
2003-11-15 1:47 ` Dmitry Bely
2003-11-15 2:25 ` Max Kirillov
2003-11-15 2:49 ` Mike Furr
2003-11-16 4:09 ` [Caml-list] Bugs from ignoring errors from close (was Re: GC and file..) Tim Freeman
2003-11-15 2:58 ` [Caml-list] GC and file descriptors David Brown
2003-11-17 14:19 ` Damien Doligez
2003-11-17 18:18 ` skaller
2003-11-14 18:35 ` Dustin Sallings
2003-11-15 14:16 ` skaller
2003-11-15 15:56 ` Ville-Pertti Keinonen
2003-11-15 17:30 ` skaller
2003-11-15 20:31 ` Martin Berger
2003-11-16 19:19 ` Brian Hurt
2003-11-17 18:15 ` skaller
2003-11-17 19:26 ` Aleksey Nogin
2003-11-18 13:49 ` skaller
2003-11-18 17:51 ` Dustin Sallings
2003-11-18 20:17 ` Aleksey Nogin
2003-11-20 7:36 ` Florian Hars
2003-11-17 21:20 ` Brian Hurt
2003-11-17 23:02 ` John J Lee
2003-11-18 12:05 ` Ville-Pertti Keinonen
2003-11-18 15:19 ` skaller
2003-11-18 18:10 ` John J Lee
2003-11-18 17:55 ` skaller
2003-11-18 20:02 ` Ville-Pertti Keinonen
2003-11-18 21:20 ` John J Lee
2003-11-19 12:25 ` skaller
2003-11-19 13:55 ` Ville-Pertti Keinonen
2003-11-19 14:26 ` Samuel Lacas
2003-11-19 14:47 ` skaller
2003-11-18 15:28 ` skaller
2003-11-18 18:00 ` John J Lee
2003-11-18 22:28 ` Brian Hurt
2003-11-18 23:07 ` John J Lee
2003-11-18 23:22 ` Benjamin Geer
2003-11-19 1:49 ` Martin Berger
2003-11-19 3:57 ` Dustin Sallings
2003-11-19 13:35 ` skaller
2003-11-19 13:00 ` skaller
2003-11-19 13:02 ` skaller
2003-11-19 17:36 ` Brian Hurt
2003-11-20 5:14 ` skaller
2003-11-20 7:37 ` David Brown
2003-11-18 15:12 ` skaller
2003-11-18 16:49 ` Martin Berger
2003-11-18 17:46 ` skaller
2003-11-19 1:33 ` Martin Berger
2003-11-19 3:19 ` Design by Contract, was " Brian Hurt
2003-11-19 2:57 ` Jacques Carette [this message]
2003-11-19 13:27 ` skaller
2003-11-19 14:41 ` Martin Berger
2003-11-19 16:54 ` Richard Jones
2003-11-19 17:18 ` Damien Doligez
2003-11-19 21:45 ` Richard Jones
2003-11-19 23:09 ` Benjamin Geer
2003-11-20 0:50 ` Nicolas Cannasse
2003-11-20 9:42 ` Benjamin Geer
2003-11-19 18:03 ` Martin Berger
2003-11-18 18:26 ` Benjamin Geer
2003-11-18 19:24 ` Xavier Leroy
2003-11-18 23:49 ` Benjamin Geer
2003-11-19 1:36 ` Martin Berger
2003-11-19 2:28 ` Nicolas Cannasse
2003-11-19 3:26 ` Brian Hurt
2003-11-19 11:44 ` Martin Berger
2003-11-19 17:29 ` Brian Hurt
2003-11-20 5:17 ` skaller
2003-11-20 16:13 ` Brian Hurt
2003-11-19 13:33 ` skaller
2003-11-19 17:01 ` Richard Jones
2003-11-22 2:39 ` [Caml-list] AutoMLI (Was: GC and file descriptors) Jim
2003-11-19 17:43 ` [Caml-list] GC and file descriptors Brian Hurt
2003-11-20 5:05 ` skaller
2003-11-19 1:33 ` Martin Berger
2003-11-19 2:47 ` Benjamin Geer
2003-11-18 22:23 ` Brian Hurt
2003-11-19 13:00 ` skaller
2003-11-17 22:37 ` OCaml popularity [was: Re: [Caml-list] GC and file...] John J Lee
2003-11-18 1:02 ` [Caml-list] Re: GC and file descriptors Jed Davis
2003-11-13 1:19 ` [Caml-list] " Nicolas George
[not found] ` <87smkstkhg.fsf@igloo.phubuh.org>
[not found] ` <347A7A46-1612-11D8-8F93-000393CFE6B8@spy.net>
2003-11-13 20:18 ` Mikael Brockman
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=web-9482517@cgpsrv2.cis.mcmaster.ca \
--to=carette@mcmaster.ca \
--cc=bhurt@spnz.org \
--cc=caml-list@inria.fr \
--cc=martinb@dcs.qmul.ac.uk \
--cc=skaller@ozemail.com.au \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).