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

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

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
>