Lazy evaluation

The whole language is lazily evaluated. The only thing evaluated strictly is the main function.

Expressions are only evaluated when patternmatched on. If you don't try to match on something, it will never be evaluated. To evaluate an expression, it is rewritten until it starts with a data constructor or a lambda.

type nat contains
    one
    succ nat

define big_nat of_type nat as succ big_nat

type tuple_of_nats contains                              
    tuple nat nat                                        
                                                         
define is_equal of_type fn nat fn nat bool as            
    lambda x lambda y match tuple x y with               
        tuple one    one     to true                     
        tuple succ a succ b  to is_equal a b             
        _                    to false                    

The nat type is a recursive datastructure. one = 1, succ one = 2, succ succ one = 3, and so on. big_nat is an infinitely large value but we can work with it because it's lazy. is_equal recursively checks if two nats are equal. Let's look at some examples and their outputs.

is_equal                                             
    succ succ one                                    
    succ succ one                                    

-- true

is_equal                                             
    succ succ one                                    
    succ succ succ one                               

-- false

is_equal                                             
    succ succ succ one                               
    big_nat                                         
                                                         
-- false

is_equal big_nat big_nat                           

-- *hangs at runtime*

This program hangs because is_equal never reaches its base case and loops forever. Note that despite working with two infinitely large values and is_equal being recursive, the program doesn't eat any memory while evaluating it.

is_equal                             
    succ succ one                                    
    succ succ succ succ ...   

-- false

... is syntax for undefined. It can be used anywhere in place of an expression. It's useful for unfinished or unreachable code.

is_equal                                             
    succ succ succ one                               
    succ succ ...                                    

-- *runtime error*

If you try to evaluate undefined, you'll get a nice runtime error showing which undefined got evaluated.