Browse thread
[Caml-list] Feature wish: types with invariants
- Alessandro Baretta
[
Home
]
[ Index:
by date
|
by threads
]
[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
| Date: | -- (:) |
| From: | Alessandro Baretta <alex@b...> |
| Subject: | [Caml-list] Feature wish: types with invariants |
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