Ocaml type with constraints?

Ocaml type with constraints?

[Angela Zhu]

[-- Attachment #1: Type: text/plain, Size: 342 bytes --]

Hi,
I want to define an OCaml type with constraints.
For example:

type item = Item of int * float;;

If here this float type is for price of some item, and I want to make sure
it is positive. In other words, if x = (xi, xf) of type item,
I want to enforce, xf must >= 0.

Is there a way to define OCaml type like this?

Thanks a lot!
Angela

[-- Attachment #2: Type: text/html, Size: 557 bytes --]

Re: [Caml-list] Ocaml type with constraints?

[Andrej Bauer]

Angela Zhu wrote:
> Hi, 
> 
> I want to define an OCaml type with constraints.
> For example:
> 
> type item = Item of int * float;;
> 
> If here this float type is for price of some item, and I want to make sure
> it is positive. In other words, if x = (xi, xf) of type item, 
> I want to enforce, xf must >= 0.
> 
> Is there a way to define OCaml type like this?

No, because Ocaml type checker always check all the types at compile
time. It is an undecidable problem whether a given expression of type
float evaluates to a non-negative number.

Best regards,

Andrej

Re: [Caml-list] Ocaml type with constraints?

[Gordon Henriksen]

On Sep 21, 2008, at 18:01, Angela Zhu wrote:

> I want to define an OCaml type with constraints. For example:
>
> type item = Item of int * float;;
>
> If here this float type is for price of some item, and I want to  
> make sure it is positive. In other words, if x = (xi, xf) of type  
> item, I want to enforce, xf must >= 0.
>
> Is there a way to define OCaml type like this?

Private types allow this enforcement, although you must implement the  
checks at runtime for the reason previously mentioned.

— Gordon

Re: [Caml-list] Ocaml type with constraints?

[Martin Jambon]

On Mon, 22 Sep 2008, Andrej Bauer wrote:

> Angela Zhu wrote:
>> Hi,
>>
>> I want to define an OCaml type with constraints.
>> For example:
>>
>> type item = Item of int * float;;
>>
>> If here this float type is for price of some item, and I want to make sure
>> it is positive. In other words, if x = (xi, xf) of type item,
>> I want to enforce, xf must >= 0.
>>
>> Is there a way to define OCaml type like this?
>
> No, because Ocaml type checker always check all the types at compile
> time. It is an undecidable problem whether a given expression of type
> float evaluates to a non-negative number.

By the way, even float does not guarantee to have a number: 0./.0. 
compiles and runs happily.


Martin

--
http://mjambon.com/

Re: [Caml-list] Ocaml type with constraints?

[Jacques Garrigue]

From: "Angela Zhu" <angela22.zhu@gmail.com>

> I want to define an OCaml type with constraints.
> For example:
> 
> type item = Item of int * float;;
> 
> If here this float type is for price of some item, and I want to make sure
> it is positive. In other words, if x = (xi, xf) of type item,
> I want to enforce, xf must >= 0.
> 
> Is there a way to define OCaml type like this?

This is the goal of private types.

module Item : sig
  type item = private Item of int * float
  val create : int -> float -> item
end = struct
  type item = Item of int * float
  let create n p =
    if p >= 0. then Item (n, p) else invalid_arg "Item.create"
end

# Item.create 3 9.95;;
- : Item.item = Item.Item (3, 9.95)
# Item.create 3 (-1.0);;
Exception: Invalid_argument "Item.create".

Note that you must imperatively use Item.create to create an item, but
you can use pattern-matching as usual to access its contents.

Jacques Garrigue