Printing and the Unit type
import Lait
#laitExpressions in Lait can do more than compute values; they can also do things via side effectful operations, such as printing.
To print things in Lait, we use the function print : String -> Unit. Here, Unit is a type in Lait that has exactly one value — written () —
which is used to represent the absence of a particular return value. Let’s see it in action:
#eval print "hello">> hello
When we sequence computations together using let, the side effects happen in order:
#eval let _ := print "hello" in print "world">> hello
If you click on “hello” in the above code snippet, you can see the rest of what is printed out.
(We use underscores in let to indicate that we don’t care about the value of the expression, since we know it will return ().)
Note that defs that contain side effects (such as print) are evaluated as soon as they are defined:
def myPrint := print "hello"…(In the textbook, you can see the print effects by hovering over the ... to the right of the definition.)
If we want to delay myPrint to only happen when we want it to, we want to make it a function. For this purpose, we can pass it a value of type Unit:
def myPrint' (u : Unit) := print "hello"
#eval myPrint' ()>> hello
Since we never care about the value of u, we have special syntax for arguments of type Unit:
def myPrint'' () := print "hello"
#eval myPrint'' ()>> hello
#eval myPrint'' ()>> hello