Skip to content

Linear types syntax: multiplicity annotation on records

Motivation

The linear types proposal describes how to extend the multiplicity annotations as in #18460 and #18461 (closed) to control the multiplicity of record fields.

The syntax is

data R = R { unrestrictedField # 'Many :: A, linearField # 'One :: B }

Proposal

I imagine the difficulty will be similar as in #18461 (closed) . A lot of places will simply be assuming that records have fields of multiplicity One. Though I'm a bit hopeful that we may mostly just need to follow the typechecker on this one.

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information