Trong toán học, logic và khoa học máy tính, một lý thuyết hình thái hoặc một hệ hình thái là một hệ thống hình thức trong đó mọi đối tượng đều có một hình thái (hay mọi biến đều có một kiểu, mọi từ đều có một loại,...). Hình thái của một đối tượng hạn chế các tác động (hay phép toán, cách dùng) có thể được thực hiện trên đối tượng (hay biến, từ) ấy. Ngành nghiên cứu các hệ hình thái cũng được gọi là Lý thuyết Hình Thái.Một số lý thuyết hình thái có thể đóng vai trò thay thế lý thuyết tập hợp để làm nền tảng cho toán học. Hai lý thuyết như vậy khá nổi tiếng là lý thuyết phép tính lambda hình thái của Alonzo và lý thuyết hình thái trực giác của Per Martin-Löf.Giống như các lý thuyết tập hợp tiên đề, lý thuyết hình thái được tạo ra để tránh những nghịch lý trong các nền tảng trước đây của toán học như lý thuyết tập hợp ngây thơ, logic hình thức.Lý thuyết hình thái có quan hệ chặt chẽ với, và đôi khi trùng lặp với, hệ thống kiểu trong khoa học máy tính.