We propose a pair of linearly typed languages for describing quantum programs, with semantics given in terms of symmetric monoidal categories. The plain language corresponds to the familiar language of quantum circuits, and the annotated language features a modality that corresponds to timing, which lets us take into account how much time a gate takes when implemented. Well-typed programs are therefore guaranteed to be realizable physically.