Lesson 1.2: Basics of Functional K

In this lesson you will learn about basic K syntactic constructs, how to write simple K definitions, and how to compile and run them.

Your first K program

Now that you've installed K on your system, you're ready for your first program in K.

Copy the code below into your editor and save it as lesson-02-a.k. K files end with the .k extension.

k
module LESSON-02-A

  syntax Color ::= Yellow() | Blue()
  syntax Fruit ::= Banana() | Blueberry()
  syntax Color ::= colorOf(Fruit) [function]

  rule colorOf(Banana()) => Yellow()
  rule colorOf(Blueberry()) => Blue()

endmodule

Note that the name of the module and name of the file match. While the name of the module has to be written in capitals, the file name can have any capitalization. It is not a requirement that the file carries the module name, but merely a convention. If you choose to name your file differenly, you will need to compile it with attribute --main-module followed by the name of the module, to point the compiler to the main module of the definition. More about naming conventions and main modules will follow in Lesson 1.5.

Now, save the file and, from within the directory where you saved it, run:

kompile lesson-02-a.k

kompile is K's compiler. It takes a K definition and compiles it into an interpreter. Right now, you are compiling a single-file K definition, but we'll cover multiple-file K definitions later on.

You should get the following output:

[Warning] Compiler: Could not find main syntax module with name
LESSON-02-A-SYNTAX in definition.  Use --syntax-module to specify one. Using
LESSON-02-A as default.

It's a warning highlighting a K convention of splitting the syntactic definitions from the actual implementation into different modules. In Lesson 1.5 you will learn how to do it the proper way, as the examples will get bigger. For the smaller examples we work on now, we can just ignore it.

kompile will also output a directory containing everything needed to execute programs and perform proofs using the K definition given as input. Check your working directory and you'll see directory lesson-02-a-kompiled has beed created inside. If you're curious, have a look at its contents and inspect the generated documentation.

This directory not only contains all the basic tools produced by a K definition, e.g., parser, interpreter, or verifier, but also all sorts of files that can be used as input to execute these tools. More about K's parser will come in the next lesson, more on the other tools in due time.

Now, save the program below in the file banana.color in the same directory as lesson-02-a.k:

colorOf(Banana())

Note that we use color as file extension, but merely because this is the sort returned by function colorOf. The file name gives us a better understanding of what the file contains.

We can now evaluate this K term by running (from the same directory):

krun banana.color

krun is a tool which uses the interpreter generated by kompile to execute this program.

You should get the following output:

<k>
  Yellow ( ) ~> .K
</k>

For now, don't worry about the <k>, </k>, or ~> .K portions of this output file. We'll come back to them later.

You can also execute small programs directly on the command line instead of putting them in a file. For example, the same program above could have been executed by running the following command:

krun -cPGM='colorOf(Banana())'

Or by running the command below:

krun -cPGM='colorOf(Banana())' --definition 'lesson-02-a-kompiled'

-cPGM='colorOf(Banana())' simply sets variable PGM responsible for holding the program to execute to value colorOf(Banana()). Attribute --definition points to the directory containing the compiled version of LESSON-02-A.

Exercise

Use krun to compute the return value of the colorOf function on a Blueberry().

Structure of a K file

A K file consists of one or more modules, of which only one is the main one, in the sense that no other module defined in that file imports it. The name of this main module will also be the one given as argument to attribute main-module at compile time. Modules residing in other K files are imported instead through requires statements (similar to include in C/C++). You'll learn more about imports and requires in Lesson 1.5. In this lesson we continue with a closer look to a K module structure.

A K module is formed of sentences (and imports), and sentences come in different forms. For example, productions and rules are two types of sentences you have seen already in example lesson-02-a.k. We'll discuss each separately.

Productions, constructors, and functions

Productions are introduced with the syntax keyword and our first K module LESSON-02-A contains 5 productions defining sorts Color and Fruit. You can think of them as enums in C or data constructs in Haskell, although you'll find that they encompass other behaviors too.

Most of productions above are constructor productions (e.g., Yellow(), Blue(), or Blueberry()), while the last one is a function production (colorOf(Fruit) [function]). It's easy to distinguish the two as the latter production has additional attribute function. There are other types of productions—tokens, brackets, lists, macros, or aliases—but you'll learn about them in due time. There are other types of attributes too, and a sentence can carry several, in which case they will be separated by comma between square brackets. We will discuss them throughout the tutorial.

Constructors can have arguments, but these ones do not. We will cover the syntax of productions in detail in the next lesson, but for now, you can write a production with no arguments as an uppercase or lowercase identifier followed by the () operator. Sorts must always start with uppercase letter.

Returning to the syntax of a K module instead, note that individual productions of the same sort are separated by pipe operator |. For example, we can write an equivalent K definition of lesson-02-a.k as definition lesson-02-b.k as follows:

