OCaml学习——OCaml-Datatypes

OCaml Datatypes

We have seen a number of basic types (e.g. int, float, char, string, bool) and a few structured types (e.g. pairs, tuples, options, lists).

In this lecture, we will see some more general ways to define our own new types and data structures.

Type Abbreviations

1
type point = float * float
  • helpful documentation
  • add nothing of substance to the language (equal to an existing type)

Data Types

1
type my_bool = Tru | Fal

|means or, a value with type my_bool is one of two things. Tru and Fal are called "constructors" (recall the constructors in Coq )

OCaml's datatype mechanism allows you to create types that contain precisely the values you want!

This is like an "enumeration" type in Pascal, C, Java,... . Just recall the explanation of constructors and constructor expressions in Coq this datatype(definition) explicitly enumerate a finite set of elements.

Data Types Can Carry Additional Values

Test

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
type point = float * float

type simple_shape =
  | Circle of point * float
  | Square of point * float

let origin : point = (0.0, 0.0)

let circ1  : simple_shape = Circle (origin, 1.0)
let circ2  : simple_shape = Circle ((1.0, 1.0), 5.0)
let square : simple_shape = Square (origin, 2.3)


let simple_area (s: simple_shape) : float =
  match s with
  | Circle (_, radius) -> 3.14 *. radius *. radius
  | Square (_, side) -> side *. side

Summary

A datatype \(t\) has constructors \(c_1\) \(c_2\) \(c_3\) \(\cdots\)

Each constructor may carry a value (like Square(s)) or be a constant constructor (like Green)

We build values of type \(t\) by applying constructors to values (or by applying constant constructors to nothing)

We examine values of type t by pattern-matching

Inductive Datatypes

Recall using int to represent nat, not good.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
type nat = Zero | Succ of nat

let rec nat_to_int (n:nat) : int =
  match n with
  | Zero -> 0
  | Succ n -> 1 + nat_to_int n

let rec double_nat (n:nat) : nat =
  match n with
  | Zero -> Zero
  | Succ n -> Succ (Succ (double_nat n))


let nat_test_zero = Zero

let _ = Printf.printf "%d\n" (nat_to_int (double_nat (Succ Zero) ))

Recall in Coq. Induction Zero (O) and Succ of nat (S(n:nat)).

1
2
3
Inductive nat : Type :=
  | O
  | S (n : nat).

Summary

OCaml data types: a powerful mechanism for defining comples data structures.

  • precise
  • general
  • type checker helps you detect errors