I have to wonder if it might not be sufficient to have Bra and Ket types and allow their composition in various ways. Writing Bra(ϕ) and Ket(ψ) and Bra(ϕ)*Ket(ψ) or BraKet(ϕ,ψ) doesn’t seem like the end of the world. The ⟨ϕ|ψ⟩ notation is cool but it doesn’t seem strictly necessary to have a quantum mechanics DSL. If one absolutely must have something like the traditional bra-ket notation, then I think you need dedicated versions of | for bra, ket and bra-ket combinations. Perhaps ⟪ϕ⟧ and ⟦ψ⟫ and ⟪ϕ,ψ⟫.
1 Like