typed-racket-eff

8.16.0.1

typed-racket-eff🔗ℹ

dannypsnl

typed/racket + effect system, The project integrate an effect system into typed/racket.

1 Guide🔗ℹ

(effect log : (-> String Void))
(effect raise : (-> String Void))

(define/eff (f) : Void { raise log}
  (log "hello")
  (raise "failed")
  (log "world"))

(with-eff/handlers ([log (λ ([resume : (-> Void Void)]
                             [v : String]) : Void
                           (printf "~a~n" v)
                           (resume (void)))]
                    [raise (λ ([resume : (-> Void Void)]
                               [err : String]) : Void
                             (printf "got error: ~a~n" err))])
  (f))

where "world" will not get printed, this is because the handler of raise didn’t resume back to f, this is how the concept of exception get implemented in the effect handler system. If we remove [log ...] in with-eff/handlers, the type checker will complain

Type Checker: type mismatch; object lacks expected method ‘log’ in: (with-eff/handlers ((raise (λ ((resume : (-> Void Void)) (err : String)) : Void (printf "got error: ~a~n" err)))) (f))

as desired behaviour of an effect system.

1.1 Forward effect🔗ℹ

If you don’t want to handle an effect immediately, use #:forward (assuming f use log and raise)

(define/eff (g) : Void { raise}
  (with-eff/handlers ([raise #:forward]
                      [log (λ ([resume : (-> Void Void)]
                               [v : String]) : Void
                             (printf "log(g): ~a~n" v)
                             (resume (void)))])
    (f)))

The function g handle the log effect, and let f use it’s raise.

1.2 Finally🔗ℹ

Use #:finally handler to ensure something will run after body clause.

(effect fread : (-> Void String))

(define/eff (f) : Void { fread}
  (println (fread (void))))

(define in (open-input-file "file.rkt"))
(with-eff/handlers ([fread (λ ([resume : (-> String Void)]
                               [_ : Void])
                             (read-line in))])
  #:finally (λ () (close-input-port in))
  (f))

1.3 Higher-order effect🔗ℹ

The higher-order effect can be done by use Eff type and the effect object, then passing current effect object eff to the invoked function, but the API is still sharp, it’s easy to forget the pattern (λ (args ...) ((f args ...) eff)).

(effect number-to-string : (-> Number String))

(define/eff (f [x : Number]) : String { number-to-string}
  (number-to-string x))

(: emap : (All (I A B)
               (-> (-> A (Eff B I))
                   (Listof A)
                   (Eff (Listof B) I))))
(define (emap f l)
  (λ (eff)
    ({inst map B A} (λ (x) ((f x) eff)) l)))

(with-eff/handlers ([number-to-string
                     (λ ([resume : (-> String Void)]
                         [v : Number])
                       (resume (format "~a" v)))])
  (emap f
        (list 1 2 3)))

2 API🔗ℹ

syntax
(effect name : type)

Defines a new effect with name, and the type must be (-> A B), correspondings to handler with parameters resume : B -> Void and value : A. For example,

(effect raise : (-> String Void))

syntax
(effect-out name)
Provide the effect correctly, usage (provide (effect-out name)).

syntax
(Eff T (effs ...))

Decorate type T with effects, which will generate an arrow type that expected an effect object.

syntax
(effs ...)
Produce an Object where each method with an effect signature, this is the effect object type.

syntax
(define/eff (name [param : T] ...) : T_out { e* ...} body* ... body)

Equivalent to

(define (name [param : T] ...)
(with-eff : T_out { e* ...}
body* ... body))

syntax
(with-eff : T_out { e* ...} body* ... body)
Create a lambda with type (Eff T_out (effs e* ...)), and with body body* ... body, i.e.
(: (Eff T_out (effs e* ...)))
(lambda (eff) body* ... body)
This macro also bind a list of function to wrap eff object, e.g.
(define (raise err) (send eff raise err))
so you can invoke effect just like usual function.

syntax
(with-eff/handlers (handlers ...) body)

Execute body with effect handlers. For example,

(effect log : (-> String Void))
(effect raise : (-> String Void))

(define/eff (f) : Void { raise log}
  (log "hello")
  (raise "failed")
  (log "world"))

(with-eff/handlers ([log (λ ([resume : (-> Void Void)]
                             [v : String]) : Void
                           (printf "~a~n" v)
                           (resume (void)))]
                    [raise (λ ([resume : (-> Void Void)]
                               [err : String]) : Void
                             (printf "got error: ~a~n" err))])
  (f))

3 Limitation🔗ℹ

To generate proper call/prompt and abort/cc, every effect handler can only take one input type, so if you want to transfer several arguments, use structure to wrap them.