Блог

Главная - Вопросы по программированию - Объяснение несоответствия поведения переменной очевидного типа в Haskell

Объяснение несоответствия поведения переменной очевидного типа в Haskell

#haskell

#haskell

Вопрос:

Раскрытие информации: я программист Scala, изучающий Haskell.

Я хотел бы немного лучше понять поведение переменной типа.

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

Почему следующий код работает над функцией:

 g :: a -> a -- a can take the concrete type Num a => a or something else like Bool
g x = x

g 10
--g 10 :: Num a => a

g True
--g True :: Bool

Однако с переменной, в отличие от функции, происходит следующая странная вещь

 e :: a
e = 1
--  No instance for (Num a) arising from the literal ‘1’
--      Possible fix:
--      add (Num a) to the context of
--        the type signature for:
--          e1 :: forall a. a
--    In the expression: 1
--    In an equation for ‘e1’: e1 = 1

То же самое, конечно, если я введу следующее в REPL

 e :: a; e = 1

Q1) Из этого, казалось бы, у нас есть разница в поведении универсального типа (т.Е. Переменной типа) между переменной и функцией? Почему это так? или что я еще не вижу или не получаю?

Теперь странная часть

Если в Repl, однако, я делаю

  e :: a; e = undefined

и затем

 e = 1

тогда я получаю

 :t e
-- e1 :: Num p => p

Таким образом, используя undefined в REPL «по крайней мере», я возвращаю поведение универсального типа для функции.

Q2) Что на самом деле здесь происходит? Для меня все это звучит не очень логично. Кто-нибудь может объяснить, пожалуйста?

Комментарии:

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

2. Хорошо, давайте посмотрим. Если вы напишете g :: a -> a; g x = 42 x , вы получите ошибку, мало чем отличающуюся от ошибки, которую вы получаете e::a . Имеет ли эта ошибка смысл для вас?

3. Вы можете просмотреть это таким образом. g :: a -> a имеет много типов. Int->Int , String->String и Bool->Bool являются всеми типами g , a->a является просто наиболее общим из этих типов. Уравнение g x = x не противоречит ни одному из этих типов. Аналогично, e :: a имеет много типов (на самом деле все возможные типы), включая Int , String , Bool и Int->Int (так что вы можете легально написать e == "abc" или e 42 ). Однако определение a = 1 не соответствует большинству из этих типов.

4. Небольшая поправка, старое определение не забыто, но сделано невидимым (оно по-прежнему доступно для других определений, которые ссылаются на старое определение).

5. Очень хорошее разъяснение, сэр!!! Спасибо. Я бы посоветовал, если у вас есть время, дать ответ на этот вопрос. Итак, (1) Я могу проголосовать, (2) и другим на моем пути, которые, возможно, сначала не поймут это, как я, было бы полезно получить официальный ответ.

Ответ №1:

Переменные типа в Haskell универсально определяются количественно. Это означает, что фактический тип g 

 g :: ∀ a . a -> a

Квантификатор обычно неявный, но вы можете фактически указать его в исходном коде Haskell (as forall ), если вы включите определенные расширения GHC.

Что это значит? Ну, буквально, g имеет тип a -> a для всех возможных значений a . То есть, g это a Bool->Boll и a String->String и Int->Int функция. Он имеет все эти типы.

Когда вы пишете g x = x , вы не нарушаете обещание, данное типом g , а именно, что аргумент может быть любого типа, и результат должен быть того же типа. Действительно, результат x и аргумент также x , и x , очевидно, имеет тот же тип, x что и .

Однако, если вы пишете g x = x 42 , это нарушает обещание. x не может быть типа Bool или String больше. Поэтому компилятор будет жаловаться.

Теперь обозначение

 e :: a

очень похожим образом следует интерпретировать как

 e :: ∀ a . a

Это означает e , что имеет тип a для всех возможных значений a . То есть у него есть все возможные типы: Int и String и Bool и Int->Int и бесконечно много других.

Вы могли бы удовлетворить тип, определив e как

 e = undefined

(и действительно, это, по сути, единственный способ удовлетворить его). Однако, если вы напишете

 e = 1

вы нарушаете обещание, данное типом e . Таким образом, вы получите ошибку того же типа, что и выше.

Если вы пишете e = undefined и после e = 1 этого, то в REPL второе определение затеняет первое, поэтому у вас есть две разные переменные с именами e , каждая из которых имеет свой собственный тип. Если вы используете REPL, вы можете переопределить любое имя в любое удобное для вас время, для этого и существует REPL! Это, конечно, невозможно в обычном модуле Haskell.