Feature engineering is the preprocess of training and serving machine learning models. Programmers formalize their domain knowledge into data operations that convert raw data to proper model inputs. Features are usually written in languages of the Sql-family, which includes F3 (Facebook Feature Framework), a compiler developed at Meta. During the development of F3, we have found that a compiler for feature engineering may benefit from Martin-Löf’s type theory and its implementation techniques. Here, we demonstrate the dependent type system of F3, and its practical applications in daily feature engineering.