k
module LESSON-02-B

  syntax Color ::= Yellow()
  syntax Color ::= Blue()
  syntax Fruit ::= Banana()
  syntax Fruit ::= Blueberry()
  syntax Color ::= colorOf(Fruit) [function]

  rule colorOf(Banana()) => Yellow()
  rule colorOf(Blueberry()) => Blue()

endmodule

We can be even more compact, as in definition lesson-02-c.k:

k
module LESSON-02-C

  syntax Color ::= Yellow()
                 | Blue()
                 | colorOf(Fruit) [function]
  syntax Fruit ::= Banana()
                 | Blueberry()

  rule colorOf(Banana()) => Yellow()
  rule colorOf(Blueberry()) => Blue()

endmodule

You can try compiling and running both lesson-02-b.k and lesson-02-c.k to see that they produce the same output as lesson-02-a.k. If you run them from the same directory, remember to run with argument --definition to specify where the compiled version of the specific K definition is:

kompile lesson-02-b.k
krun -cPGM='colorOf(Banana())' --definition 'lesson-02-b-kompiled'

and

kompile lesson-02-c.k
krun -cPGM='colorOf(Banana())' --definition 'lesson-02-c-kompiled'

Rules, matching, and variables

We learned that functions are a type of productions carrying attribute function. However, the function production only introduces a specific function, it does not define it. For defining the behavior of a function in K, we use rules.

A rule begins with the rule keyword, which is followed by a left-hand side, rewrite operator =>, and a right-hand side. The left-hand side contains the name of the function and zero or more patterns corresponding to the parameters of the function. The right-hand side is another pattern. It specifies the function behavior for those parameters. Then, we can read the rule as follows: if the function is called with arguments that match the patterns on the left-hand side, then the function will return the value of the rewritten pattern on the right-hand side.

For example, in the above example, if the argument of the colorOf function is Banana(), then the return value of the function is Yellow().

Note that a function's definition can be expressed through several rules and that functions in K can be partial.

Let's add a new fruit constructor Kiwi() in lesson-02-d.k

k
module LESSON-02-D

  syntax Color ::= Yellow()
                 | Blue()
                 | Kiwi()
                 | colorOf(Fruit) [function]
  syntax Fruit ::= Banana()
                 | Blueberry()

  rule colorOf(Banana()) => Yellow()
  rule colorOf(Blueberry()) => Blue()

endmodule

and compile:

kompile lesson-02-d.k

You will notice that the new K definition compiled just fine. Now, execute the following:

krun -cPGM='colorOf(Kiwi())' --definition 'lesson-02-d-kompiled'

and observe the error:

[Error] krun: lesson-02-d-kompiled/interpreter 
/tmp/.krun-2025-04-14-20-41-45-bxhfwDNT0t/tmp.in.LwwPb4Jo9W -1 
/tmp/.krun-2025-04-14-20-41-45-bxhfwDNT0t/result.kore
colorOf ( Kiwi ( ) )

The function is undefined for this value, i.e., there is no rule for function colorOf whose left-hand side can be pattern-matched to Kiwi(), thus no right-hand side pattern either, and no output value.

We said that the left- and right-hand sides of a rule are patterns. Thus, constructors are a type of pattern. We will introduce more complex patterns later, but before we proceed to the next lesson, let us briefly discuss one more type of pattern—variables.

A variable, syntactically, consists of an uppercase identifier. It differs from a constructor in that it matches any pattern with one exception: two variables with the same name must match the same pattern.

Take the more complex example below (lesson-02-e.k):

k
module LESSON-02-E

  syntax Container ::= Jar(Fruit)
  syntax Fruit ::= Apple() | Pear()

  syntax Fruit ::= contentsOfJar(Container) [function]

  rule contentsOfJar(Jar(F)) => F

endmodule

Note that Jar is a constructor with a single argument. Multiple arguments are separated by comma.

In this example, F is a variable. It will match either Apple() or Pear(). The return value of the function is created by substituting the matched values of all of the variables into the variables on the right-hand side of the rule.

To demonstrate, compile this definition and execute the following program with krun:

kompile lesson-02-e.k 
krun -cPGM='contentsOfJar(Jar(Apple()))' --definition 'lesson-02-e-kompiled'

The program returns Apple(), because that is the pattern that was matched by F.

Exercise

Extend the definition of function colorOf in lesson-02-d.k to return a pattern for Kiwi().

Exercises

Extend the definition in lesson-02-d.k with the addition of blackberries. For simplicity, consider blackberries to be black and kiwis to be green. Then compile your definition and test that your additional fruits are correctly handled by the colorOf function.
Create a new definition which defines an outfit as a multi-argument constructor consisting of a hat, shirt, pants, and shoes. Define a new sort Boolean with two constructors, true and false. Productions for hat, shirt, pants, and shoes will have a single argument each—a color, either black or white. Then define an outfitMatching function that will return true if all the pieces of the outfit are the same color. You do not need to define the case that returns false. Execute your program on different values to see that your function behaves the way you expect.

Next lesson

Once you have completed the above exercises, you can continue to Lesson 1.3: BNF Syntax and Parser Generation.