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

Algebraic effect constructs for Zilch #4

Open
3 tasks
Mesabloo opened this issue Sep 9, 2021 · 1 comment
Open
3 tasks

Algebraic effect constructs for Zilch #4

Mesabloo opened this issue Sep 9, 2021 · 1 comment
Labels
about: Zilch Anything about Zilch kind: todo Thins to do topic: grammar Grammar rules seem incomplete or missing topic: typechecking Typing rules are not well described or missing

Comments

@Mesabloo
Copy link
Member

Mesabloo commented Sep 9, 2021

To do:

  • Describe the syntax for handlers
  • Describe the syntax for effect declarations and applications
  • Create small type inference rules only for effects
@Mesabloo Mesabloo added topic: grammar Grammar rules seem incomplete or missing topic: typechecking Typing rules are not well described or missing about: Zilch Anything about Zilch labels Sep 9, 2021
@Mesabloo Mesabloo added the kind: todo Thins to do label Sep 10, 2021
@Mesabloo
Copy link
Member Author

The retained grammar for zilch effect constructs, as originally discussed in the linked discussion (at the bottom of the linked issue), is:

  • effect handlers (potentially parameterized):
    forall-quantification ::= '<' (id+ ':' kind | id)*_',' ('|' type+_',')? '>'
    
    handler ::= 
      'handler' id forall-quantification? ('(' (id (':' type)?)*_',' ')')? ':=' { handler-branch+_; }
    handler-branch ::= 'return' id ('->' | '') expr
                     | id '(' id*_, ')' ('->' | '') expr
  • effect declarations:
    effect ::= 'effect' id ('(' id*_',' ')')? ':=' { (id ':' type)*_; }
  • effectful functions
    effect-row ::= '{' type*_',' ('|' id+_',')? '}'
    arrow-type ::= type-atom effect-row? ('->' | '') type
                 | '(' type+_',' ')' effect-row? ('->' | '') type
    where type-atom is specifically defined not to include some types (e.g. arrow-type) and -> is equivalent to {}->

  • x*_s is a shortcut for (x (s x)*)?
  • x+_s is a shortcut for x (s x)*

@Mesabloo Mesabloo moved this to In Progress in Issue tracker Nov 1, 2021
@Mesabloo Mesabloo moved this from In Progress to Todo in Issue tracker Sep 20, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
about: Zilch Anything about Zilch kind: todo Thins to do topic: grammar Grammar rules seem incomplete or missing topic: typechecking Typing rules are not well described or missing
Projects
Status: Todo
Development

No branches or pull requests

1 participant