Почему определение функций для всех типов одновременно не разрешено в Haskell?
==============================================================================

Это, наверное, очень простой вопрос, но ...

Функция, которая определена как, скажем,

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

Но Haskell позволяет только общее определение, как`foo a = 0`. 

И даже если вы ограничиваете`a` быть одним из определенного класса типов, например экземпляра класса типов Show:

Вы все еще не можете сделать что-то вроде

даже если`"hello" :: [Char]` является примером`Show`

Почему существует такое ограничение?

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

Почему это хорошо? Это дает гораздо более сильные инварианты о программах. Например, по одному только типу вы знаете, что`a -> a` должна быть функция идентичности (или расходится). Подобные «свободные теоремы» применяются ко многим другим полиморфным функциям. Параметричность также является основой для более продвинутых методов абстракции на основе типов. Например, тип`ST s a` в Haskell (государственная монада) и тип соответствующего`runST` функция, положиться на`s` будучи параметрическим. Это гарантирует, что у запущенной функции нет возможности связываться с внутренним представлением состояния.

Это также важно для эффективной реализации. Программа не должна передавать дорогостоящую информацию о типе во время выполнения (type erasure), и компилятор может выбирать перекрывающиеся представления для разных типов. Как пример последнего, 0 и False и () и [] все представлены 0 во время выполнения. Это было бы невозможно, если бы была разрешена такая функция, как ваша.



 известную как «стирание типа»: типы не имеют вычислительного значения, поэтому код, который вы генерируете, не должен их отслеживать. Это значительное благо для производительности.

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

тогда это свойство не будет правдой: поведение`f` будет действительно зависеть от типа его первого аргумента.

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



`a -> Integer` допускается только одно поведение - возвращать постоянное целое число. Зачем? Потому что вы не знаете, какой тип`a` является. Без заданных ограничений это может быть абсолютно что угодно, а поскольку Haskell статически типизирован, вам нужно разрешить все, что связано с типами во время компиляции. Во время выполнения информация о типе больше не существует и, следовательно, с ней невозможно ознакомиться - все варианты выбора используемых функций уже сделаны.

Наиболее близким Haskell к такому поведению является использование классов типов - если вы создали класс типов, называемый`Foo` с одной функцией:

Тогда вы можете определить экземпляры этого для разных типов

Тогда, пока вы можете гарантировать какой-то параметр`x` это`Foo` ты можешь позвонить`foo` в теме. Это все еще нужно, хотя - тогда вы не можете написать функцию

Поскольку компилятор не знает, что`a` является примером`Foo`, Вы должны сказать это, или опустить сигнатуру типа и позволить ей понять это для себя.

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



 Хаскелл может это сделать! (хотя это обычно используется только в очень определенных обстоятельствах)

Загрузите это и поэкспериментируйте с этим:

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

Большинство так называемых обобщенных функций (например, SYB) полагаются на`Typeable` или`Data` ограничение. Некоторые пакеты вводят свои собственные альтернативные функции, которые служат по существу той же цели. Без чего-либо подобного этим классам это невозможно сделать.



`a -> Integer` на самом деле не означает "функцию отany введите в`Integer`& Quot; как вы это описываете. Когда определение или выражение имеет тип`a -> Integer`, это означает, что для любого типа`T`можно**specialize** или же**instantiate** это определение или выражение в функцию типа`T -> Integer`.

Слегка переключая нотацию, можно думать об этом так:`foo :: forall a. a -> Integer` действительно функцияtwo аргументы: тип`a` и значение этого типа`a`, Или, с точки зрения карри,`foo :: forall a. a -> Integer` это функция, которая принимает тип`T` в качестве аргумента, и производит специализированную функцию типа`T -> Integer` для этого`T`, Используя функцию тождества в качестве примера (функция, которая создает свой аргумент в качестве результата), мы можем продемонстрировать это следующим образом:

Эта идея реализации полиморфизма как аргумента типа для полиморфной функции исходит из математической структуры, называемой[Система F](http://en.wikipedia.org/wiki/System_F), который Хаскель фактически использует в качестве одного из своих теоретических источников. Однако Haskell полностью скрывает идею передачи параметров типа в качестве аргументов функциям.