sigmal-docs

Sigmal Language Specification — Part 05

Abstractions: Functor, Applicative, Monad, and Effect Encoding

Top > Design docs > Core design > Part 05

---

1. Typeclasses as Records

In Sigmal, typeclasses are ordinary record types.

There is no special language-level typeclass mechanism.

Example: Functor

Functor =
  \ (F : $0 -> $0)
  = &{
    map :
      \ (A : $0)
        (B : $0)
        (f : A -> B)
        (x : F A)
      -> F B;
  };

An instance is simply a record value of this type.

There is:

• No implicit instance resolution
• No global instance registry
• No coherence rules

All dictionaries must be passed explicitly.

---

2. Applicative

Applicative =
  \ (F : $0 -> $0)
  = &{
    pure :
      \ (A : $0)
        (x : A)
      -> F A;

    ap :
      \ (A : $0)
        (B : $0)
        (ff : F (A -> B))
        (fa : F A)
      -> F B;
  };

Applicative is purely a structural interface.

---

3. Monad

Monad =
  \ (M : $0 -> $0)
  = &{
    pure :
      \ (A : $0)
        (x : A)
      -> M A;

    bind :
      \ (A : $0)
        (B : $0)
        (m : M A)
        (f : A -> M B)
      -> M B;
  };

There is no special syntax for do-notation in the core language.

Such sugar, if provided, must desugar to explicit bind usage.

---

4. Downcasting Between Abstractions

Because abstractions are ordinary records, conversion functions can be written explicitly.

Example:

monadToApplicative =
  \ (M : $0 -> $0)
    (mon : Monad M)
  = &{
    pure = mon.pure;

    ap =
      \ (A : $0)
        (B : $0)
        (ff : M (A -> B))
        (fa : M A)
      -> M B
      = mon.bind A B fa
        (\ (a : A) -> M B
          = mon.bind (A -> B) B ff
              (\ (f : A -> B) -> M B = mon.pure B (f a) )
        );
  };

No global coherence or collision issues arise because:

• No implicit selection occurs
• No overlapping instances are resolved automatically
• All dictionary passing is explicit

---

5. Generic Effect Encoding (Free Construction)

Sigmal does not bake effects into the language.

Effects are encoded purely via data types.

Operation Frame (Σ-pack)

OpFrame =
  \ (Op : $0 -> $0)
    (A  : $0)
  = #{
    Frame
      (X : $0)
      (op : Op X)
      (k  : X -> A);
  };

This packages:

• An operation op
• A continuation k
• An existential intermediate type X

---

Free Construction

Free =
  \ (Op : $0 -> $0)
    (A  : $0)
  = #{
    Pure(x : A);
    Op(frame : OpFrame Op (Free Op A));
  };

This encodes effectful programs as pure data.

A program written in this style:

• Does not execute effects directly
• Builds a tree of operations
• Is interpreted later

---

6. Handlers

A handler is a record type; a handler value is a record value of this type:

Handler =
  \ (Op : $0 -> $0)
  = &{
    handle :
      \ (X : $0)
        (op : Op X)
      -> X;
  };

Interpretation is explicit via a function such as:

runFree :
  \ (Op : $0 -> $0)
    (A  : $0)
    (h  : Handler Op)
    (p  : Free Op A)
  -> A;

The core language does not privilege any effect encoding.

---

7. Capability-Based Effects

An alternative to free constructions is capability passing.

Capabilities are explicit records:

Allocator =
  &{
    alloc : Nat -> Ptr;
    free  : Ptr -> Unit;
  };

Functions requiring allocation:

makeBuffer =
  \ (alloc : Allocator)
    (size  : Nat)
  = alloc.alloc size;

There is:

• No ambient world
• No implicit global allocator
• No hidden I/O

All operational power must be passed explicitly.

---

8. Effect System Direction

Sigmal’s core language does not include a built-in effect system.

Effects are modeled explicitly as:

• Free constructions
• Capability records
• Explicit state threading
• Structured data encodings

An optional future effect tracking system may:

• Annotate effect usage at the type level
• Remain explicit
• Avoid global inference
• Avoid implicit propagation

Such a system must preserve:

• Totality
• Explicit evidence discipline
• Determinism

---

9. No Built-In Law Enforcement

If algebraic laws are required (Functor laws, Monad laws, etc.), they must be represented explicitly.

Example:

Monoid =
  \ (A : $0)
  = &{
    empty  : A;
    append : A -> A -> A;
  };

If associativity or identity proofs are required, they must be encoded as additional fields.

The compiler does not assume algebraic laws.

---

10. Dictionary Passing and Specialization

Dictionary passing is explicit.

The compiler may optimize dictionary passing (e.g., specialization or inlining), but such optimization:

• Must not change semantics
• Must not introduce implicit resolution

All abstraction remains explicit at the language level.

---

11. Capabilities and Systems Programming

Because capabilities are explicit values, Sigmal supports:

• Freestanding environments
• Kernel development
• Sandboxed execution
• Deterministic embedded systems
• Controlled capability injection

There is no ambient authority.

---

12. Open Questions (Abstractions and Effects)

• Law encoding strategy (Functor/Monad laws in type system?)
• Effect tracking at the type level
• Ergonomic surface sugar for monadic sequencing
• Compiler specialization of dictionary passing
• Optimization of free constructions (fusion)
• Interaction between capability passing and effect encoding

---

13. Summary

Abstractions in Sigmal are:

• Structural
• Explicit
• Dictionary-passed
• Pure
• Total

Effects are:

• Not built into the core
• Encoded as data
• Interpreted explicitly
• Capability-driven

There is no:

• Implicit instance resolution
• Global registry
• Ambient effect system
• Hidden runtime mechanism

All higher-level abstraction arises from:

• Dependent functions
• Records
• Inductive types

---

Sigmal.org - the calculus we can build on

This site is open source. Improve this page.