Munus: A Language of Obligation

On the Design of a Type System in Which Values Owe Each Other Duties

Dr. Clara Hoffmann, Institut für Soziale Informatik, Technische Universität Wien

Acta Informatica Socialis, vol. 7, no. 2, 2026

1. Introduction

Type systems exist to prevent certain classes of error. A type annotation tells the compiler what a value is — integer, string, boolean, record — and the compiler ensures that values are used consistently with their types. An integer cannot be called as a function. A string cannot be divided by two. The type system is, in this sense, a system of classification: it assigns each value to a category and enforces the rules of the category.

Munus does not classify. Munus obligates.

Munus is a statically typed programming language in which types describe not what a value is but what a value owes. A value’s type is a set of obligations — duties it must fulfil toward other values it interacts with. When a value is passed to a function, it enters a relationship with the function’s other parameters, and this relationship carries reciprocal obligations that the type checker verifies at compile time. A value that fails its obligations does not produce a type error. It produces a breach, which is handled not by rejection but by a process the language calls adjudication, in which the compiler determines which party is at fault, what remedy is appropriate, and whether the relationship can be repaired.

The language was designed in 2022 by Prof. Johann Kreuter of the Technische Universität Wien, a computer scientist whose secondary appointment is in the Department of Sociology and whose intellectual debts, by his own account, are “half to Robin Milner and half to Max Weber.” The name is Latin — munus means obligation, duty, gift, and public office, a semantic range that Kreuter considers appropriate, since the language concerns itself with all four.

2. Origins

Kreuter’s career prior to Munus was in verification, specifically the formal verification of concurrent systems. His research focused on the problem of ensuring that multiple processes cooperate correctly — that messages are delivered, protocols are followed, resources are shared fairly. The standard approach uses session types, which describe the expected sequence of interactions between processes as a protocol. A process that deviates from the protocol is incorrect.

Kreuter’s dissatisfaction with session types was not technical but sociological. Session types model interaction as a protocol — a fixed sequence of steps that both parties agree to follow. But Kreuter, who had been reading Weber’s Economy and Society in a seminar he co-taught with a sociologist, noticed that the protocol model implicitly assumed a modern, bureaucratic, contractual relationship between processes — a relationship in which obligations are explicit, symmetric, and specified in advance.

This is not the only model. In Weber’s typology of social relations, contractual obligation is one possibility among several. There is also traditional obligation (I owe you because I have always owed you), charismatic obligation (I owe you because of who you are), and — most interesting to Kreuter — patrimonial obligation, in which duties flow from a relationship of personal dependence and are not specified in advance but emerge from the ongoing interaction. A vassal does not have a contract with a lord. The vassal has a relationship with the lord, and the obligations arise from the relationship’s history and context.

Kreuter’s 2021 paper, “Toward a Sociology of Types” (published in a workshop proceedings that the programming languages community ignored and the sociology community could not parse), proposed a type system modelled not on contracts but on social obligation. A value’s type would not be a fixed classification but a set of relationships with other values, each carrying obligations that were partly specified and partly emergent. The type checker would not verify that values are used consistently with a classification. It would verify that values fulfil their obligations to each other.

3. The Language

3.1 Obligation Types

In Munus, a type annotation does not say what a value is. It says what the value owes. The annotation x: owes(yield Int to consumer) declares that x is obligated to produce an integer when a value designated as its “consumer” requests one. The annotation f: owes(accept Pair from provider, yield Result to requester) declares that f is obligated to accept a pair from its provider and produce a result for its requester.

Obligations are always directed — owed to a specific other value — and they are always mutual. When x is passed to f, x acquires an obligation to f (to be a valid argument) and f acquires an obligation to x (to use x in a manner consistent with x’s own obligations). The type checker verifies that all obligations can be simultaneously satisfied.

A simple Munus programme:

let x: owes(yield Int to any) = 5
let y: owes(yield Int to any) = 10

fn add(a: owes(yield Int to add), b: owes(yield Int to add))
    -> owes(yield Int to caller) {
    a.fulfil + b.fulfil
}

let z = add(x, y)

The .fulfil method is how a value discharges its obligation. When a.fulfil is called inside add, the value bound to a produces the integer it owes. The type checker has verified, at compile time, that a is capable of fulfilling this obligation. The keyword any in x’s type means that x is willing to fulfil its obligation to any consumer. The keyword caller in the return type means the result is owed to whoever called the function. These are the language’s simplest relational modifiers. They become more complex.

3.2 Relational Modifiers

Obligations in Munus can be qualified with relational modifiers that describe the nature of the obligation, not just its content. The modifiers, drawn from Weber’s typology, are:

