Sandy Maguire

Summary of Skills

Rearchitected a failed 4-year compiler effort by migrating to a lesser-known core calculus; replaced the entire language foundation, unblocking system-wide progress
Asymptotically improved compiler performance from unscalable to linear; reduced compile times from hours to seconds and GHC build times by 93%
Built the core ML training infrastructure---used as the foundation for all models trained at the company
Guided the Python team through implementing the new runtime, including a fully-trampolined CPS transformation to eliminate stack overflows
Introduced modern engineering practices: testing, code review, Git discipline; migrated 4 fragmented repos into a monorepo to support cohesive development
Rewrote or replaced ~240k lines of code (~18% of the codebase), modernizing the compiler and runtime stack

Built a GHC plugin to track and reify federated service calls at the type-level.
Designed a property-testing framework for verifying the correctness of higher-order algebraic effects.

Wrote three books on advanced programming techniques and high-quality software engineering.

Increased new feature cadence by 30x after becoming lead of a four-person engineering team.
Directed a team of three to implement a high-throughput, low-latency brokered streaming library.

Led the architectural design of a user-defined permission model for the cloud.
Improved compile times by 96% and test coverage by 65% for a service-critical internal compiler.

Increased revenue by 0.5% after analyzing the advertising platform's spending behaviors.
Improved site-wide response time by 0.4% by parallelizing the backend graph ranker.

Integrated Neovim tightly with the Agda compiler, allowing for interactive proof assistance.

Improved performance of single-core mesh rendering by ~2x.
Reduced code duplication by 50% by reorganizing types to be shared between 2D and 3D.

Developed an interactive tactic engine for Haskell, capable of robust, type-aware code synthesis.
Provided in-editor support for automatic pattern splitting.

Discovered a convenient encoding of an effect system based on higher-order free monads via simultaneous co-Yoneda and codensity transformations.
Implemented a GHC plugin to support ad-hoc functional dependencies when working with Polysemy; dramatically improving the developer experience.

An exploration of topics from mathematics and computer science, entirely in literate Agda.

A series of worked examples on designing and efficiently implementing combinator libraries.
Algebra-Driven Design is now the basis of a course taught at OST Zurich.

thinkingwithtypes.com

A how-to manual on using (and not misusing) Haskell's more advanced type-level features.

University of Waterloo, Waterloo, ON

model checking, proof assistants, music, functional programming, compilers, robotics, electronics, math pedagogy