[note: I know several languages can capture *some* of these ideas, and anything with higher-order functions can *express* them, but I'm looking for one where an idea like "follower" or "most valuable" can be captured with an explicit definition or annotation rather than (for example) a Dafny invariant]

[note2: many languages have built-in support for some of Sajaniemi's roles (e.g., 'const'), but I'm looking for one that will let me define new roles in the same way that I can define new types.]

@gvwilson Haven't read your above article, but I'd say that in languages, like Prolog, which is usually not typed, and has both a notion of failure and a separate notion of error/exception, when you add a type system it's often _descriptive_ rather than _prescriptive_, which seems related to the question you're asking…

The question being how would you want to type:
```
append([], L, L).
append([H|T], L, [H|M]) :- append(T, L, M).
```
since the first clause would _succeed_ with any `L`.

@gvwilson Wouldn‘t an „Iterator“ type fit that description? A couple of languages have those.

Swift has a few more types that go in that direction of „how it‘s used“ but often not on the same level of simplicity as in Sajaniemi‘s variable roles.

Here are some that I think go in that direction and that exist in Swift:

- Sequence and Collection: protocols in Swift
- ~Copyable: a value that cannot be copied, so a move-only type: only one object can hold onto it at a time
- Mutex: used to wrap other values in it, to prevent concurrent access/modification of the wrapped value in a concurrent program
- actor: a keyword-level type in Swift. Used to protect state and then „act“ on it in a concurrency-safe manner. Some parallels to Mutex, but a lot more complexity around it. Ensures modifications to the state are serialized (instead of happening concurrently) but doesn‘t block like a Mutex.
- the `let` keyword basically captures the „fixed value“ concept. However there are subtle differences between using it for value types and for reference types.
- the Result type holds the result of a computation that may have gone wrong

@gvwilson In functional programming you can abstract over patterns like that. For example, the `foldMap` function traverses a structure and collects all the elements according to some given mapping function and the monoid structure on the result, like how you'd use a gatherer variable in imperative languages.

Another thing that comes to mind are effect systems. The Writer effect is much lik a gatherer variable, for example. If you can define custom effects, you can separate uses of mutation.

@gvwilson my brain says something something intrinsic vs extrinsic typing (https://ncatlab.org/nlab/show/intrinsic+and+extrinsic+views+of+typing) for the conceptual aspect

and for something more like what a programming language offers would be parametric polymorphism aka type classes where “what” you act on doesn’t matter but you have capabilities that limit/define the operations on it