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

Question

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

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

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

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

Answer 1

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

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

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

Answer 2

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

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

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

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

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

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

Answer 4

Тип 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 полностью скрывает идею передачи параметров типа в качестве аргументов функциям.

Answer 5

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

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