Имеют ли значение переменные типа в заголовках GADT?

Есть ли разница между этими двумя декларациями GADT?

data A a b where
    ...

data A :: * -> * -> * where
    ...

syntax haskell gadt
person rightfold    schedule 24.11.2016    source источник
comment
Отличный вопрос. Это моя любимая мозоль - я всегда задавался вопросом, зачем нам нужно называть индексы, когда имена кажутся неуместными в другом месте. Это очень отличается от индексов и параметров в индуктивных типах, используемых в зависимых системах, таких как, например, Agda/Coq.   -  person chi    schedule 24.11.2016
comment
Обратите внимание, что, напротив, в семействах типов у нас есть разница между type family A :: * -> * -> * и type family A a :: * -> * - первый допускает такие экземпляры, как A Int Bool = Char ; A Int Char = Bool, а последний - нет, допуская только, например. A Int = Maybe. (имя a пока неактуально, правда в type family A a :: * -> *)   -  person chi    schedule 24.11.2016
comment
... тогда как type family B b :: * не позволяет вам использовать, например. MaybeT B a, что возможно с type family B :: * -> *. Первый будет приложением синонима частичного типа. (LiberalTypeSynonyms иногда может обойти это ограничение.)   -  person leftaroundabout    schedule 24.11.2016
comment
Есть разница с включенным TypeInType - вы не можете писать, например, X :: (a :: k) -> P a -> *, пока X (a :: k) (p :: P a) действителен. Существует также разница в том, какие параметры kind на самом деле являются индексами (опять же только с TypeInType) - объявление data X0 :: Fin n -> * where X0 :: X0 Fz недопустимо (поскольку n на самом деле является параметром, а X0 не является параметрическим в n) , в то время как data X0 (q :: Fin n) where X0 :: X0 Fz действителен. Однако data X0 :: forall n . Fin n -> * также делает n индексом.   -  person user2407038    schedule 25.11.2016
comment
Вот еще одно странное несоответствие.. с включенным TypeInType data X1 :: k -> * является параметрическим для вида k, но без TypeInType он индексируется для вида k. И еще... data X2 :: forall k . k -> forall k' . k' -> * и data X2 :: forall k . k -> forall k' . k' -> * имеют совершенно разные виды - суждение X1 ~ X2 даже плохо типизировано! Но даже X2 невозможно выразить с помощью первого синтаксиса. Везде в Haskell (за исключением, возможно, TypeApplications) порядок forall связанных переменных типа не имеет значения.   -  person user2407038    schedule 25.11.2016
comment
@ user2407038 Интересно. Я не слишком хорошо знаком с последствиями TypeInType. Вы можете превратить свои комментарии в расширенный ответ.   -  person chi    schedule 25.11.2016

Ответы (1)


arrow_upward
8
arrow_downward

Нет никакой разницы. Можно подумать, что не упоминать переменные типа в заголовке было бы необходимо, чтобы использовать для них разные имена в сигнатурах конструктора, например:

data A :: * -> * -> * where
    AN :: Num x => x -> b -> A x b
    AS :: IsString s => s -> b -> A s b

Однако, поскольку Руководство пользователя GHC говорит...

В отличие от объявления типа данных в стиле Haskell-98, переменные типа в заголовке data Set a where не имеют области видимости.

... и так это тоже работает:

data A a b where
    AN :: Num x => x -> b -> A x b
    AS :: IsString s => s -> b -> A s b
person duplode    schedule 24.11.2016
comment
Действительно, первое мне нравится больше всего, но я всегда заканчиваю тем, что пишу второе, так как оно короче и мне лень. Думаю, для документации было бы полезно давать им вызывающие воспоминания имена. - person chi; 24.11.2016
comment
Я предпочитаю второй стиль, потому что не люблю писать добрые подписи. - person Benjamin Hodgson♦; 24.11.2016
comment
Я предполагаю, что было бы возможно опустить переменные типа из синтаксиса, но тогда нам бы понадобились сигнатуры частичного вида. - person dfeuer; 24.11.2016