должен полностью описать, что вы можете с ним сделать. Если вы можете вызывать его только для определенных типов, это должно отражать сигнатура типа.

тоящее время я пытаюсь обернуть голову вокруг типов классов и экземпляров, и пока не совсем понимаю их смысл. У меня есть два вопроса по этому вопросу:

1) Почему необходимо иметь класс типа в сигнатуре функции, когда функция использует некоторую функцию из этого класса типов. Пример:

f :: (Eq a) => a -> a -> Bool
f a b = a == b

Зачем ставить(Eq a) в подписи. Если== не определено дляa тогда почему бы просто не скинуть ошибку при встречеa == b? Какой смысл в том, чтобы объявлять класс типа впереди?

2) Как связаны классы типов и перегрузка функций?

Это невозможно сделать:

data A = A
data B = B

f :: A -> A
f a = a

f :: B -> B
f b = b

Но это можно сделать так:

data A = A
data B = B

class F a where
  f :: a -> a

instance F A where
  f a = a

instance F B where
  f b = b

Что с этим? Почему у меня не может быть двух функций с одинаковым именем, но работающих на разных типах ... Исходя из C ++, я нахожу это очень странным. Но у меня, вероятно, неправильные представления о том, что это на самом деле. но как только я заверну их в эти экземпляры класса типов, я смогу.

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

 lo tolmencre25 дек. 2017 г., 21:36
Нет, я имею в виду выбросить ошибку при обнаружении неопределенной функции во время компиляции.
 chi25 дек. 2017 г., 23:06
Если бы мне пришлось проводить принудительное сравнение, классы типов неопределенно связаны с концепциями C ++ 20, за исключением того, что в Haskell нет SFINAE: функция компилируется рано (в отличие от шаблонов), и ограничения должны гарантировать, что определение функции в порядке для всех типы (с предоставлением ограничений).
 Daniel Wagner25 дек. 2017 г., 21:42
Если я напишуf :: a -> a -> Boolи позже примените его к чему-то, что нельзя сравнить на равенство, скажем,f (1+) (1-)как компилятор обнаружит, что нам теперь нужно иметь(==) определены для того, чтобы выбросить ошибку? Ответ: компилятор записывает небольшой факт оf что это относится(==) к его аргументам, так что он знает, когда видит вызовыf чтобы проверить это(==) доступен. Как мы отмечаем этот факт? Ответ: мы помещаем это в тип, какf :: Eq a => a -> a -> Bool.
 25 дек. 2017 г., 23:02
@lotolmencre Ах, может быть, я начинаю понимать твою точку зрения. Возможно, вы запутались, поскольку привыкли к шаблонам C ++. Шаблоны C ++ более или менее компилируются (включая проверку типов) для каждого экземпляра аргументов шаблона. (Ограниченные) полиморфные функции Haskell компилируются только один раз, и «шаблонизации» не существует (аналогично, например, дженерикам Java). В C ++ вам нужны заголовочные файлы, содержащие исходные шаблоны. В Haskell вам не нужен исходный код после компиляции.
 chi25 дек. 2017 г., 21:33
«просто выбросить ошибку» во время выполнения - это именно то, чего пытаются избежать статически типизированные языки. Основной момент наличия системы типов - это раннее обнаружение ошибок определенного типа во время компиляции.

Ответы на вопрос(4)

Каждая переменная может использоваться как выражение самостоятельно;Каждое выражение имеет тип, которыйточно указывает, что вам разрешено делать с этим.

Если у тебя есть

f :: A -> A

а также

f :: B -> B

затем, в соответствии с принципами, принятыми в Haskell,f все равно будет действительным выражением, само по себе, которое все еще должно иметьОдин тип. Хотя это можно сделать с использованием подтипов, это было гораздо сложнее, чем решение класса типов.

Точно так же, необходимостьEq a в

(==) :: Eq a => a -> a -> Bool

исходит из того, что тип== должен полностью описать, что вы можете с ним сделать. Если вы можете вызывать его только для определенных типов, это должно отражать сигнатура типа.

Решение Вопроса

Я согласен с большей частьюВиллем Ван Онсем ответ, но я думаю, что он упускает из виду одно из главных преимуществ классов типов по сравнению с действительно специальной перегрузкой:абстракция, Представьте, что мы использовали специальную перегрузку вместо классов типов для определенияMonad операции:

-- Maybe
pure :: a -> Maybe a
pure = Just

(>>=) :: Maybe a -> (a -> Maybe b) -> Maybe b
Just x >>= f = f x
Nothing >>= _ = Nothing

-- Either
pure :: a -> Either e a
pure = Right

(>>=) :: Either e a -> (a -> Either e b) -> Either e b
Right x >>= f = f x
Left err >>= _ = Left err

Теперь мы знаем, что каждая монада может быть выражена в терминахpure а также>>=как указано выше, но мытакже знать, что они могут быть эквивалентно выражены с помощьюfmap, pure, а такжеjoin, Поэтому мы должны быть в состоянии реализоватьjoin функция, которая работает наЛюбые монада:

join x = x >>= id

Однако сейчас у нас проблема. Что такоеjoinТип?

Очевидно, чтоjoin должен быть полиморфным, так как он работает на любой монаде по замыслу. Но давая ему тип подписиforall m a. m (m a) -> m a было бы явно неправильно, так как этоне работают для всех типов, только монадические. Следовательно, нам нужно что-то в нашем типе, что выражает необходимость существования некоторой операции(>>=) :: m a -> (a -> m b) -> m b, что именно то, что обеспечивает ограничение класса типов.

