[Caml-list] Feature wish: types with invariants

[Alessandro Baretta <alex@baretta.com>]

This is a *wish* as opposed to a *request* because it does 
not add to the power of the language but only to the comfort 
and ease of use.

I would like to have the possiblity of expressing invariant 
properties which must always hold on a given datatype I'm in 
the process of defining. Consider the following definition 
of a doubly linked list:

type 'a dlist = 'a option * 'a * 'a option

There is absolutely no way to distinguish this data 
structure from that of a binary tree, or, worse yet, of a 
directed graph.

In order to enforce the structural properties of a dlist, I 
would need to disseminate the code with assertions. 
Basically, I'd like the compiler to throw in assertions for 
me whenever a new value of type dlist is constructed. Such 
assertions would have to verify invariant properties 
specified in the definition of the type.

I'd like to write:

exception Dlist_exn
type 'a dlist = 'a option * 'a * 'a option : ( dlist_value )
   where
     (match dlist_value with
        | None, _, None -> true
        | Some(_, _, this), _, None -> this == dlist_value
        | None, _, Some(this, _, _) -> this == dlist_value
        | Some(_, _, this1), _, Some(this2, _, _) ->
            this1 == dlist_value && this2 == dlist_value
      ) otherwise Dlist_exn

What do you guys think? It should not be overly messy, or am 
I completely mistaken?

Alex

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