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.
Disciple is pure. This is argued in the first chapter of Ben Lippmeier's thesis: http://www.cse.unsw.edu.au/~benl/papers/thesis/lippmeier-imp...