• contractual — the obligation is explicit, symmetric, and specified in advance. This is the default and behaves like a conventional type system.
• traditional — the obligation exists because the relationship has a history. A value that has been passed to a function repeatedly acquires a traditional obligation to that function, even if the obligation was not declared. The type checker infers traditional obligations from the programme’s structure.
• charismatic — the obligation exists because of a specific value’s properties. A value that is particularly well-suited to a function’s needs (e.g., an integer that is always within the expected range) acquires a charismatic relationship that gives it priority over other values of the same type.
• patrimonial — the obligation is asymmetric and emerges from a relationship of dependence. A value that was created by a function owes a patrimonial obligation to that function, and the function owes a patrimonial obligation of care to the value it created.

The modifiers affect how the type checker evaluates obligation fulfilment. A contractual obligation is strict: the value must produce exactly what was promised. A traditional obligation is lenient: the value should produce roughly what has been produced before, and minor deviations are tolerated. A charismatic obligation grants the value latitude to produce unexpected results, on the grounds that charismatic relationships are defined by the exceptional rather than the conventional. A patrimonial obligation is the most complex: it introduces a hierarchy between the values, in which the superior (typically the creating function) has both authority over and responsibility for the subordinate (the created value).

3.3 Breach

When a value fails to fulfil an obligation, the result is not a type error but a breach. A breach triggers the adjudication process, which is the compiler’s mechanism for determining fault and remedy.

Adjudication proceeds in three stages. First, the compiler identifies the breaching value and the obligation that was not fulfilled. Second, it determines fault — whether the breach was caused by the breaching value itself (it was incapable of fulfilment), by the value it owed the obligation to (it made an unreasonable demand), or by a third party (another value in the programme created conditions that made fulfilment impossible). Third, it determines a remedy.

Remedies in Munus are not rejections. The compiler does not refuse to compile a programme with a breach. Instead, it applies one of several remedial measures:

• coerce — the breaching value is converted to a type that can fulfil the obligation. This is the equivalent of implicit type coercion in conventional languages, but in Munus it is not automatic — it is a remedy applied after a finding of breach, and it is logged.
• substitute — a different value, one capable of fulfilment, is substituted for the breaching value. The compiler maintains a registry of values that have declared themselves available for substitution, and selects the most appropriate one.
• excuse — the obligation is forgiven. The breaching value continues without fulfilling it, and the compiler notes that the obligation was excused, not discharged. Excused obligations accumulate in a value’s record and affect its standing in future adjudications.
• sever — the relationship between the two values is terminated. The breaching value is removed from the function’s scope. This is the closest Munus comes to a type error, and it is rare.

The adjudication results are recorded in a file the compiler produces alongside the executable, called the Urteil (judgment). The Urteil lists every breach, every finding of fault, every remedy applied, and the compiler’s reasoning. Large programmes have long Urteils. The longest Urteil in the community’s records is 12,000 lines for a programme of 3,000, a ratio of four lines of judgment per line of code, which the community considers normal and outsiders consider alarming.

4. The Communal Type

The most distinctive feature of Munus is the communal type — a type that belongs not to a single value but to a group of values that share a set of mutual obligations. A communal type is declared by specifying the obligations that all members owe to each other:

community Workers {
    each owes(yield Status to all)
    each owes(accept Task from coordinator)
    coordinator owes(distribute Task to each)
    coordinator owes(yield Summary to observer)
}

This declares a community of values called Workers in which every member is obligated to report its status to all other members, every member must accept tasks from a designated coordinator, the coordinator must distribute tasks, and the coordinator must produce summaries for an observer. The type checker verifies that all communal obligations are satisfiable and that no member’s obligations conflict.

Communal types introduce a form of collective responsibility. If one member of a community breaches an obligation, the adjudication process considers not only the breaching member but the community as a whole: were the other members’ obligations compatible with the breach? Did the community’s structure contribute to the failure? Could the breach have been prevented by a different distribution of obligations?

This has the practical effect that adding a member to a community can cause the entire community to be re-adjudicated, since the new member’s obligations interact with everyone else’s. In large programmes with many communities, adding a single value can trigger a cascade of adjudications as the compiler works through the implications of the new relationship. The community calls this “the ripple,” and it is the primary source of long compile times in Munus. A programme with fifty communal types, each containing twenty values, takes approximately three minutes to compile. The Urteil for such a programme is typically around 8,000 lines.

5. The Standing Problem

A consequence of the adjudication system is that values in Munus accumulate a record: a history of fulfilled obligations, breaches, excused obligations, and remedies applied. This record affects how the compiler treats the value in future adjudications. A value with a clean record — one that has always fulfilled its obligations — is given the benefit of the doubt in ambiguous cases. A value with a history of breaches is scrutinised more closely.

The community calls this “standing,” and it is the language’s most controversial feature. Standing means that two values of the same structural type are not interchangeable if one has a better record than the other. A function that accepts an integer may prefer an integer with high standing over one with low standing, even though both are capable of producing the same result, because the high-standing integer has a history of reliable fulfilment.

In practice, standing produces a stratification of values. Well-behaved values are preferred. Poorly-behaved values are marginalised — passed to functions less often, substituted more readily, severed more quickly. A value that has been excused too many times acquires what the community calls “low standing,” and the compiler treats it with suspicion: adjudications involving low-standing values default to finding fault with the low-standing party unless evidence clearly indicates otherwise.

