Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

effect syntax: effect patterns as computation patterns #13135

Open
wants to merge 1 commit into
base: trunk
Choose a base branch
from

Conversation

Octachron
Copy link
Member

This PR is meant to be read at the top of the effect-syntax PR(#12309). In particular, only the last commit is new.

This commit aims at making the typechecker part of the effect syntax changes smaller.
This is done by merging back effect patterns into the computation pattern umbrella in the typechecker part of the compiler. Splitting patterns by kind is then done when compiling to the lambda IR.

This change also has the advantage of making the error messages for non-toplevel computation patterns more uniform:

let f [effect _, _] = ()

Error: Effect patterns are not allowed in this position.

let g [exception _ ] = ()

Error: Exception patterns are not allowed in this position.

Incidentally, it makes the compiler support cases containing mixed effect, exception and value cases:

let catch f = match f () with _  | exception _ | effect _, _ -> ( )
type _ Effect.t += A: unit Effect.t
type _ Effect.t += B: unit Effect.t

let () = catch ignore; catch (fun () -> raise Not_found); catch (fun () -> Effect.perform A)

However, the feature is mostly useless, since effect types require type equations to be useful, and we discard type equations introduced under or-patterns. In other words, it is impossible to bind the continuation in the pattern above:

let test f = match f () with k | effect A, k -> ()
Error: The variable k on the left-hand side of this or-pattern has type 'a
      but on the right-hand side it has type (%eff, 'b) continuation
      The type constructor %eff would escape its scope

@Octachron Octachron mentioned this pull request Apr 29, 2024
9 tasks
@gasche gasche added the typing label May 15, 2024
At the typechecker level, effect cases are similar to the other
computation patterns. This commit refactorize the parsing and
typechecking of effect cases to fully fall in the computation pattern
category
@Octachron Octachron force-pushed the effect-pattern-as-computation-pattern branch from e50ee90 to aa28263 Compare May 15, 2024 15:43
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

3 participants