Ошибки компиляции с семьями типа, GADTs и именованными записями

Question

В следующем коде, T1 и T2 компилироваться, но T3 не удается:

{-# LANGUAGE GADTs #-} 
{-# LANGUAGE TypeFamilies #-} 

type family F a 

data T1 b where 
    T1 :: a -> T1 (F a) 

data T2 b where 
    T2 :: { x2 :: a } -> T2 a 

data T3 b where 
    T3 :: { x3 :: a } -> T3 (F a) 

Я пытаюсь понять, почему. T3 всего лишь T1, но с названной записью. Это не похоже на все, что особенно важно, поскольку в любом случае можно использовать синтаксис конструктора.

Эти примеры, вероятно, выглядят глупо, но в моем коде есть ограничение на a, например. (Show a), поэтому эти значения могут использоваться, когда они извлекаются.

Answer 1

Давайте забудем о T2 и T3 и попробуем определить функцию экстрактора для T1. Каким должен быть тип?

x1 :: ??? 
x1 (T1 a) = a 

Ну, вы можете догадаться, x1 :: T1 (F a) -> a. Но это неправильно, и если вы попробуете это, вы получите ту же ошибку, которую вы получили для определения T3.

Проблема заключается в том, что если кто-то вручает вам T1 T, и вы не знаете тип A таким образом, что F A является T, вы не можете сделать вывод о том, что T1 T содержит значение типа A, поскольку он может вместо этого содержать другой тип B с F B, равным T. В крайнем случае, предположим, что мы имеем

type instance F _ =() 

Тогда, если мы взяли нашу догадку x1 :: T1 (F a) -> a, мы должны были бы

T1 :: a -> T1() 
x1 :: T1() -> b 

и составлении этих позволил бы нам написать a -> b, что плохо.

Реальный тип x1 это нечто вроде экзистенциально- обеспечения-ограничения

T1 t -> (exists a. (F a ~ t) *> a) 

который GHC не поддерживает.

Проблема с T3 фактически то же самое, как если бы у вас была

data T3' where T3' :: { x3' :: a } -> T3' 

Вы можете извлечь поле с сопоставления с образцом (который может быть полезным, если бы было больше полей или ограничение), но не с селектор или функция записи.