Почему классы типов, а не просто сопоставление с образцом?

Это что-то вроде философского вопроса, но я надеюсь, что на него ответила официальная документация или «слово божье» (читай: SPJ). Есть ли конкретная причина, по которой комитет Haskell решил потребовать явные интерфейсы в форме классов типов, а не более единообразное решение, основанное на сопоставлении с образцом?

В качестве примера возьмем Eq:

class Eq a where
    (==), (/=) :: a -> a -> Bool
    x == y = not $ x /= y
    x /= y = not $ x == y

instance Eq Int where
    (==) = internalIntEq

Почему бы нам не сделать что-то подобное вместо этого (потерпите псевдо-Haskell):

(==), (/=) :: a -> a -> Bool
default x == y = not $ x /= y             -- 1
default x /= y = not $ x == y

(Int a) == (Int b) = a `internalIntEq` b  -- 2

То есть, если бы Haskell разрешал сопоставление с образцом обычных типов данных, то:

  • Программисты могут создавать специальные классы, т. е. instance будет неявным (2)

  • Типы по-прежнему можно было вывести и сопоставить статически (SupportsEqualsEquals a => ...)

  • Реализации по умолчанию будут поставляться «бесплатно»

  • Классы могут быть легко расширены, ничего не нарушая

Должен быть способ указать шаблон по умолчанию (1), который, хотя и объявлен раньше других, всегда соответствует последнему. Противоречат ли какие-либо из этих гипотетических функций чему-то, что присуще Haskell? Стало бы сложно или невозможно правильно определять типы? Похоже, это мощная функция, которая очень хорошо сочетается с остальной частью Haskell, поэтому я полагаю, что есть веская причина, по которой мы не делаем это таким образом™. Является ли этот механизм специального полиморфизма просто слишком специальным?


