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

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

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

foo :: a -> Integer

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

foo 1 = 10
foo 5.3 = 100
foo (x:xs) = -1
foo  _     = 0

Но Haskell допускает только общее определение, например foo a = 0.

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

foo :: (Show a) => a -> Integer

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

foo "hello" = 10
foo   _     = 0

хотя "hello" :: [Char] является экземпляром Show

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

Ответ 1

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

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

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

Ответ 2

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

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

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

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

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

Ответ 3

Для функции 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 может работать только с такой информацией, как у компилятора о типе чего-то. Это может звучать ограничительно, но на практике модели и параметрический полиморфизм настолько мощные, что я никогда не пропускаю динамическую типизацию. На самом деле я обычно нахожу динамический ввод текста раздражающим, потому что я никогда не полностью уверен, что на самом деле есть.

Ответ 4

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

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

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

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

Ответ 5

Этот вопрос основан на ошибочной предпосылке, 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. Некоторые пакеты представляют свои собственные альтернативные функции, которые служат по существу той же цели. Без чего-то подобного этим классам это невозможно сделать.