Сигнатура типа Haskell от u f = f.f сильнее, чем хотелось бы
Я написал следующую простую функцию
u f=f.f
В соответствии с ghci это имеет сигнатуру типа
u :: (b -> b) -> b -> b
Однако эта подпись типа слишком строгая. Haskell гарантирует, что наш ввод будет иметь тип (b -> b), когда это не обязательно должно быть. Например, функция (:[]) имеет сигнатуру типа
(:[]) :: a -> [a]
Это не форма (b -> b) (если вы не разрешаете бесконечные типы) и, следовательно, не может быть передана u. Однако вы можете составить (:[]) с собой.
g=(:[]).(:[])
Это работает и имеет тип
(:[]).(:[]) :: a -> [[a]]
Поэтому я должен в принципе передать это u.
Я попытался написать новую подпись типа, чтобы заменить сгенерированную подпись, но я не мог придумать способ выражения требований функции. Я всегда придумываю подпись того же типа, которую предоставляет компилятор. Есть ли сигнатура типа, которую мы можем дать, чтобы ослабить u, чтобы функции, подобные (:[]), могли быть переданы ей?
Ответы
Ответ 1
Существует множество различных функций, которые могут делать это для конкретных случаев, но не работают в целом.
u1 :: (forall a. a -> f a) -> b -> f (f b)
u2 :: (forall a. f a -> a) -> f (f b) -> b
и бесконечно больше. Но функция
u f x = f (f x)
не имеет самого общего типа в Haskell, когда RankNTypes находится в игре. Как отмечает заводчик, существуют системы типов, которые могут дать u принципиальный тип желаемого типа, но они принимают расширение системы типов в совершенно другом направлении от тех, на которые ориентировались дизайнеры Haskell.
