Tricky тип подписи для пар обращенных пар

Question

Допустим, у меня есть следующий тип данных:

data D a b = D (a,b) (b,a) 

И я хочу, чтобы определить следующую функцию на нем:

apply f (D x y) = D (f x) (f y) 

Что тип подписи от apply?

Вот некоторые примеры f которые хорошо:

f :: a -> a -- OK 
f :: (a, b) -> (b, a) -- OK 
f :: (a, b) -> ((a, c), (b, c)) -- OK 

Во всех вышеперечисленных случаях, мы в конечном итоге с действительным типом Д.

Но это не в порядке:

f :: (a, b) -> (a, a) 

Потому что, когда мы отправляем такую ​​функцию через apply, нам приходится пытаться построить D (a,a) (b,b), который недействителен, если a = b.

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

типизированные Отверстия Edit:

В попытке найти тип с помощью типизированных отверстий, я попытался следующие:

x = apply _ (D (1::Int,'a') ('b',2::Int)) 

И получил:

Found hole ‘_’ with type: (Int, Int) -> (b, b) 
Where: ‘b’ is a rigid type variable bound by 
      the inferred type of x :: D b b 

который, кажется, я не понимаю, как f :: (Int, Int) -> (b, b) явно не будет работать здесь.

Answer 1

Несколько типов подходят apply, но вывод ((t, t) -> (b, b)) -> D t t -> D b b является наиболее разумным и полезным. Альтернативы будут более высокого ранга, поэтому давайте включим, что расширение языка:

{-# LANGUAGE RankNTypes #-} 

Первое, мы можем сделать apply id работы:

apply :: (forall a. a -> a) -> D a b -> D a b 
apply f (D x y) = D (f x) (f y) 

Однако теперь id является только функция который работает apply (все общие функции типа forall a. a -> a равны id).

Вот еще один тип:

apply :: (forall a. a -> (c, c)) -> D a b -> D c c 
apply f (D x y) = D (f x) (f y) 

Но это тоже происходит по цене. Теперь f -s могут быть только постоянными функциями, которые игнорируют предыдущие поля D. Итак, apply (const (0, 0)) работает, но мы не можем проверить аргумент f.

Напротив, выведенный тип довольно полезен. Мы можем выразить с ним преобразования, которые рассматривают фактические данные, содержащиеся в D.

На этом этапе мы можем спросить: почему GHC делает вывод о том, что он представляет? В конце концов, некоторые функции работают с альтернативными типами, но не работают с типом по умолчанию. Может ли быть лучше иногда выводить более ранжированные типы? Ну, такие типы часто чрезвычайно полезны, но вывод их неосуществим.

Тип вывода для классов ранга-2 довольно сложный и не очень практичный, поскольку невозможно вывести наиболее общие типы. При заключении ранжирования 1 мы можем сделать более общий тип, чем все другие допустимые типы для одного и того же выражения. Таких гарантий у ранга 2 нет. И вывод для классов 3-го и 3-го классов - это только undecidable.

По этим причинам GHC придерживается определения 1-го ранга, поэтому он никогда не вводит типы с аргументами функции forall -s.

Answer 2

Принимая вещи в крайности общности, мы хотим, чтобы тип, который выглядит как

apply :: tf -> D a b -> D c d 

где tf представляет тип f. Для того, чтобы применить f к (a,b) и получить (c,d), нам нужно

tf ~ (a,b) -> (c,d) 

Для того, чтобы применить f к (b,a), чтобы получить (d,c), нам нужно

tf ~ (b,a) -> (d,c) 

Если мы включаем TypeFamilies (или GADTs) мы получим магическое ограничение, мы должны выразить это:

{-# LANGUAGE TypeFamilies #-} 

apply :: (((a,b) -> (c,d)) ~ tf, 
      ((b,a) -> (d,c)) ~ tf) => 
     tf -> D a b -> D c d 

Я подозреваю, что это один из самых распространенных типов. К сожалению, это довольно дико; работая через то, будет ли конкретное приложение проходить проверку типа, не всегда так просто. Следует также отметить, что по причинам, лично я не понимаю, вы не можете надежно определить специализацию с помощью

apply' :: ... 
apply' = apply 

Вместо этого, вы должны иногда использовать

apply' f = apply f