More Like this

1. Rademacher type and Enflo type coincide

   Ivanisvili, Paata; van Handel, Ramon; Volberg, Alexander. (September 2020, Annals of mathematics)

   null (Ed.)

   A nonlinear analogue of the Rademacher type of a Banach space was introduced in classical work of Enflo. The key feature of Enflo type is that its definition uses only the metric structure of the Banach space, while the definition of Rademacher type relies on its linear structure. We prove that Rademacher type and Enflo type coincide, settling a long-standing open problem in Banach space theory. The proof is based on a novel dimension-free analogue of Pisier’s inequality on the discrete cube. 

   more » « less
2. Rademacher type and Enflo type coincide

   https://doi.org/10.4007/annals.2020.192.2.8  

   Ivanisvili, Paata; Van Handel, Ramon; Volberg, Alexander (February 2020, Annals of mathematics)

   A nonlinear analogue of the Rademacher type of a Banach space was introduced in classical work of Enflo. The key feature of Enflo type is that its definition uses only the metric structure of the Banach space, while the definition of Rademacher type relies on its linear structure. We prove that Rademacher type and Enflo type coincide, settling a long-standing open problem in Banach space theory. The proof is based on a novel dimension- free analogue of Pisier’s inequality on the discrete cube. 

   more » « less
3. Stitch: the sound type-indexed type checker (functional pearl)

   https://doi.org/10.1145/3406088.3409015  

   Eisenberg, Richard A. (August 2020, Haskell 2020: Proceedings of the 13th ACM SIGPLAN International Symposium on Haskell)

   null (Ed.)

   A classic example of the power of generalized algebraic datatypes (GADTs) to verify a delicate implementation is the type-indexed expression AST. This functional pearl refreshes this example, casting it in modern Haskell using many of GHC's bells and whistles. The Stitch interpreter is a full executable interpreter, with a parser, type checker, common-subexpression elimination, and a REPL. Making heavy use of GADTs and type indices, the Stitch implementation is clean Haskell code and serves as an existence proof that Haskell's type system is advanced enough for the use of fancy types in a practical setting. The paper focuses on guiding the reader through these advanced topics, enabling them to adopt the techniques demonstrated here. 

   more » « less
4. Twinning stress of type I and type II deformation twins

   https://doi.org/10.1016/j.actamat.2019.07.004  

   Mullner, Peter (July 2019, Acta materialia)

   Recent reports on highly mobile type II twin boundaries challenge the established understanding of deformation twinning and motivate this study. We consider the motion of twin boundaries through the nucleation and growth of disconnection loops and develop a mechanism-based model for twin boundary motion in the framework of isotropic linear elasticity. While such mechanisms are well established for type I and compound twins, we demonstrate based on the elastic properties of crystals that type II twin boundaries propagate in a similar way. Nucleation of a type I twinning disconnection loop occurs in a discrete manner. In contrast, nucleation of a type II twinning disconnection loop occurs gradually with increasing Burgers vector. The gradual nucleation of a type II disconnection loop accounts for the higher mobility of type II twin boundaries compared with type I twin boundaries. We consider the homogeneous nucleation of a disconnection loop, which is adequate for twinning in shape memory alloys with a low-symmetry crystal lattice. For the magnetic shape memory alloy Ni-Mn-Ga, the model predicts twinning stresses of 0.33 MPa for type II twinning and 4.7 MPa for type I twinning. Over a wide temperature range, the twinning stress depends on temperature only through the temperature dependence of the elastic constants, in agreement with experimental results. 

   more » « less
5. Gradual type theory

   https://doi.org/10.1017/S0956796821000125  

   NEW, MAX S.; LICATA, DANIEL R.; AHMED, AMAL (January 2021, Journal of Functional Programming)

   null (Ed.)

   Abstract Gradually typed languages are designed to support both dynamically typed and statically typed programming styles while preserving the benefits of each. Sound gradually typed languages dynamically check types at runtime at the boundary between statically typed and dynamically typed modules. However, there is much disagreement in the gradual typing literature over how to enforce complex types such as tuples, lists, functions and objects. In this paper, we propose a new perspective on the design of runtime gradual type enforcement: runtime type casts exist precisely to ensure the correctness of certain type-based refactorings and optimizations. For instance, for simple types, a language designer might desire that beta-eta equality is valid. We show that this perspective is useful by demonstrating that a cast semantics can be derived from beta-eta equality. We do this by providing an axiomatic account program equivalence in a gradual cast calculus in a logic we call gradual type theory (GTT). Based on Levy’s call-by-push-value, GTT allows us to axiomatize both call-by-value and call-by-name gradual languages. We then show that we can derive the behavior of casts for simple types from the corresponding eta equality principle and the assumption that the language satisfies a property called graduality , also known as the dynamic gradual guarantee. Since we can derive the semantics from the assumption of eta equality, we also receive a useful contrapositive: any observably different cast semantics that satisfies graduality must violate the eta equality. We show the consistency and applicability of our 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 parameterized by the implementation of the dynamic types, and so gives a family of implementations that validate type-based optimization and the gradual guarantee. 

   more » « less