dannypsnl / typed-racket-eff

typed/racket + effect system
https://pkgs.racket-lang.org/package/typed-racket-eff
Other
8 stars 0 forks source link

higher order #5

Closed dannypsnl closed 2 weeks ago

dannypsnl commented 2 weeks ago

An effect type must be provided, e.g.

(Eff A { log })
= (-> (Object (log (-> String Void))) A)

This equation defines the type Eff, but we cannot simply use define-type because need to lookup effect log to know the signature of Object; so alternative I thought a macro

(eff/signature { log raise })
= (Object (log (-> String Void))
          (raise (-> String Void)))

can be useful, then type of map can use polymorphism of typed/racket, belike:

(All (O)
  (-> (A -> Eff B O)
      (List A)
      (Eff (List B) O)))
(define ((emap f l) eff)
  (map (lambda (x) ((f x) eff)) l))
dannypsnl commented 2 weeks ago
(define/eff (f [msg : String]) : Void { log }
  (log msg))

(: emap : (All (I)
               (-> (-> String (-> I Void))
                   (Listof String)
                   (-> I Void))))
(define (emap f l)
  (λ (eff)
    (map (λ ([x : String]) ((f x) eff))
         l)
    (void)))

(with-eff/handlers ([log (λ ([resume : (-> Void Void)]
                             [msg : String])
                           (printf "~a~n" msg)
                           (resume (void)))])
  (emap f '("hi" "ho" "ha")))

This one success, output

hi
ho
ha