Tricks

A mark before a task type's parameter filters the tasks it takes idea

(fixed T) -> Y against (T) -> Y, and (bind T) -> Y against (T) -> Y.

The idea

A task's type says how each parameter is given (see Tasks as values). The trick is that a mark before the type of a parameter, fixed or bind, does not make another type of value: (int) -> int and (fixed int) -> int are the same type, as bind x: int and fixed x: int are of one type, and differ only in what may be done with the name. The mark filters. Where a place wants a (fixed int) -> int, a task that changes its parameter is refused, and every task that doesn't is taken. Where the place wants a plain (int) -> int, every task is taken, the ones the mark would refuse too. So the plain type accepts all that the marked one accepts and more, and the mark is a way to narrow the input range on purpose: a tricky filter, not a new kind of thing.

The marks are ordered by how much of the parameter a task may change, and each accepts what the ones after it do:

Reading it by rows or by columns says the same thing twice. (fixed T) is the narrowest input range, the tasks that leave their parameter alone; (bind T) widens it by the tasks that change only its contents; the plain type takes every task. The two differences the idea asks for are the first and the second column against the first: (fixed T) -> Y against (T) -> Y, and (bind T) -> Y against (T) -> Y. The two marked types also differ from each other, by the bind x: T row.

On a whole value

A whole value is copied, so what a task does to its own copy is invisible to the caller, and the plain type needs no filter for the caller's sake. The mark is for whoever writes the type: it says that the tasks given here never change what they are handed, even their own copy, which a reader of the type sees without opening them.

task reads(n: int) -> int
    <- n + 1
fi

task counts_down(flex n: int) -> int      ; changes its own copy of n
    flex steps = 0
    loop n > 0
        n = n - 1
        steps = steps + 1
    fi
    <- steps
fi

fixed a: (int) -> int = reads              ; taken
fixed b: (int) -> int = counts_down        ; taken: a plain type takes every task
fixed c: (fixed int) -> int = reads        ; taken
fixed d: (fixed int) -> int = counts_down  ; the idea: refused, counts_down changes n

On a type with no contents, a number say, bind acts as fixed everywhere in Vela, so (bind int) -> int and (fixed int) -> int would filter alike. The two marks part ways on a value that has contents, a shape or an array, whose fields a bind task may change in its own copy:

shape Point
    x: int
    y: int
fi

task shifts(bind p: Point) -> int     ; changes a field of its copy
    p.x = p.x + 1
    <- p.x
fi

task moves(flex p: Point) -> int      ; assigns its copy whole
    p = Point { x: p.x + 1, y: p.y }
    <- p.x
fi

fixed e: (Point) -> int = moves               ; taken
fixed f: (bind Point) -> int = shifts       ; taken
fixed g: (bind Point) -> int = moves        ; the idea: refused, moves assigns p whole
fixed h: (fixed Point) -> int = shifts      ; the idea: refused, shifts changes a field

On a twofold value

Here the filter matters to the caller too. A slice, a map and a pointer are twofold: a task's copy of one names the caller's items, so a task that changes them changes what the caller sees. Narrowing the input range is then a promise about the caller's data:

task total(xs: [int]@r) -> int            ; reads the items
    flex sum = 0
    each x in xs
        sum += x
    fi
    <- sum
fi

task zeroes(bind xs: [int]@r) -> int    ; writes items, keeps the length
    each i in 0..xs.len
        xs[i] = 0
    fi
    <- xs.len
fi

task drain(flex xs: [int]@r) -> int     ; takes items out
    flex sum = 0
    loop xs.len > 0
        sum += xs.del()
    fi
    <- sum
fi

task report(look: (fixed [int]@r) -> int, xs: [int]@r)
    show(look(xs))
fi

report(total, scores)        ; taken
report(zeroes, scores)       ; the idea: refused, zeroes changes the items it is given
report(drain, scores)        ; the idea: refused, drain changes them too

What it is for

