экземпляры семейства данных: новый тип, данные

Question

В Haskell 98 decls тип данных должен быть либо newtype, либо data.Но семейства данных могут иметь комбинацию newtype instance, data instance.Означает ли это, что newtype является свойством конструктора данных, а не типа данных?Может ли быть Haskell с чем-то вроде:

data Foo a = MkFoo1 Int a
           | MkFoo2 Bool a
           | newtype MkFoo3 a

Я знаю, что не могу написать следующее, но почему / что идет не так?:

data family Bar a

newtype instance Bar (Maybe Int)  = MkBar1 (Maybe Int)
            -- MkBar1 :: (Maybe Int) -> Bar (Maybe Int), see below

newtype instance Bar [Char]  = MkBar2 [Char]

data instance Bar [Bool]  where
  MkBar3 :: Int -> Bool -> Bar [Bool]
  -- can't be a newtype because of the existential Int

-- we're OK up to here mixing newtypes and data/GADT

data instance Bar [a]  where
  MkBar4 :: Num a => a -> Bar [a]
  -- can't be a newtype because of the Num a =>

Я не могу написатьэто потому, что головка экземпляра Bar [a] перекрывает две головки для MkBar2, MkBar3.Тогда я мог бы это исправить, переместив эти два конструктора decls в where ... для Bar [a].Но тогда MkBar2 становится GADT (потому что его тип результата не Bar [a]), поэтому не может быть newtype.

Тогда он является newtype свойством типа результата,а не конструктор?Но рассмотрим тип, выведенный для экземпляра newtype MkBar1 выше.Я не могу написать верхнего уровня newtype с тем же типом

newtype Baz a  where
  MkBaz :: (Maybe Int) -> Baz (Maybe Int)

-- Error: A newtype constructor must have a return type of form T a1 ... an

А?MkBar1 - конструктор нового типа, тип которого не соответствует этой форме.

Если возможно, пожалуйста, объясните, не вдаваясь в разговоры о ролях: я пытался понять их;это просто делает мою голову болит.Поговорите о построении и сопоставлении с образцом этих конструкторов.

Answer 1

Они эквивалентны:

newtype          NT a b  = MkNT (Int, b)

data family DF a b
newtype instance DF a b  = MkDF (Int, b)

-- inferred MkNT :: (Int, b) -> NT a b
--          MkDF :: (Int, b) -> DF a b

Более того, вы не можете объявить любой другой экземпляр / конструктор в семействе DF, потому что их заголовки экземпляра будут перекрываться DF a b.

.сообщение об ошибке в q re standalone newtype Baz вводит в заблуждение

-- Error: A newtype constructor must have a return type of form T a1 ... an

(и предположительно датируется тем, что появились семейства данных).Конструктор нового типа должен иметь возвращаемый тип в точности как заголовок экземпляра (переименование по модулю альфа, если он использует синтаксис GADT).Для автономного нового типа «заголовок экземпляра» означает заголовок newtype.

Для экземпляров данных не нового типа различные конструкторы могут иметь типы возвращаемых данных, более специфичные, чем заголовок экземпляра (что делает их GADT).

Тип, объявленный в заголовке экземпляра data / newtype (в литературе по-разному называемый «схемой типа», «монотипом» - потому что нет ограничений, «Тип без функции» - в статье 2008 года »).Проверка типов с использованием открытых функций типов ') - это основной тип, с которым должны возвращаться все возвращаемые типы конструкторов.(Не может быть никаких конструкторов с точно таким возвращаемым типом.)

Если ваш экземпляр - newtype, правила намного строже: может быть только один конструктор, и его тип возвращаемого значения должен быть точноосновной тип.Итак, чтобы ответить на исходный q

Означает ли это, что newtype является свойством конструктора данных, а не типа данных?... но ... Тогда является ли newtype свойством типа результата, а не конструктора?

Нет, не конструктора;да, больше похоже на результат: быть новым типом - это свойство экземпляра семейства данных / его основного типа.Просто для автономных новых типов может быть только один экземпляр, и его основной тип является наиболее общим типом для этого конструктора типов.Производно, мы можем сказать, что основной тип нового типа / тип возврата однозначно идентифицирует конструктор данных.Это важно для безопасности типов, потому что значения этого типа делят свое представление с типом внутри конструктора данных нового типа, то есть без обертки - как указывает комментарий @ AlexisKing.Тогда сопоставление с образцом не нужно искать в конструкторе: совпадение неопровержимо / конструктор является виртуальным.

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

Answer 2

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

Означает ли это, чтоnewtype это свойство конструктора данных, а не тип данных?Может ли быть Haskell с чем-то вроде:

data Foo a = MkFoo1 Int a
           | MkFoo2 Bool a
           | newtype MkFoo3 a

Нет.То, что newtype, безусловно, является свойством конструктора типа, а не конструктора данных.Семейство данных, как и семейство типов, имеет два уровня конструкторов типов:

• конструктор типов data/type family FamTyCon a
• конструкторы типов для экземпляров data/type instance FamInstTyCon a = ...

Различные экземпляры одного и того же конструктора семейства data/type по-прежнему принципиально разных типов - они оказываются объединенными в одном конструкторе типов (и этот конструктор типов будет инъективным и генеративным - см. Связанный вопрос для получения дополнительной информации).на этом).

По аналогии с семейством типов вы не ожидаете, что сможете найти образец соответствия для чего-то типа TyFam a, верно?Потому что у вас могут быть type instance TyFam Int = Bool и type instance TyFam () = Int, и вы не сможете статически знать, смотрите ли вы на Bool или Int!