Days of the Week

The following declaration tells Kind that we are declaring a new set of data - a Type.

type Day {  // Day is a Type
  monday    // Monday    is a Day
  tuesday   // Tuesday   is a Day
  wednesday // Wednesday is a Day
  thursday  // Thursday  is a Day
  friday    // Friday    is a Day
  saturday  // Saturday  is a Day
  sunday    // Sunday    is a Day
}

The type is called Day, and its members are Monday, Tuesday, Wednesday, etc. The <name> : <type> definition can be read as "name is a type". Above, we have both an example of creating a new Day : Type, and declaring an element of an existing type Wednesday : Day.

Now that we have defined what a Day is, we can write functions that operate using this type. Type the following:

NextWeekday (d: Day) : Day

This declares that we have a function called NextWeekday, which takes an argument called d, of type Day, and returns a Day. Continue defining the function as follows:

NextWeekday Day.monday      = ?
NextWeekday Day.tuesday     = ?
NextWeekday Day.wednesday   = ?
NextWeekday Day.thursday    = ?
NextWeekday Day.friday      = ?
NextWeekday Day.saturday    = ?
NextWeekday Day.sunday      = ?

Here, we are doing what we call pattern matching. We are declaring how the function should run for each possibility of the input d. It won't always be necessary to do this, as will be shown in examples later on.

Finally, complete the functions by writing what each one should return, and use spaces to style as you prefer:

NextWeekday Day.monday      = Day.tuesday
NextWeekday Day.tuesday     = Day.quarta
NextWeekday Day.wednesday   = Day.thursday
NextWeekday Day.thursday    = Day.sexta
NextWeekday Day.friday      = Day.monday
NextWeekday Day.saturday    = Day.monday
NextWeekday Day.sunday      = Day.monday

With the function finished, we can check its operation with some examples. The main way to do this in Kind is to create a Main function in your file and run it with the command kind2 run <file>.

For example, if you write the following Main and run the file:

Main {
  // Two workdays after Saturday
  NextWeekday (NextWeekday Day.saturday)
}

You should get something like:

(Day.tuesday)

Another way to test your code is to say what we expect the code to return, through a proof:

// // The third workday after a Monday is a Thursday
TestNextWeekday : Prop.Equal Day (NextWeekday (NextWeekday (NextWeekday Day.monday))) Day.thursday
TestNextWeekday = Prop.Equal.refl

The details of how proofs work will be explained later on. For now, what needs to be understood is:

  • We have the realization that (NextWeekday (NextWeekday (NextWeekday Day.monday))) is equal to Day.thursday
  • This realization was named TestNextWeekday
  • TestNextWeekday = Equal.refl says that the realization can be proven using only simplification on both sides.

To test that this proof (and any other proof going forward) is correct, you need to check the file using the command kind2 check <file>, which should return something like:

All terms check.