Algebraic Effects¶
Operation, EffectSignature, Handler, FreeMonad, Plotkin-style effect signatures with handler-based interpretation.
algebraic
¶
Algebraic effects + handlers.
Following Plotkin & Power and Bauer & Pretnar, exposes a free-monad-
over-signature construction so any user-defined effect signature
induces a Monad instance automatically. Handlers translate
a free-monad computation into a target monad's effects.
The free-monad carrier Free_Σ^{≤d}(A) is realised as a flat
FinSet whose flat-index layout is:
- Indices
[0, |A|)represent leaf nodesleaf(a). - For each operation
op_i(in declared order), a contiguous block of|op_i.parameter| · |Free^{d-1}(A)|^{|op_i.result|}indices represents operation nodesop_i(p, k)wherepis a parameter andkis a deterministic continuationop_i.result → Free^{d-1}(A).
The flat-FinSet representation avoids the CoproductSet
auto-flattening collision that would otherwise dissolve the
recursive leaf-vs-operation distinction when A is itself a
coproduct. Structural decomposition is recovered from
signature + depth rather than from the carrier object.
Handler interpretation walks the flat-index decomposition in
post-order: leaves are routed through return_clause and
operation nodes through operation_clauses.
References
- Plotkin, G. and Power, J. (2003). Algebraic operations and generic effects. Applied Categorical Structures, 11(1), 69–94. doi:10.1023/A:1023064908962.
- Bauer, A. and Pretnar, M. (2015). Programming with algebraic effects and handlers. Journal of Logical and Algebraic Methods in Programming, 84(1), 108–123. doi:10.1016/j.jlamp.2014.02.001.
Operation
¶
EffectSignature
¶
Bases: Model
A signature of effect operations.
Realisable both as a Python value (a tuple of operations) and as
a panproto.Theory whose sorts are SetObject and
whose operations are the listed Operation instances.
| ATTRIBUTE | DESCRIPTION |
|---|---|
name |
Signature name; appears in panproto theory naming.
TYPE:
|
operations |
The operations comprising the signature.
TYPE:
|
to_theory
¶
to_theory() -> object
Realise this signature as a panproto Theory.
| RETURNS | DESCRIPTION |
|---|---|
Theory
|
The theory whose single sort is |
Source code in src/quivers/monadic/algebraic.py
86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 | |
Handler
¶
Bases: Model
Interpretation of a free-monad computation in a target monad.
A handler supplies a clause for each operation in its signature
plus a return-clause that lifts plain values into the target
monad. run folds a bounded-depth signature tree by
interpreting each leaf through return_clause and each
operation node through operation_clauses.
Operation-clause shape: for an operation op whose result feeds
a continuation k : op.result → target(B), the clause has
signature op.parameter × [op.result → target(B)] → target(B).
The implementation translates each free-monad operation node's
continuation (a function-space flat index into the inner-tree
carrier) into the corresponding target-side function-space
continuation by recursive descent, then routes through the clause.
| ATTRIBUTE | DESCRIPTION |
|---|---|
signature |
The effect signature this handler interprets.
TYPE:
|
target |
The target monad in which the operations are realised.
TYPE:
|
return_clause |
TYPE:
|
operation_clauses |
For each
TYPE:
|
as_theory_morphism
¶
as_theory_morphism() -> object
Realise this handler as a panproto theory morphism.
The morphism's domain is signature.to_theory(); its
codomain is the target monad's panproto theory.
Source code in src/quivers/monadic/algebraic.py
289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 | |
run
¶
Apply this handler to a free-monad computation up to depth.
Returns a morphism Free_Σ^{≤depth}(A) → target(A).
The construction proceeds by induction on the tree depth:
leaves are routed through return_clause; each
operation node is decomposed into its parameter and
continuation components, the continuation is recursively
interpreted into the target monad, and the result is fed
through the corresponding operation-clause morphism.
Source code in src/quivers/monadic/algebraic.py
329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 | |
FreeMonad
¶
Bases: Model
The free monad over an effect signature with a depth bound.
FreeMonad(sig, depth) carries the bounded-depth signature-tree
construction. Its typeclass instance methods are concrete
V-relation morphisms over the flat-FinSet carrier.
| ATTRIBUTE | DESCRIPTION |
|---|---|
signature |
The signature whose free monad this is.
TYPE:
|
depth |
The depth bound for the operation-tree carrier.
TYPE:
|
pure
¶
pure : A → Free^d(A) is the leaf injection.
Source code in src/quivers/monadic/algebraic.py
459 460 461 462 463 464 465 466 467 468 469 | |
fmap
¶
Lift f : A → B to Free^d(f) : Free^d(A) → Free^d(B).
Acts as f on the leaf summand and recursively as
Free^{d-1}(f) on each operation's continuation slots.
Each operation node's continuation function-space is re-encoded
through the recursive fmap's deterministic image.
Source code in src/quivers/monadic/algebraic.py
471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489 490 491 492 493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508 509 510 511 512 513 514 515 516 517 518 519 520 521 522 523 524 525 526 527 528 529 530 531 532 533 534 535 536 537 | |
join
¶
join : Free^d(Free^d(A)) → Free^d(A) via tree splicing.
Splices outer trees: an outer-leaf carrying an inner tree
produces that inner tree directly; an outer-operation node
op(p, k) produces op(p, k') where each continuation
slot is the recursive join of the corresponding outer
subtree. Truncation at depth d is enforced by recursive
descent: outer ops at depth d produce inner ops whose
sub-trees come from depth-d-1 recursion.
Source code in src/quivers/monadic/algebraic.py
539 540 541 542 543 544 545 546 547 548 549 550 551 552 553 554 555 556 557 558 559 560 561 562 563 564 565 566 567 568 569 570 571 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587 588 589 590 591 592 593 594 595 596 597 598 599 600 601 602 603 604 605 606 607 608 609 610 611 612 613 614 615 616 617 618 619 620 621 622 623 624 625 626 627 628 629 630 631 632 | |
bind
¶
bind(m, k) = join_B ∘ Free^d(k)(m).
Source code in src/quivers/monadic/algebraic.py
634 635 636 | |
apply
¶
apply : Free^d([A → B]) ⊗ Free^d(A) → Free^d(B).
Derived from lift_a2 and the function-space evaluator.
Source code in src/quivers/monadic/algebraic.py
638 639 640 641 642 643 644 645 646 | |
lift_a2
¶
lift_a2(f) : Free^d(A) ⊗ Free^d(B) → Free^d(C).
Recursive definition (the standard free-monad applicative):
liftA2(f)(leaf(a), leaf(b)) = leaf(f(a, b)).liftA2(f)(op(p, k), n) = op(p, λr. liftA2(f)(k(r), n)).liftA2(f)(leaf(a), op(p, k)) = op(p, λr. liftA2(f)(leaf(a), k(r))).
The recursion descends one depth at a time on the side carrying
the operation, while the other side stays at its current
depth. Sub-results are produced in
:math:\mathrm{Free}^{\max(d_a, d_b) - 1}(C) and re-encoded
into the parent's op-summand continuation slots through the
appropriate sub-carrier function-space cardinality. Truncation
is enforced uniformly when the output depth would exceed the
bound d: such sub-results are dropped, preserving the
bounded-depth contract.
Source code in src/quivers/monadic/algebraic.py
648 649 650 651 652 653 654 655 656 657 658 659 660 661 662 663 664 665 666 667 668 669 670 671 672 673 674 675 676 677 678 679 680 681 682 683 684 685 686 687 688 689 690 691 692 693 694 695 696 697 698 699 700 701 702 703 704 705 706 707 708 709 710 711 712 713 714 715 716 717 718 719 720 721 722 723 724 725 726 727 728 729 730 731 732 733 734 735 736 737 738 739 740 741 742 743 744 745 746 747 748 749 750 751 752 753 754 755 756 757 758 759 760 761 762 763 764 765 | |