"По-настоящему" общая функция в Haskell
Предположим, что у меня есть составной тип данных -
data M o = M (String,o)
Теперь я могу определить функцию, которая работает для ВСЕХ M
, независимо от o
. Например -
f :: M o -> M o
f (M (s,o)) = M (s++"!", o)
Однако f
на самом деле не такой общий, как хотелось бы. В частности, использование f
в выражении фиксирует тип o
, поэтому я не могу использовать f
снова с другим типом o
. Например, следующее: typecheck -
p f = undefined where
m1 = M ("1", ())
m2 = M ("2", True)
m1' = f m1
m2' = f m2
Выдает ошибку - Couldn't match expected type 'Bool' with actual type '()'
Удивительно, но если я не предоставляю f в качестве аргумента и вместо этого просто использую глобальное определение f, то он компилируется и работает отлично! т.е. компилирует -
p = undefined where
m1 = M ("1", ())
m2 = M ("2", True)
m1' = f m1
m2' = f m2
Есть ли для этого конкретная причина? Как я могу обойти эту проблему, то есть определить функцию f
, которая может быть применена ко всем (M o)
, даже если o
изменяется в одном выражении? Я предполагаю, что здесь существуют экзистенциальные типы, но я просто не могу понять, как это сделать.
Ответы
Ответ 1
Проблема заключается в том, что компилятор не может правильно определить тип p. Вы должны будете дать ему подпись типа:
p :: (forall o. M o -> M o) -> a
Это тип ранга 2, поэтому вам потребуется расширение языка:
{-# LANGUAGE Rank2Types #-}
или
{-# LANGUAGE RankNTypes #-}
Подробнее об этом читайте здесь: http://www.haskell.org/haskellwiki/Rank-N_types
Ответ 2
Есть ли для этого конкретная причина?
Действительно, есть одно. Чтобы сказать это в одном предложении: вывод типа не будет работать должным образом, если вы снимете ограничение системы HM, что аргументы лямбда должны быть мономорфными.
Саймон Пейтон Джонс разработал средство проверки типов, которое расширяет HM и допускает более высокий уровень полиморфизма. Но в таких случаях требуются аннотации явного типа. См. Ответ Sjoerds.
Ответ 3
f
f
не совпадает с функцией верхнего уровня f
. Это любая функция, заданная в качестве аргумента при вызове p
. Поскольку вы не дали p
сигнатуру типа, компилятор должен определить, что f
от того, как вы его используете. Первое использование означает, что f :: M () -> M ()
, что означает p :: (M () -> M ()) -> a
. Как сказал кто-то другой, вы должны дать p
явную подпись, используя forall
, чтобы сделать то, что вы пытаетесь сделать.