Values, functions and data

Chapter 1’s program greets the world. From here on, you build something more useful: a todo list. Create src/hello/todo.hf, and add each definition in this chapter to it, in order, after its name:

module hello.todo

Data types

data Status = Open | Done

A data type lists its constructors. A Status is either Open or Done.

Records

type Todo = { title : String, status : Status }

todo : String -> Todo
todo title = { title = title, status = Open }

finish : Todo -> Todo
finish t = { t | status = Done }

A record type names its fields. t.title reads a field, and { t | status = Done } is t with one field replaced.

Pattern matching

pending : Status -> Bool
pending Open = True
pending Done = False

isOpen : Todo -> Bool
isOpen t = pending t.status

A function can have one equation per pattern.

As text

instance toStringStatus : Show Status
toStringStatus = { show = mark }
  where
  mark : Status -> String
  mark Open = "[ ]"
  mark Done = "[x]"

instance toStringTodo : Show Todo
toStringTodo = { show = \t -> show t.status ^ " " ^ t.title }

toStringStatus comes before toStringTodo because a definition only sees the ones above it.

Lists

title : Todo -> String
title t = t.title

openTitles : List Todo -> List String
openTitles ts = List.map title (List.keepIf isOpen ts)

List.keepIf keeps the todos that are open, and List.map takes the title of each.