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

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

[oliver]

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

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

[Gabriel Scherer]

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
>

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

[Cedric Cellier]

 
> - 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

I attempted to read this one out of curiosity,
and it raised a question: is there a way to write
these unsafe functions (List.Unsafe.tail/head...) in pure OCaml?

this code:

let head (Cons (a, b)) = a

would still generate code that check input constructor in order to raise an exception if it's not Cons (-unsafe command line parameter does not change this, regretably, according to the manual).

Is there another way?

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

[Gabriel Kerneis]

On Mon, Apr 09, 2012 at 07:37:48AM +0200, Cedric Cellier wrote:
> > - 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
> 
> I attempted to read this one out of curiosity,
> and it raised a question: is there a way to write
> these unsafe functions (List.Unsafe.tail/head...) in pure OCaml?

It depends on what you call "pure OCaml".  Using the evil Obj module:

let head (l : 'a list) : 'a = Obj.obj (Obj.field (Obj.repr l) 0) ;;

which relies on the underlying representation (use at your own risks) and
generates a call to caml_array_unsafe_get:
    L1: const 0
        push
        acc 1
        ccall caml_array_unsafe_get, 2
        return 1

Similarly:
let tail (l : 'a list) : 'a list = Obj.obj (Obj.field (Obj.repr l) 1) ;;

Best,
-- 
Gabriel

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

[Gabriel Scherer]

In the next OCaml version, you will be able to do that more cleanly with GADTs.
That is actually one of the advantages of having GADTs in the
language; while the typing effects can be (more or less awkwardly)
encoded in existing constructions, such encodings tends to rely on
higher-order constructions and are not very efficient at runtime. By
contrast, with plain GADTs, you get the usual algebraic datatypes
(which are very efficiently handled by the compiler), with some
additional goodness due to type-informed dead clause removal.

    type 'a li =
      | Nil
      | Cons of 'a * 'a li

    let head (Cons (hd, _tl)) = hd
    (* ocamlopt -dlambda:
       (let
         (head/1037
           (function param/1068
             (if param/1068 (field 0 param/1068)
               (raise
                 (makeblock 0 (global Match_failure/16g) [0: "test.ml" 5 4])))))
    *)


    (* size-indexed lists *)
    type z
    type 'n s

    type ('a, _) gli =
      | GNil : ('a, z) gli
      | GCons : 'a * ('a, 'n) gli -> ('a, 'n s) gli

    let ghead : type a n . (a, n s) gli -> a =
      fun (GCons (hd, _tl)) -> hd
    (* ocamlopt -dlambda:
       (let (ghead/1051 (function param/1069 (field 0 param/1069)))
    *)


On Mon, Apr 9, 2012 at 8:51 AM, Gabriel Kerneis <kerneis@pps.jussieu.fr> wrote:
> On Mon, Apr 09, 2012 at 07:37:48AM +0200, Cedric Cellier wrote:
>> > - 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
>>
>> I attempted to read this one out of curiosity,
>> and it raised a question: is there a way to write
>> these unsafe functions (List.Unsafe.tail/head...) in pure OCaml?
>
> It depends on what you call "pure OCaml".  Using the evil Obj module:
>
> let head (l : 'a list) : 'a = Obj.obj (Obj.field (Obj.repr l) 0) ;;
>
> which relies on the underlying representation (use at your own risks) and
> generates a call to caml_array_unsafe_get:
>    L1: const 0
>        push
>        acc 1
>        ccall caml_array_unsafe_get, 2
>        return 1
>
> Similarly:
> let tail (l : 'a list) : 'a list = Obj.obj (Obj.field (Obj.repr l) 1) ;;
>
> Best,
> --
> Gabriel
>
> --
> 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
>

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

[oliver]

On Sat, Apr 07, 2012 at 06:45:26PM +0200, Gabriel Scherer wrote:
> 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
[...]


Thank you for the many links.

Thats much more than I expected to be there. :-)

Ciao,
   Oliver

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

[Daniel Bünzli]

Le samedi, 7 avril 2012 à 17:14, oliver a écrit :

> do you know of articles (or books?) that describe
> the usage of types for enhancing software quality
> by coding the software invariants as types?


The following paper shows how parametric polymorphism can be used to encode a finite subtyping hierarchy.
  

http://dx.doi.org/10.1017/S0956796806006046
http://www.cs.cornell.edu/people/fluet/research/phantom-subtyping/

Best,

Daniel