Учитывая это, становится ясно, что специальная перегрузка позволяет перегрузить имена, но невозможно абстрагироваться от этих перегруженных имен, потому что нет гарантии, что различные реализации связаны каким-либо образом. Вымог определить монады без классов типов, но тогда вы не можете определитьjoin, when, unless, mapM, sequenceи все другие приятные вещи, которые вы получаете бесплатно, когда определяете только две операции.

Следовательно, классы типов необходимы в Haskell, чтобы обеспечить возможность повторного использования кода и избежать колоссального дублирования. Но не могли бы выобе перегрузка в стиле типа и специальная перегрузка имен?даи на самом деле Идрис делает. Но типичный вывод Идриса очень отличается от типичного в Хаскеле, поэтому его легче поддержать, чем в Хаскеле, по многим причинам в ответе Виллема.

потому что именно так был разработан Haskell.

Зачем ставить(Eq a) в подписи. Если== тогда не определяется, почему бы просто не выдать ошибку при встречеa == b?

Почему мы помещаем типы в сигнатуру программы на C ++ (а не просто как утверждение в теле)? Потому что так устроен C ++. Как правило, концепция того, на чем строятся языки программирования:сделать явным то, что должно быть явным».

Не сказано, что модуль Haskell с открытым исходным кодом. Так что это означает, что у нас есть только подпись. Таким образом, это означает, что когда мы, например, пишем:

Prelude> foo A A

<interactive>:4:1: error:
    • No instance for (Eq A) arising from a use of ‘foo’
    • In the expression: foo A A
      In an equation for ‘it’: it = foo A A

Мы часто пишемfoo здесь с типами, которые не имеютEq класс типов. В результате мы получили бы много ошибок, которые обнаруживаются только во время компиляции (или если бы Haskell был динамическим языком во время выполнения). Идея ставитьEq a в сигнатуре типа мы можем найти сигнатуруfoo заранее, и, таким образом, убедитесь, что типы являются экземпляром класса типов.

Обратите внимание, что вам не нужно писать сигнатуры типов самостоятельно: Haskell обычно может получить сигнатуру функции, но сигнатура должна включать всю необходимую информацию для эффективного вызова и использования функции. Добавляя ограничения типов, мы ускоряем разработку.

Что с этим? Почему у меня не может быть двух функций с одинаковым именем, но работающих на разных типах.

Опять же: так устроен Haskell. Функции в функциональных языках программирования естьпервоклассные гражданеMsgstr "Это означает, что у них обычно есть имя, и мы хотим максимально избегать конфликтов имен. Точно так же, как классы в C ++ обычно имеют уникальное имя (за исключением пространств имен).

Скажем, вы бы определили две разные функции:

incr :: Int -> Int
incr = (+1)

incr :: Bool -> Bool
incr _ = True

bar = incr

Тогда какойincr было быbar должен выбрать? Конечно, мы можем сделать типы явными (т.е.incr :: Bool -> Bool), но обычно мы хотим избежать этой работы, так как она создает много шума.

Еще одна веская причина, по которой мы этого не делаем, заключается в том, что, как правило, класс типов - это не просто набор функций: он добавляетконтракты к этим функциям. Например,Monad Класс типов должен удовлетворять определенным отношениям между функциями. Например(>>= return) должно быть эквивалентноid, Другими словами, класс типов:

class Monad m where
    (>>=) :: m a -> (a -> m b) -> m b
    return :: a -> m a

Не описывает дванезависимый функции(>>=) а такжеreturn: это набор функций. У вас есть оба (обычно с некоторыми договорами между>>= а такжеreturn) или ничего из этого.

 Daniel Wagner05 апр. 2018 г., 22:54
«Потому что так все устроено». Хорошо, конечно, но почему это так задумано?
 Willem Van Onsem06 апр. 2018 г., 00:33
@DanielWagner: хорошо, что утверждается в оставшейся части ответа. Например, чтобы сделать явным то, что должно быть явно, и т. Д. Насколько я знаю, не все обоснования полностью задокументированы проектировщиками, и может возникнуть путаница, если некоторые из них были «нарочно» или более «(счастливым) совпадением»: ).

Тип подписиf :: a -> a -> Bool это сокращение дляf :: forall a. a -> a -> Bool. f не будет действительно работатьдля всех типыa если это работает только дляaс, которые имеют(==) определены. Это ограничение для типов, которые имеют(==) выражается с использованием ограничения(Eq a) вf :: forall a. (Eq a) => a -> a -> Bool.

«Для всех» / универсальная квантификация лежит в основе (параметрического) полиморфизма Хаскелла и, помимо прочего, обеспечивает мощные и важные свойстваparametricity.

 lo tolmencre25 дек. 2017 г., 21:38
Ах так(Eq a) => a -> a -> Bool означаетforall a. a in Eq => a -> a -> Bool
 David25 дек. 2017 г., 21:43
@lotolmencre Если я вас правильно понимаю, это примерно означает что-то подобноеa должен быть «членом» класса «Уравнение») ... Есть немного больше, так как технически(Eq a) является приложением (на уровне типа)Eq к типу, чтобы получить ограничение, хотя.Eq принимает один тип и возвращает ограничение. Это важно, потому что, например, некоторые классы типов принимают более одного типа (для этого необходимо включить расширение, но это обычное расширение).
 David25 дек. 2017 г., 21:47
Один из способов взглянуть на это состоит в том, что классы типов с одним параметром являются предикатами типов (поэтомуEq a => ... означает "a имеет экземплярEqMsgstr "). Это очень хорошо распространяется на классы многопараметрических типов, поскольку позволяет вам рассматривать их как отношения между типами. Это может быть немного впереди вещей, но может быть полезно получить представление о том, куда они движутся ,

Ваш ответ на вопрос