Re: [Caml-list] Articles on using types for enhancing sw-quality?

[Gabriel Scherer <gabriel.scherer@gmail.com>]

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 <oliver@first.in-berlin.de> 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
>