Types and Functions
This section will very briefly go over types and functions. They will be explained much more thoroughly in later chapters.
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.