Types and Functions

This section will very briefly go over types and functions. They will be explained much more thoroughly in later chapters.

dragon animation

Let's write a program to do some basic boolean logic, starting with the boolean type.

type bool contains
    true
    false

This created the bool type and the values true and false. true and false are called data constructors because they're used to construct a value of type bool. Thus, the types of true and false are bool.

Now let's write the not function that takes a bool and returns a bool.

define not of_type fn bool bool as lambda x match x with
    true  to false
    false to true

Let's break down what's going on here. Variables are defined with the syntax

define NAME of_type TYPE as EXPRESSION

In this function, the input bool is captured by the lambda and placed in the x variable. Then, x is matched on to return the corresponding bool. The type of not is fn bool bool because not is a function from a bool to a bool.

To test the code, write the main function and execute the file.

define main of_type bool as not true
~/code$ thorn bool.th
false

Success! not true is indeed false. Now let's write the slightly harder or function. or takes two bools and checks if either of them are true. But how can we write a function that takes multiple arguments?

As seen before, a function is really just a lambda expression with a name. However, if you know anything about lambda calculus, A lambda takes and returns only a single value. The trick is to take the first argument and return a function. That returned function will then take the second argument and return the final value. So the type of or would be fn bool fn bool bool, a function from a bool to a (function from a bool to a bool). Types don't have paranthesis because they use polish notation. Here's the final function.

define or of_type fn bool fn bool bool as 
    lambda a lambda b match a with 
        true  to true
        false to b

And here's the and function, slightly different from or.

define and of_type fn bool fn bool bool as 
    lambda a lambda b match a with 
        true  to b
        false to false

As you can see, the lambda expression is capturing an argument and returning a different lambda expression. A benefit of doing it this way is currying. or true false is of type bool, but or true is of type fn bool bool. It is a partially applided function.

Now, to get to the point, here's a somewhat complicated expression written in C. Note all those pesky paranthesis and infix/prefix operators.

!((true && false) || (!(true || true) && !false)) 

And here's that same expression rewritten in thorn with our functions

not or and true false and not or true true not false

Pretty cool if i do say so myself. How is this possible? Polish notation. The types of all values are known at the time of parsing and polish notation is used to group values by their types. In fact, paranthesis and any other operators or special characters are outright prohibited in thorn.

Back Next