Inductive Data Types
Lecture notes for COMP302.
Lists as inductive structures
- NOTE: Induction works if and only if the system has a well-founded order.
Inductive definitions of data types
[ ] is a list. If you have a list, say
l, and an item, say
i::l is also a list.
List0 = [ ]
List1 = , ,...,[ ]
List2 = [1; 1], [1; 2],...,[4; 1],...
The entire collection LIST = union_n LIST_n, an infinite set. However, the description is short, concise, and finite.
This is a built-in type. There are functions like
map, filter in this module.
How do I define my own inductive types?
Lists are linear data types, tail recursion works well for linear data types.
Trees are not built-in. Here we only talked about binary trees.
EMPTYis a tree. If
t1, t2are trees, and
iis an item. Then
i(t1, t2)is a tree (NOT linear).
How to code a
Treein OCaml We have user-defined inductive types.
type 'a tree = Empty | Node of 'a tree * 'a * 'a tree
'a means:Polymorphic binary trees.
'acan be instantiated with any type: ints, strings…
You don’t have to declare types. Type inference comes to help.
let max (n, m) = if n < m then m else n;;
Node: constructor function. Always start with capital letters.
Const, Var, Plus, Times
type binding: char * int
type env = binding list
let rho: env = [('x', 11); ('y', 7); ('z', 2)]
What if there’s no such names?
OPTION TYPE, a new type constructor. If
tis a type, then
t optionis another type. Allows you to optionally return a
EX. 1729 is an integer.
None is an integer option.
Some 1729 is an integer option.
Not returning int value, return