Linear Dependent Type Theory for Quantum Programming Languages