typeclass haskell pattern-matching
person Jon Purdy    schedule 02.02.2012    source источник
comment
Я не очень хорошо разбираюсь в этом, но я думаю, что одна из основных проблем заключается в том, что вы теряете параметричность и, следовательно, бесплатные теоремы: вы знаете, что делают id :: a -> a или fst :: (a,b) -> a, просто по их сигнатурам, потому что у них есть только параметрический полиморфизм. Если у вас есть какой-то механизм typecase, вы теряете параметричность. Например, a -> a -> Bool допускает только две (всего) реализации в Haskell (const $ const True и const $ const False); если у вас typecase, то вы теряете эту гарантию.   -  person Antal Spector-Zabusky    schedule 02.02.2012
comment
@AntalS-Z: Просто убедись, что я правильно тебя понял. Вы хотите сказать, что я могу объявить id :: a -> a, а затем определить id (Int i) = i + 1? Потому что это не так: последнее определение будет иметь тип SupportsPlus a => a -> a, что несовместимо.   -  person Jon Purdy    schedule 02.02.2012
comment
Вот как это звучит из вашего вопроса; ваша подпись типа для (==) задается как a -> a -> Bool. Если вам нужно указать класс типов SupportsEquals, то, похоже, все, что вы сделали, это изменили синтаксис --- я не понимаю, почему он другой. И я не думаю, что он может выражать классы типов с несколькими параметрами, функциональные зависимости или ассоциированные типы, хотя этого, конечно, не было в первоначальном плане. На самом деле, может ли он даже выражать классы типов более высокого порядка? Откуда вы знаете, что return :: a -> m a должно быть ad-hoc поверх m, а не a?   -  person Antal Spector-Zabusky    schedule 02.02.2012
comment
@JonPurdy Как он приобрел этот тип? i явно является Int, как это могло быть изменено на SupportsPlus a => a? Применяется ли одно и то же правило обобщения ко всем определениям или только к тем, которые используют нотацию typecase? Означает ли это, что даже при отсутствии глобальной подписи id :: a -> a id (Int i) = i + 1 имеет тип SupportsPlus a => a -> a"? If so, what are the semantics of expressions like id 3.7`?   -  person Doug McClean    schedule 02.02.2012
comment
@AntalS-Z: разница заключается в инверсии того, кто «владеет» информацией об интерфейсе. Прямо сейчас класс типов определяет, какие операции разрешены для параметра типа. Таким образом, сам тип определяет, какие операции разрешены. Я не уверен, почему классы типов с несколькими параметрами должны отличаться, кроме того, что вам все еще нужны fundeps, но они могут быть указаны в объявлении функции/оператора. Но я думаю, что вы правы — Monad может быть там, где это не удается. Не могли бы вы помочь мне с конкретным примером?   -  person Jon Purdy    schedule 02.02.2012
comment
@DougMcClean: Просто чтобы прояснить, вы не можете вывести специальные классы без явных сигнатур типов, и я не предлагаю этого. SupportsPlus (или как бы это ни называлось) происходит от использования + в (неправильном) определении id. Однако я вижу, в чем я был не прав — между Int -> Int и SupportsPlus a => a -> a есть некоторая двусмысленность, потому что ни одно из них не является полностью правильным.   -  person Jon Purdy    schedule 02.02.2012
comment
@JonPurdy: я не уверен, что вы подразумеваете под тем, что сам тип определяет, какие операции разрешены. Из вашего примера кажется, что функция определяет, какие типы разрешены. И если подпись требуется, ваш тип для (==) ошибочен? Что касается случаев, которые кажутся проблематичными: переменные типа более высокого типа и типы в позициях без аргументов. Рассмотрим maxBound :: Enum a => a или fmap :: Functor f => (a -> b) -> (f a -> f b) --- как здесь будет работать сопоставление? (Кстати, мне нравится вопрос, даже если я не совсем разбираюсь в деталях.)   -  person Antal Spector-Zabusky    schedule 02.02.2012
comment
@AntalS-Z: Мы можем перенести это обсуждение в чат?   -  person Jon Purdy    schedule 02.02.2012
comment
@JonPurdy: chat.stackoverflow.com/rooms/7265/< /а>   -  person Antal Spector-Zabusky    schedule 02.02.2012
comment
Я категорически против закрытого голосования. Конечно, это открытый, субъективный вопрос. Но я думаю, что это прекрасное интеллектуальное упражнение — исследовать, почему язык был разработан определенным образом.   -  person gatoatigrado    schedule 02.02.2012

Ответы (2)


arrow_upward
12
arrow_downward

Является ли этот механизм специального полиморфизма слишком случайным?

Этот вопрос просто требует ссылки на статью Филипа Уодлера и Стива Блотта 1988 года Как сделать рекламу -hoc полиморфизм менее ad-hoc, где они представляют идею классов Type. Уодлер, вероятно, является «словом Божьим» в этом случае.

Есть несколько проблем, которые я вижу с предлагаемой техникой "сопоставление шаблона для любого типа данных Haskell".

Метод сопоставления с образцом недостаточен для определения полиморфных констант, таких как mempty :: Monoid a => a.

Техника сопоставления с образцом все еще возвращается к классам типов, но в худшем смысле. Классы типов классифицировать типы (поймите сами). Но техника сопоставления с образцом делает его довольно расплывчатым. Как именно вы должны указать, что функции foo и bar являются частью «одного и того же» класса? Ограничения класса типов станут совершенно нечитаемыми, если вам придется добавлять новый для каждой используемой вами полиморфной функции.

Техника сопоставления с образцом вводит в Haskell новый синтаксис, усложняя спецификацию языка. Ключевое слово default выглядит не так уж плохо, но сопоставление с образцом «по типам» является новым и запутанным.

Сопоставление с образцом «на обычных типах данных» побеждает бесточечный стиль. Вместо (==) = intEq у нас (Int a) == (Int b) = intEq a b; такого рода искусственное совпадение с образцом предотвращает сокращение эта-эта.

