ADT можно легко объяснить с помощью теории моделей как модель алгебраической c теории. Но GADT меня озадачивает: остается ли это моделью алгебраической c теории, или это модель геометрической c теории, или есть правильное теоретико-типовое описание того, что такое GADT, с точки зрения теории типов?