Skip to content

Sixian Li

Inductive Data Types

Functional Programming

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

Let [ ] is a list. If you have a list, say l, and an item, sayi, then i::l is also a list. List0 = [ ] List1 = [1], [2],...,[ ] 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.

  • Inductive definition: EMPTY is a tree. If t1, t2 are trees, and i is an item. Then i(t1, t2) is a tree (NOT linear).

  • How to code a Tree in OCaml We have user-defined inductive types. type 'a tree = Empty | Node of 'a tree * 'a * 'a tree

    1. 'a means:Polymorphic binary trees. 'a can 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;;

    2. Node: constructor function. Always start with capital letters.

    • Examples:

  • Expression trees

    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 t is a type, then t option is another type. Allows you to optionally return a NOne value.

    • EX. 1729 is an integer.

      None is an integer option.

      Some 1729 is an integer option.

      Not returning int value, return int option.