Добавление ограничений типа в объявления данных

Я читал о создании наших собственных типов и классов типов из Learn You a Haskell for Great Good. Я не совсем понимаю поведение компилятора Haskell, когда я добавляю ограничение типа к своим объявлениям data.

Например, у меня есть

{-# LANGUAGE DatatypeContexts #-}

data (Ord a) => OrderedValue a = OrderedValue a

getOrderedValue :: OrderedValue a -> a
getOrderedValue (OrderedValue a) = a

Как видно выше, у меня есть ограничение типа для моего объявления данных, согласно которому любое значение, содержащееся внутри OrderedValue, должно иметь экземпляр Ord.

Я попытался скомпилировать этот код, и компилятор выплюнул

• No instance for (Ord a) arising from a use of ‘OrderedValue’
  Possible fix:
    add (Ord a) to the context of
      the type signature for:
        getOrderedValue :: forall a. OrderedValue a -> a
• In the pattern: OrderedValue a
  In an equation for ‘getOrderedValue’:
      getOrderedValue (OrderedValue a) = a

Изменение определения getOrderedValue на

getOrderedValue :: (Ord a) => OrderedValue a -> a
getOrderedValue (OrderedValue a) = a

ожидаемо исправил проблему.

У меня вопрос - почему компилятор здесь жалуется? Я предположил, что компилятор должен иметь возможность сделать вывод, что шаблон a соответствует в

getOrderedValue (OrderedValue a) = a

имеет экземпляр Ord, потому что конструктор значения OrderedValue предназначен для создания экземпляров типа OrderedValue с параметром типа a, имеющим экземпляр Ord.

Уф, это был полный рот.

Спасибо.

ИЗМЕНИТЬ - я просмотрел альтернативные ответы, предложенные @melpomene, спасибо за это. Однако я ищу ответ, который описывает почему разработчики языка Haskell решили реализовать его именно таким образом.


typeclass type-constraints haskell
person divesh premdeep    schedule 17.10.2018    source источник
comment
Возможный дубликат Почему Haskell не хотите выводить классы типов данных в сигнатурах функций?   -  person melpomene    schedule 17.10.2018
comment
... или stackoverflow.com/questions/12770278/ < / а>   -  person melpomene    schedule 17.10.2018
comment
Предполагается, что компилятор может сделать это: попробуйте удалить сигнатуру типа функции и посмотрите. Но здесь вы отключаете любой вывод, потому что вы явно указываете тип своей функции, поэтому компилятор даже не начинает вывод. Он просто жалуется, что подпись неверна (или, скорее, функция не подходит для этой подписи)   -  person gigabytes    schedule 17.10.2018
comment
@gigabytes Это первый случай, с которым я столкнулся, когда добавление сигнатуры функции фактически изменяет поведение компилятора. Я думал, что сигнатуры функций служат больше для удобства чтения / документации, потому что они на самом деле не нужны.   -  person divesh premdeep    schedule 17.10.2018
comment
@melpomene Ура, однако эти ответы не объясняют, почему.   -  person divesh premdeep    schedule 17.10.2018
comment
@diveshpremdeep Неудивительно, что добавление сигнатуры функции может изменить поведение компилятора. Если вы добавите просто неправильную подпись, например sort :: IO Double -> Char, то это обязательно вызовет ошибку времени компиляции. Дело в том, что вы можете спросить компилятор, какова (наиболее общая) правильная подпись, вместо того, чтобы писать ее самостоятельно - хотя чаще всего лучше начать с подписи и позволить компилятору помочь вам с реализацией < / i> вместо этого. И иногда подписи действительно необходимы, особенно когда задействованы типы Rank-2.   -  person leftaroundabout    schedule 17.10.2018
comment
Как сказал @leftaroundabout, это просто случай неправильной сигнатуры типа. Если вы напишете сигнатуру того же типа, которую компилятор определил бы в одиночку, конечно, его поведение не изменится. Но если вы напишете неправильный или один правильный, но менее общий, чем самый общий (который предполагается), то, конечно, компилятор будет действовать соответствующим образом.   -  person gigabytes    schedule 17.10.2018
comment
Подпись предназначена для документирования, но не только для этого. Обычная документация предназначена только для людей. Подписи, напротив, читаются как людьми, так и компилятором, который проверяет код на соответствие подписи. Действительно, мы добавляем их в код, чтобы компилятор мог выявить ошибки как можно раньше. Если мы хотим, чтобы функция возвращала строку, но мы допускаем ошибку и заставляем ее возвращать логическое значение, компилятор с радостью определит непредусмотренный тип и сообщит об ошибках (возможно) только при использовании функции, что удивит программиста. С типовой сигнатурой ошибка обнаруживается рано.   -  person chi    schedule 17.10.2018
comment
@diveshpremdeep Определение типа неразрешимо в любой относительно сложной системе типов. Компилятору Haskell нужны сигнатуры типов во многих ситуациях. Что касается вашего кода: надеюсь, вы прочитали книгу: вам не следует добавлять такие ограничения в объявление data. Они действительно ничего не добавляют к вашему типу и вызывают только головную боль. Есть альтернативы получше.   -  person Bakuriu    schedule 18.10.2018
comment
@gigabytes Действительно, если я опущу объявление типа, компилятор успешно скомпилирует мой код. Насколько я понимаю, мой исходный код не работает, потому что я заменяю объявление предполагаемого типа компилятором своим собственным, о котором упоминал пользователь leftaroundabout. Пожалуйста, добавьте свой комментарий в качестве ответа, чтобы я мог его принять. Спасибо!   -  person divesh premdeep    schedule 18.10.2018
comment
@Bakuriu Я сейчас просматриваю книгу. Мне просто было любопытно, почему компилятор так себя ведет.   -  person divesh premdeep    schedule 18.10.2018
comment
см. этот ответ в первом предложенном дубликате.   -  person Will Ness    schedule 21.10.2018

Ответы (1)


arrow_upward
2
arrow_downward

Предполагается, что компилятор может сделать это: попробуйте удалить сигнатуру типа функции и посмотрите. Например, с ghci:

Prelude> :set -XDatatypeContexts
Prelude> data Ord a => OrderedValue a = OrderedValue a
Prelude> let getOrderedValue (OrderedValue a) = a
Prelude> :t getOrderedValue
getOrderedValue :: Ord t => OrderedValue t -> t

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

Итак, здесь компилятор проверяет тип вашего кода и обнаруживает, что такой тип, как OrderedValue a -> a, неверен, потому что он игнорирует ограничение Ord a.

Однако обратите внимание, что DatatypeContexts, который позволяет накладывать ограничение на тип данных, устарел. Все согласны с тем, что лучше налагать ограничения только на те функции, которые действительно в них нуждаются. Если вы удалите ограничение Ord a из типа данных, тогда функция getOrderedValue будет хорошо компилироваться, потому что не будет Ord a ограничения, которому нужно подчиняться, и действительно, вы можете заметить, что это более точно соответствует интуиции, стоящей за исходным типом, который вы написали, который теперь правильный.

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

Например, следующая функция:

mysum = foldr (+) 0

имеет тип (Num b, Foldable t) => t b -> b, но вы можете написать:

mysum :: [Integer] -> Integer
mysum = foldr (+) 0

потому что это правильный тип для функции, хотя и более конкретный. Конечно, после того, как конкретный тип назначен для mysum, вы не сможете вызвать его с другим экземпляром Foldable или другого Num типа: вы теряете общность, когда специализируете тип.

person gigabytes    schedule 21.10.2018