ну вот я про него и говорил, когда кроме одного

а мейер?

мейер 7.4 тоже не пользуется

Вопрос про GADTs - каково практическое применение того, что конструкторы могут возвращать разный тип? Я вот прочитал пример про type witness, как ещë можно использовать?

Вроде канонiческий пример - well-typed интерпретатор

Можно поподробнее?

Пока вроде нашел пару пейперов, где они упоминаются, вроде понял зачем оно

Это когда мы делаем AST вместо

data Expr = Int Int | Bool Bool | Add Expr Expr | If Expr Expr Expr

в виде

data Expr a where
  Int :: Int -> Expr Int
  Bool :: Bool -> Expr Bool
  Add :: Expr Int -> Expr Int -> Expr Int
  If :: Expr Bool -> Expr a -> Expr a

чтобы в рантайме не проверять сложение инта с булём.

Ну это да

В общем, как я понял, конструкторы содержат инфу о типе, и, матчась по конструкторам, мы, грубо говоря, можем в каком-то смысле матчиться по типам

в конструкторе есть неявный пруф что типопеременная равна какому-то типу, и матчась мы достаем этот пруф с другими значениями

data T a where
 TBool :: Bool -> T Int
 TInt :: Int -> T Bool

f :: T a -> a
f (TBool True) = 1
f (TBool False) = 0
f (TInt x) = x == 0

~~~

data T a
  = TBool {a ~ Int} Bool
  | TInt {a ~ Bool} Int

coe :: a -> a ~ b -> b
sym :: a ~ b -> b ~ a

f :: T a -> a
f (TBool {p :: a ~ Int} True) =
  (coe (sym p) (1 :: Int)) :: a
f (TBool {p :: a ~ Int} False) =
  (coe (sym p) (0 :: Int)) :: a
f (TInt {p :: a ~ Bool} (x :: Int)) =
  (coe (sym p) ((x == 0) :: Bool)) :: a

я считаю что это хороший пример, чтобы сразу не было ложной интуиции, что тип в гадте как-то завязан на тип содержимого, а то у меня так и было

Спасибо! Попробую прочитать...

С coe и sym сложно -.-

Почему только сигнатуры?

Т.е. GADTs выражаются через дататайпы с констрейнтом на равенство типов?

потому что они не определены, но есть в контексте.
Да, GADT-ы выражены через равенства типов
coe просто кастит значение одного типа к другому, если они равны, а sym переворачивает пруф

вместо coe на самом деле cast, я перепутал