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

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

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

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

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

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

f () = "foo"
f [] = "bar"

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

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

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

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

class Foo a where
    foo :: a -> Integer

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

instance Foo [a] where
    foo [] = 0
    foo (x:xs) = 1 + foo xs

instance Foo Float where
    foo 5.2 = 10
    foo _ = 100

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

bar :: a -> Integer
bar x = 1 + foo x

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

bar :: Foo a => a -> Integer
bar x = 1 + foo x

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

Тип a -> Integer на самом деле не означает «функцию от любого типа до Integer», как вы ее описываете. Когда определение или выражение имеет тип a -> Integer, это означает, что для любого типа T можно специализировать или создавать экземпляр этого определения или выражения в функции типа T -> Integer.

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

-- | The polymorphic identity function (not valid Haskell!)
id :: forall a. a -> a
id = \t -> \(x :: t) -> x

Эта идея реализации полиморфизма как аргумента типа для полиморфной функции исходит из математическая структура, называемая System F , которую Хаскелл фактически использует в качестве одного из своих теоретических источников. Однако Haskell полностью скрывает идею передачи параметров типа в качестве аргументов функциям.

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

{-# LANGUAGE ScopedTypeVariables, NoMonomorphismRestriction #-}

import Data.Generics

q1 :: Typeable a => a -> Int
q1 = mkQ 0 (\s -> if s == "aString" then 100 else 0)

q2 :: Typeable a => a -> Int
q2 = extQ q1 (\(f :: Float) -> round f)

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

Prelude Data.Generics> q2 "foo"
0
Prelude Data.Generics> q2 "aString"
100
Prelude Data.Generics> q2 (10.1 :: Float)
10

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

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