links icon indicating copy to clipboard operation
links copied to clipboard

Polymorphic operations

Open Orbion-J opened this issue 1 year ago • 0 comments

This branch supports the new syntax for handlers, operation types and allow to write polymorphic operations.

For this we have to annotate the cases in the handler with polymorphic operation types.

Example

sig h : (Comp(b, {A:forall a. (a) => a, Fail:forall a. a|c})) {A{_}, Fail{_}|c}~> Maybe(b)
fun h (m) {
    handle(m()) {
        case <A(x) => k> : (forall a.  (a) => a) -> k (x)
        case <Fail> : (forall a. () => a) -> Nothing
        case x -> Just(x)
    }
 }

sig f : () {A:forall a. (a) => a|_}-> Int
fun f () {
    if (do A(true)) do A(1) else
    do A(42)
}

This is done by having actual operation patterns and using the type annotation system associated with it.

PS: sorry again for the messy commits, I did not managed to get rid of them

Orbion-J avatar Jul 22 '22 14:07 Orbion-J