Effects

examples/effects.sld:

;; Effect rows and handlers. `log` performs Log; a handler decides what
;; logging means, and the type system tracks which code may perform it.
(import
 (snail-core base)
 (snail-core io))

(effect Log
  ((log (-> String Unit))))

(: total-cost (-> (List I64) I64 ! Log))
(define (total-cost prices)
  (fold-left (lambda (total price)
               (log (string-append "adding " (show price)))
               (+ total price))
             0 prices))

;; The same function, quiet or verbose, depending only on its handler.
(: quietly (All (A e) (-> (-> A ! Log e) A ! e)))
(define (quietly action)
  (handle Log
      ((log (lambda (message) (unit))))
    (action)))

(display (quietly (lambda () (total-cost (list 3 4 5)))))
(newline)
(display (handle Log
             ((log (lambda (message) (write-line message))))
           (total-cost (list 1 2))))
(newline)

It prints:

12
adding 1
adding 2
3

A callback can use fewer effects than its caller has permission to perform. This function adds output around an action while preserving the action’s row:

(: announce (All (A e) (-> (-> A ! e) A ! console e)))
(define (announce action)
  (write-line "calling")
  (action))

The call to action uses e, which fits the surrounding console e for any substitution of e. Extra permissions do not authorize effects absent from the context, and unrelated quantified tails are not interchangeable. Function-type equality still compares complete rows; this inclusion rule applies when calling.