Kreuter describes standing as a natural consequence of a relational type system. “In any social system,” he has said, “actors who fulfil their obligations reliably acquire reputation. Actors who do not, lose it. If you model types as social relationships, reputation emerges whether you design it or not. I chose to design it, because the alternative is that it emerges anyway and you pretend it doesn’t.”

Critics — most vocally, a group at ETH Zurich led by Dr. Lena Ammann — have argued that standing introduces a form of systemic bias into the type system. A value that fails an obligation early in the programme’s execution acquires low standing that follows it for the remainder of the programme, making it more likely to be found at fault in future adjudications, which further lowers its standing. The cycle is self-reinforcing. Ammann’s 2025 paper, “On the Impossibility of Rehabilitation in Obligation-Typed Systems,” proved formally that a value whose standing falls below a threshold cannot recover through normal obligation fulfilment, because the compiler’s bias against low-standing values prevents it from being assigned obligations it could fulfil successfully.

Kreuter’s response was that the proof was correct and the phenomenon was a feature. “Some values,” he wrote, “are not suitable for the obligations they have been assigned. The type system discovers this through experience rather than declaration, which is more honest than rejecting them at the outset on the basis of a classification they had no part in choosing.”

Ammann’s response to the response was that “calling structural prejudice ‘honesty’ does not make it less prejudicial, but it does make it more Weberian.”

6. Forgiveness

In version 0.7, released in late 2024, Kreuter introduced a mechanism for resetting a value’s standing: the forgive keyword.

forgive x {
    -- x's standing is restored to neutral within this block
    -- obligations are adjudicated without reference to x's history
    -- if x fulfils its obligations, standing improves globally
}

The forgive block is the most debated construct in the language. Its proponents argue that it corrects the standing problem — it gives low-standing values an opportunity to demonstrate fulfilment without the burden of their history. Its critics argue that it undermines the entire point of standing, which is to encode the wisdom of experience into the type system. “If you can forgive at will,” Ammann wrote, “then standing is not a property of the value but a property of the programmer’s patience, which is a different thing and not one the type system should model.”

The deepest objection came from a doctoral student in Vienna named Felix Rainer, who argued that forgive introduced a category error. Obligation, in Weber’s framework, is a social relation. Forgiveness is a moral act. By introducing forgiveness into a system of social obligation, Kreuter had imported the language of individual moral agency into a framework that was designed to describe structural relations. “Munus was interesting,” Rainer wrote, “because it treated values as social actors embedded in relationships. forgive treats them as moral agents capable of redemption. These are not the same thing. You can forgive a person. You cannot forgive a role.”

Kreuter has not responded to this criticism directly. He has said only that forgive was “necessary,” that the alternative was a type system that converged inevitably toward rigidity, and that “a social system without the possibility of forgiveness is not a social system but a caste system, and I have read enough Weber to know the difference.”

7. Current Status

Munus has approximately 600 active users, a single compiler maintained by Kreuter’s research group in Vienna, and a community whose discussions are divided roughly equally between technical questions (how to structure obligations, how to manage standing, how to avoid adjudication cascades) and sociological questions (whether the type system is a model of society or a society in its own right, and whether the distinction matters).

The language has attracted interest from researchers in multi-agent systems, who recognise the obligation structure as a formalisation of agent-to-agent contracts and who have begun using Munus to model cooperative scenarios. It has also attracted interest from organisational theorists, who have noted that the communal type’s structure — roles, obligations, standing, adjudication — is isomorphic to a model of a small organisation, and who have published papers using Munus programmes as formal descriptions of organisational dynamics.

Kreuter is uncomfortable with the organisational interpretation. He insists that Munus is a programming language, not a theory of organisations. He compiles it. He benchmarks it (Munus programmes run approximately twenty percent slower than equivalent Rust programmes, a penalty attributable almost entirely to the standing system’s overhead). He files bugs. He is, he says, “a language designer who happened to read Weber, not a sociologist who happened to write a compiler.”

The community does not entirely believe him. The annual Munus workshop, held in Vienna, opens each year with a session titled “Is Munus a Language or a Polity?”, which Kreuter attends and at which he says the same thing — “It is a language” — and which the community receives with the same respectful scepticism. The session has never produced consensus, and the question has never been resolved, and the community has begun to suspect that the question’s irresolvability is itself a feature of the system, in the same way that certain obligations in Munus can be neither fulfilled nor severed but only carried, indefinitely, by values that did not choose them and cannot put them down.

The author thanks Prof. Kreuter for access to his research group’s internal documentation and for a series of conversations that were, in a manner consistent with the language he designed, both illuminating and obligating. Dr. Ammann provided a thorough and passionate account of her objections, for which the author is grateful and from which the author has not fully recovered. Felix Rainer’s criticism arrived after this paper was substantially complete but before the author had stopped thinking about it, which is to say it arrived at the worst possible time and was therefore maximally effective.