Type-Safe Modeling for Optimization

Abstract

Mathematical optimization has many applications in operations research, image processing, and machine learning, demanding not only computational efficiency but also convenience and correctness in constructing complex models. In this work, we introduce HashedExpression, an open-source algebraic modeling lan- guage (AML) that allows users to express unconstrained, box-constrained, and scalar-expressions-constrained optimization problems, aimed at embeddability, type-safety, and high-performance through symbolic transformation and code generation. Written in Haskell, a statically-typed, purely functional program- ming language, HashedExpression places a great emphasis on modeling correct- ness by providing users with a type-safe, correct-by-construction interface that uses Haskell type-level programming to express constraints on correctness which the compiler uses to flag many modelling errors as type errors (at compile time). We show how type-safety can be added in steps, first matching expressions’ shape and then associated physical units. The library implements symbolic ex- pressions with a hashed indexing scheme to implement common subexpression elimination (CSE). It abstracts away details of the underlying lookup table via monadic type class instances. We explain how using symbolic expressions with CSE enables performance-enhance transformations and automatic computation of derivatives without the issue of “expression swelling”. For high-performance purposes, we generate low-level C/C++ code for symbolic expressions and pro- vide bindings to open-source optimization solvers such as Ipopt or L-BFGS-B. We explain how this architecture lays the groundwork for future work on par- allelization including SIMDization and targetting multi-core CPUs and GPUs, and other hardware acceleration.