Skip to content
Snippets Groups Projects
abstract.tex 2.04 KiB
Newer Older
  • Learn to ignore specific revisions
  • Dan Licata's avatar
    Dan Licata committed
    Gradually typed languages are designed to support both dynamically typed
    and statically typed programming styles while preserving the benefits of
    each.  While existing gradual type soundness theorems for these
    
    Dan Licata's avatar
    Dan Licata committed
    languages aim to show that type-based reasoning is preserved when
    
    Dan Licata's avatar
    Dan Licata committed
    moving from the fully static setting to a gradual one, these theorems do
    not imply that correctness of type-based refactorings and optimizations
    is preserved.  Establishing correctness of program transformations is
    technically difficult, because it requires reasoning about program
    equivalence, and is often neglected in the metatheory of gradual
    
    languages.  
    
    In this paper, we propose an \emph{axiomatic} account of
    
    Dan Licata's avatar
    Dan Licata committed
    program equivalence in a gradual cast calculus, which we formalize in a
    logic we call \emph{gradual type theory} (GTT). Based on Levy's
    call-by-push-value, GTT gives an axiomatic account of both call-by-value
    and call-by-name gradual languages.  Based on our axiomatic account we
    prove many theorems that justify optimizations and refactorings in
    gradually typed languages. For example, 
    \emph{uniqueness principles} for gradual type connectives show that if the
    $\beta\eta$ laws hold for a connective, then casts between that
    connective must be equivalent to the so-called ``lazy'' cast semantics.
    Contrapositively, this shows that ``eager'' cast semantics violates the
    extensionality of function types.  As another example, we show that
    gradual upcasts are pure functions and, dually, gradual downcasts are
    
    strict functions.  We show the consistency and applicability of our
    
    Dan Licata's avatar
    Dan Licata committed
    axiomatic theory by proving that a contract-based implementation using
    the lazy cast semantics gives a logical relations model of our type
    theory, where equivalence in GTT implies contextual equivalence of the
    programs.  Since GTT also axiomatizes the dynamic gradual guarantee, our
    model also establishes this central theorem of gradual typing.  The
    model is parametrized by the implementation of the dynamic types, and so
    gives a family of implementations that validate type-based optimization
    and the gradual guarantee.