Определение поведения функции по типу функции

Ответ 1

Если бы он сделал что-либо из этого, его тип изменился бы. То, что говорится в цитате, состоит в том, что, учитывая, что мы знаем, что fst имеет тип (a, b) -> a, мы можем сделать эти выводы об этом. Если бы у него был другой тип, мы бы не смогли этого сделать.

Например, см., что

snd :: (a, b) -> a
snd (x, y) = y

не проверяет тип, и поэтому мы знаем, что значение типа (a, b) -> a не может вести себя как snd.

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

Обратите внимание, в частности, на полиморфизм слов: мы не можем делать подобные выводы о неполиморфных типах. Например,

myFst :: (Int, String) -> Int
myFst (a, b) = a

но также выполняет

myFst :: (Int, String) -> Int
myFst (a, b) = 42

и даже

myFst :: (Int, String) -> Int
myFst (a, b) = length b

Параметричность в решающей степени зависит от того, что полиморфная функция не может "смотреть" на типы, с которыми она вызвана. Таким образом, единственным значением типа a, которое fst знает, является тот, который он дал: первый элемент кортежа.

Ответ 2

Дело в том, что после того, как у вас есть этот тип, варианты реализации сильно ограничены. Если вы вернули Int, то ваш тип будет (a,b) -> Int. Так как a может быть чем угодно, мы не сможем сделать это из-за шума в реализации, не прибегая к undefined, и поэтому должны вернуть тот, который нам дал вызывающий.

Ответ 3

Вы должны прочитать статью Теоремы бесплатно.

Ответ 4

Попробуем добавить еще несколько ручных масок к тому, что уже дано Real World Haskell. Попытаемся убедить себя, что, учитывая, что у нас есть функция fst с типом (a,b) -> a, единственная полная функция, которой она может быть, следующая:

fst (x,y) = x

Прежде всего, мы не можем вернуть ничего другого, кроме значения типа a, то есть в предположении, что fst имеет тип (a,b) -> a, поэтому мы не можем иметь fst (x,y) = y или fst (x,y) = 1, потому что это не имеет правильный тип.

Теперь, как говорит RWH, если я даю fst a (Int,Int), fst не знает, что это Ints, более того, a или b не должны принадлежать к любому типу классов, поэтому fst не имеет доступных значений или функций, связанных с a или b.

Так что fst знает только о значении a и значении b, которое я ему даю, и я не могу превратить b в a (он не может сделать функцию b -> a), поэтому он должен вернуть заданное значение a.

На самом деле это не просто волшебная ручная магия, можно фактически вывести, какие возможные выражения существуют для данного полиморфного типа. На самом деле существует программа под названием djinn, которая делает именно это.

Ответ 5

Дело здесь в том, что как a, так и b являются переменными типа (это может быть одно и то же, но это не нужно). Во всяком случае, поскольку для заданного набора двух элементов fst всегда возвращает первый элемент, возвращаемый тип должен всегда совпадать с типом для первого элемента.

Ответ 6

Фундаментальная вещь, которую вы, вероятно, не хватает, такова:

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

• В Haskell, если вы скажете, что "эта функция возвращает любой тип", это означает, что вызывающий получает решение о том, какой тип должен быть. (!)

Итак, если я пишу foo :: Int -> x, он не может просто вернуть String, потому что я не могу запросить его String. Я могу попросить Customer, или ThreadId, или что-нибудь еще.

Очевидно, что метод foo не знает, как создать значение любого возможного типа, даже типов, которые еще не существуют. Короче говоря, писать foo невозможно. Все, что вы попробуете, даст вам ошибки типа и не будет компилироваться.

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

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

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

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

Вы слышали выражение "в Haskell, если оно компилируется, оно обычно работает правильно"? Ну, вот почему.; -)