Наконец, это полностью меняет наше понимание сигнатур типов. a -> a -> Foo в настоящее время является гарантией невозможности проверки входных данных. Ничего нельзя предположить о входах a, за исключением того, что эти два входа имеют один и тот же тип. [a] -> [a] снова означает, что элементы списка не могут быть проверены каким-либо осмысленным образом, что дает вам Theorems for Free (еще одна статья Вадлера).

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

person Dan Burton    schedule 02.02.2012
comment
относительно ваш последний пункт, я не думаю, что его предложение состоит в том, чтобы полностью изменить полиморфизм, я думаю, что просто добавить кучу ограничений типа для каждой используемой функции. то есть a -> a -> Foo по-прежнему гарантирует, что входные данные не могут быть проверены - если используется неявный класс типов, он становится частью подписи. - person gatoatigrado; 02.02.2012
comment
Большое спасибо за понимание, и бумаги. Я не согласен с парой ваших пунктов, хотя. Ограничения класса типов не стали бы нечитаемыми, потому что им даже не нужно было бы быть видимыми — вы могли бы просто сказать «(+) not defined in (foo::Foo + bar::Bar)». Пункт о сигнатурах типов важен. Вы точно знаете, что id :: a -> a по-прежнему, потому что определение, включающее любую другую функцию, будет иметь несовместимую сигнатуру. Кроме того, ре. эта-редукция, вы пишете на аппликативном (в отличие от конкатенативного) языке, так что не все в любом случае может быть бесточечным. - person Jon Purdy; 02.02.2012
comment
@gatoatigrado: Да, именно это я и имею в виду. Это не нарушает ни одну из теорем, которые у нас уже есть. По крайней мере, я так не думаю. - person Jon Purdy; 02.02.2012

arrow_upward
4
arrow_downward

Я не знаю Слова Божьего, но вот несколько аргументов.

Определение функции в одном и том же модуле больше не является уникальным. Теперь вы можете написать

(==) = internalIntEq
(==) = internalFloatEq

Это делает код менее читаемым. Существует предложение под названием "TypeBasedNameResolution", которое делает что-то подобное, но важным фактом является то, что такое ветвление типов выполняется только для (==) из разных модулей.

Добавление идентификаторов компилятором является плохой практикой. В вашем случае вы автоматически создаете класс типов SupportsEqualsEquals. Новый пользователь может спросить: «Откуда это», и не будет соответствующего источника, определяющего это.

Пропуск написания подписей экземпляров не дает вам столько, сколько вы думаете. Вы можете получить необходимые параметры, например, через :t internalIntEq в ghci. Я предполагаю, что это могло бы быть более удобным, но я бы предпочел иметь инструмент, с помощью которого я мог бы спросить «какой тип экземпляра для Eq, где == есть internalIntEq».

Более продвинутые функции класса неясны. Куда вы помещаете связанные типы и функциональные зависимости? Это очень важно для меня!!

Установка по умолчанию усложняет модульную компиляцию. Вы не получите расширяемые классы бесплатно. Рассмотреть возможность,

f :: Supports[==] a => a -> a -> Bool
f = (/=)

Насколько я понимаю, это компилируется в

f :: Instance (Supports[==]) a -> a -> a -> Bool
f eq_inst x y = not (x eq_inst.== y)

Теперь, если я предоставлю новый экземпляр /= для определенного типа a_0 и передам несколько x :: a_0 в f, тогда

f x x = not (x == x)
-- computation you really want: f x x = x /= x, using the new /= instance for a_0

Вы можете спросить: «Когда можно было быть настолько глупым, чтобы ограничить f Supports[==] вместо Supports[/=]?» Но контексты могут исходить не только от сигнатур функций; они могут исходить из функций более высокого порядка и т. д. и т. д.

Надеюсь, поможет.

person gatoatigrado    schedule 02.02.2012