Skip to content

Latest commit

 

History

History
95 lines (77 loc) · 2.63 KB

TODO.md

File metadata and controls

95 lines (77 loc) · 2.63 KB
Raw

TODO

Design

Circuits

  • Decide how to represent circuits, circuits with input and circuit-building computations. (Done: as in the paper)
  • Decide how programs are meant to be executed: from a starting circuit or standalone. Consequently, choose whether $Q$ should appear in the implementation of the language type system or not. (Done: the former)

Implementation

Wire language checking

  • Label pairs
    • Implementing
    • Testing
  • Implement sized lists of labels
    • Implementing
    • Testing

PQR Language checking

  • Language constructs

    • Boxed circuits and apply
      • Implementing boxed circuits
      • Testing boxed circuits
      • Implementing apply
      • Testing apply
    • Tuples and destructuring let
      • Implementing tuples
      • Testing tuples
      • Implementing destructuring let
      • Testing destructuring let
    • Abstraction and application
      • Implementing abstraction
      • Testing abstraction
      • Implementing application
      • Testing application
    • Lifting and forcing (aka linear boxing and unboxing of terms)
      • Implementing lift
      • Testing lift
      • Implementing force
      • Testing force
    • Return and sequencing let
      • Implementing return
      • Testing return
      • Implementing sequencing let
      • Testing sequencing let
    • Circuit boxing
      • Implementing box
      • Testing box
    • Lists and fold
      • Implementing lists
      • Testing lists
      • Implementing fold
      • Testing fold

  • Well-formedness constraints

  • Subsumption (e.g. ⊢ m : Circ 1 (Qubit,Qubit) ; 5 entails ⊢ m : Circ 2 (Qubit,Qubit) ; 8)

    • Decide whether to implement subsumption as a distinct case or within rules. Decided the former.
    • Implement subsumption
      • Implement subtyping
        • Interface with SMT solver

  • Instantiation (e.g. ⊢ f : List i Qubit -o [i,0] List i Qubit entails ⊢ f : List 3 Qubit -o [3,0] List 3 Qubit)

    • Implement instantiation

  • Unified syntax

    • AST
    • Type inference
    • Testing

  • Pattern matching

  • Better error messages

  • Better handling of shadowing

  • Better unification

Parser

  • Parsing wire bundles
  • Parsing indices
  • Parsing PQR
  • Better parser (e.g. solve postfix operators always requiring parentheses)
  • Top-level definitions

Performance

  • SMT solving with one file per program (as opposed to per query)
  • Use HashMap in place of Map

Examples

  • List functions
  • QFT
  • Arithmetic (adder)