• A promise a reader sees in the type. A task taking a callback marked fixed tells whoever calls it that the callback leaves what it is given alone, without opening the callback, and tells whoever writes the callback what it may not do.
• Handing out read-only data safely. A call through a (fixed T) -> Y cannot change what it is given, so such a call may be given what a fixed name owns (see What a fixed name owns), which a call through a type that may change it never is. The mark is what buys that, as the plain type may not.
• Checkers, validators and observers. A task that looks at data to decide or log something has no business changing it; the mark makes the type say so.
• Middle ground. (bind T) allows a callback that fixes up items in place, zeroing them or sorting them, and still refuses one that grows the slice, takes items out, or replaces a value whole, so the caller's length and place stay as they were.
• A plain type for everything else. A place that takes a callback it will call on its own copies, and doesn't care what the callback does to them, writes the plain type and takes every task.

How one limits the input range

The author of a type chooses the range by the mark written, from the widest to the narrowest:

1. (T) -> Y: every task with that parameter.
2. (bind T) -> Y: no task that assigns the parameter whole, or, on a twofold value, adds or takes out items of its copy.
3. (fixed T) -> Y: only tasks that change nothing of the parameter, not its contents either.

A range is only ever narrowed, never widened: a value of the narrower type goes where the wider is expected, as a (fixed T) -> Y task goes where (T) -> Y is, and never the other way. A task is held by the type it was given, so one stored in a (T) -> Y variable, which may hold a task that changes, is refused where a (fixed T) -> Y is wanted.

Where it stands today built

Tested on commit f44da22, with the release compiler. The idea is not built as described, in either of its two differences:

• On a whole value, no filter at all. fixed, bind and flex before the type of a value copied whole read as nothing: (fixed int) -> int, (bind int) -> int, (flex int) -> int and (int) -> int are one type, and each takes reads and counts_down alike. The marks are allowed, and filter nothing (see A value the task changes through).
• On a twofold value, the filter exists with the plain type as its narrowest end. (fixed [int]@r) -> int is the same as ([int]@r) -> int, and both take only a task that reads. (bind [int]@r) -> int takes tasks that read or are written bind, and (flex [int]@r) -> int takes every task. So the order is the idea's turned about: today the plain type is the strictest and flex the widest, where the idea has the plain type the widest.

That is the rule the safety page and the language reference describe, and the owner rule depends on it: a call through a type that may change what it is given is never given what a fixed name owns.

What building it would take

• The fit of one task type to another (task_fits, taken_for and fits_regions in src/check.rs) would order the three marks, as KeptMode orders a lambda's, and keep the mark on a whole value instead of reading it as nothing. The value stays of one type, as the author says; what travels with it is how much of its parameter the task may change, so a narrower one goes where a wider is expected and not back.
• A call through a type is checked as a call of a task with that parameter, as today, so the owner rule would have the plain type behave as flex does now (nothing a fixed name owns is given to it) and the fixed mark behave as the plain type does now.
• Messages, hover and completion in Vela Studio, the run tests and fail fixtures for each cell of the tables, and an example, as for any feature.

Questions for the author open

1. The twofold order. The idea makes the plain type the widest. Today the plain type is the strictest on a twofold value, and flex is the widest mark. Is the plain type to become the widest, so a task that changes a slice's items now needs (flex [int]@r) and would then be taken by ([int]@r) (breaking, as every program that writes a plain type for a reading callback would take changing ones too)? Or does the filter apply only on a whole value, and the twofold rule stay as it is?
2. The fate of flex in a task's type. If the plain type becomes the widest, (flex T) would say what (T) says. Is it dropped, kept as a synonym, or kept to mean a task that changes?
3. Same type, shown the same. Is the mark part of how a type is written, so .type and messages show (fixed int) -> int for one, or does a value show the plain type, and may a (fixed int) -> int value be compared with == with a (int) -> int one?
4. Other places that take a task. The same filter on a lambda's type, a wrapper's next, and a type group's task, (fixed P...) -> R?
5. A generic parameter. (fixed T) -> Y in a task that takes types, where T may be a whole value or a twofold one: the same rule for the type each copy is given?

Adding to this page

An entry names the trick, says what it filters or limits, shows it on a small program, says what it is for, and says where it stands in the compiler today, tested. When a trick is built, its entry says so, and links to where the guide explains it.