From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by walapai.inria.fr (8.13.6/8.13.6) with ESMTP id q37GkDLw008699 for ; Sat, 7 Apr 2012 18:46:13 +0200 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: Au4CAKBugE/RVdK2mGdsb2JhbAArGhanL5FTCCIBAQEBAQgJDQcUJ4IJAQEBAgISAiwBCBMSCwEDDAYFCw0NISIBEQEFAQoSBhMJCQIOh10BAwsLKZsECowZgnGETgoZJwMKV4h2AQULkE8ElWyBEY1FPYQM X-IronPort-AV: E=Sophos;i="4.75,387,1330902000"; d="scan'208";a="139445375" Received: from mail-iy0-f182.google.com ([209.85.210.182]) by mail4-smtp-sop.national.inria.fr with ESMTP/TLS/RC4-SHA; 07 Apr 2012 18:46:07 +0200 Received: by iahk25 with SMTP id k25so6907094iah.27 for ; Sat, 07 Apr 2012 09:46:06 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-type:content-transfer-encoding; bh=FYtSsSG+lvJrXJJsqVAQbexlxpEgM61VpXbBmPdIeTg=; b=Vu2XDcUg97XcSHQZCaaW0BlItC2DN4FU2IKFJ/lF2xl5WHNHF/zv3YJzUtCNdh7quw 7Hfit+lUhh7mJQ94v4IL4AFOX5B96XjpDAlVrbXewq6CN4MosKuQmiMPVxXaU3+ag2g0 smmwRtzChvkvqgWd+V8B+20Ohhj53+purlQTaR2L0tPmP+ruD9F/68uXz9goTdCtnPYb W9tOOqnU83iLKO0JZdqy00z8qTvQB0e+XEj/SEgARfEE6dtsaxSEIxR0Lmm1Y7EaX5q3 WQaodKJRz0gF6d9hq4fqBw2SJ1mFuTnea5ySv1Lyli9gEkfMp9cQNqq83svT+pUIW+mg fSOg== Received: by 10.42.180.66 with SMTP id bt2mr1004197icb.56.1333817166476; Sat, 07 Apr 2012 09:46:06 -0700 (PDT) MIME-Version: 1.0 Received: by 10.50.140.100 with HTTP; Sat, 7 Apr 2012 09:45:26 -0700 (PDT) In-Reply-To: <20120407151452.GA12887@siouxsie> References: <20120407151452.GA12887@siouxsie> From: Gabriel Scherer Date: Sat, 7 Apr 2012 18:45:26 +0200 Message-ID: To: oliver Cc: caml-list@inria.fr Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 8bit X-MIME-Autoconverted: from quoted-printable to 8bit by walapai.inria.fr id q37GkDLw008699 Subject: Re: [Caml-list] Articles on using types for enhancing sw-quality? In the ML-type-system community, enforcing invariant through typing has mostly been discussed, as far as I'm aware, informally, and is part of the language communities folklore. There have been publications centered on the use of richer features (than the base ML type systems), with examples that fit into your description. So pick any advanced type-system feature X (phantom types, GADTs, polymorphic variants, private types, higher-order polymorphism) and you will find examples of "how X allows to write Y in a safer way". Some examples: - François Pottier and Yann Régis-Gianas used GADTs to encode the stack shape of a LR parser, getting safer, more efficient generated parsers as a result: http://gallium.inria.fr/~fpottier/publis/fpottier-regis-gianas-typed-lr.pdf - Martin Sulzmann and Razvan Voicu added general Constraint Handling Rules to GADT in the Chameleon and were able to encode even more sophisticated invariants in the type system. Such use of constraint/logical programming at the type level was however not adopted in the mainstream ML languages. Language-Based Program Verification via Expressive Types www.cs.mu.oz.au/~sulzmann/publications/plpv06-langverification.ps - Chung-chieh Shan and Oleg's "Lightweight Static Capabilities" presents several examples of phantom types and a general design method to use them to enhance program safety: http://okmij.org/ftp/papers/lightweight-static-capabilities.pdf - The ST monad in Haskell, initially described by Simon Peyton-Jones and John Launchbury, is a very clever use of higher-order polymorphism to make the system prove that some simple but common cases of interal use of mutable state are observably pure http://research.microsoft.com/~simonpj/Papers/state-lasc.ps.gz Fluet and Morrisett expanded this idea to represent full-fledged region types in a sufficiently expressive ML type system. See the maybe-practical examples by Oleg: http://okmij.org/ftp/Haskell/regions.html - "regular types" being used to describe expressive static types about XML data http://www.cduce.org/ There are two other related communities discussing the use of types for program correctness. The obvious candidate is the community advocating programming with dependent types (using Coq, Agda, Epigram, Cayenne, Guru, etc.). They have plenty of literature on how you can use dependent types to get full functional correctness as a result of type-checking -- the price to pay being very subtle and difficult programming. See for examples the long list of "Papers using Agda" here: http://wiki.portal.chalmers.se/agda/agda.php?n=Main.Publications The less obvious community is the fraction of the people working on retrofitting static analysis into dynamically typed languages. This is difficult because the programs that are written tend to falsify a lot of the simplifying invariants typed programmers respect and use to reason about (such as the fact that all elements of a list have the same type), and you need relatively powerful and forgiving type systems to accept that. Furthermore, people working in this area have a hard time selling the idea to their larger community, so they tend to use examples, case studies, killer applications, etc... See for example: - Sam Tobin-Hochstadt work on Typed Racket: http://www.informatik.uni-trier.de/~ley/db/indices/a-tree/t/Tobin=Hochstadt:Sam.html - the work on Dyalizer, a static analys tool for Erlang, based on a kind of "optimistic typing" that only rejects programs that are provably wrong, instead of only accepting programs that are provably safe. A part of what Dialyzer allows is to write type annotations for Erlang functions; the methodology of incrementally adding annotations/specifications to increase confidence in a program is described in the paper "Gradual Typing of Erlang Programs: A Wrangler Experience", by Konstantinos Sagonas and Daniel Luna. http://www.it.uu.se/research/group/hipe/dialyzer http://www.it.uu.se/research/group/hipe/dialyzer/publications/wrangler.pdf On Sat, Apr 7, 2012 at 5:14 PM, oliver wrote: > Hello, > > do you know of articles (or books?) that describe > the usage of types for enhancing software quality > by coding the software invariants as types? > > (And if possible, for example enforce certain operations >  on such values, maybe also encoded as types?) > > I remember an interesting talk from Yaron Minsky > on that topic. > But this rather was an explanation on > why OCaml and other strongly typed languages are > very useful to ensure software integrity by the > type system. There were examples, but not completely > going too much into depth there. > > I would like to explore this more thoroughly and look > for articles / books (or other videos), that explain > the design technique in more depth. > > So, if you know of something regarding this topic, > please let me know. > > Ciao, >   Oliver > > -- > Caml-list mailing list.  Subscription management and archives: > https://sympa-roc.inria.fr/wws/info/caml-list > Beginner's list: http://groups.yahoo.com/group/ocaml_beginners > Bug reports: http://caml.inria.fr/bin/caml-bugs >