According to Sabry's criteria for pure languages:
1. it is a conservative extension of the simply typed λ-calculus.
2. it has a well-defined call-by-value, call-by-need, and call-by-name evaluation functions (implementations), and
3. all three evaluation functions (implementations) are weakly equivalent.
