RankNTypes: применить ту же функцию для пар различных типов

Question

Я пытался определить эту функцию, чтобы перегруппировать три списка пар:

{-# LANGUAGE RankNTypes #-} 

mapAndZip3 :: (forall x. x -> f x) -> [a] -> [b] -> [c] 
            -> [(f a, f b, f c)] 
mapAndZip3 f la lb lc = zipWith3 (\a b c -> (f a, f b, f c)) la lb lc 


main = do 
    let x = mapAndZip3 (fst) [(1,"fruit"), (2,"martini")] 
          [("chips","fish"),("rice","steak")] 
          [(5,"cake"),(4,"pudding")] 
    print x -- was expecting [(1,"chips",5), (2,"rice",4)] 

Сначала я не включил RankNTypes или в forall, но потом после определения this, а именно определения liftTup, я думал, что этого должно быть достаточно.

Но ясно, что это не было, так как я все еще получаю ошибку:

mapAndZip3.hs:8:25: 
Couldn't match type `x' with `(f0 x, b0)' 
    `x' is a rigid type variable bound by 
     a type expected by the context: x -> f0 x at mapAndZip3.hs:8:13 
Expected type: x -> f0 x 
    Actual type: (f0 x, b0) -> f0 x 
In the first argument of `mapAndZip3', namely `(fst)' 

Я четко иметь ограниченное понимание forall ключевого слова, но от того, что я понял, что должен в этом случае позволяют для f принять любой тип. Я не понимаю: один раз в данном контексте и используется один раз, определяет ли определение «фиксированный» для оставшегося контекста?

Это не похоже, потому что, если я заменю «чипы» и «рис» на Интс, компилятор все еще жалуется, поэтому я предполагаю, что я принимаю что-то неправильно (конечно, если я удалю аннотацию типа mapAndZip3 в этом последнем случае все работает, потому что подпись упрощается до mapAndZip3 :: (a -> t) -> [a] -> [a] -> [a] -> [(t, t, t)], но это не то, что я хочу).

Я также нашел эту question, но не могу сделать, если это та же проблема или нет, так как функция Я пытаюсь применить не id, но fst или snd, функции, которые на самом деле возвращают различные типы (a -> b).

Answer 1

Проблема в вашей подписи - f. Давайте расширим это немного:

mapAndZip3 :: forall (a :: *) (b :: *) (c :: *) (f :: *->*) 
      => (forall x. x -> f x) -> [a] -> [b] -> [c] 
           -> [(f a, f b, f c)] 

f здесь должен быть «любой функцией типа уровня», в вашей конкретизации было бы type f (a,b) = a. Но Haskell не позволяет вам абстрагироваться от функций уровня типа, только над конструкциями типа , например Maybe или IO. Таким образом, mapAndZip3 Just на самом деле было бы возможно, но fst не строится, но deconstruct тип кортежа.

Функции уровня на самом деле даже не существуют в Haskell98, они возможны только с TypeFamilies. Проблема в основном в том, что родной язык Haskell является нетипизированным , но функции уровня уровня должны быть полными функциями . Но тогда вы не можете определить какую-либо нетривиальную функцию (то есть, кроме id или конструкторов типов), которая определена для всех типов. Тип уровня fst, конечно, не является полным, он работает только с типами кортежей.

Чтобы работать с такими функциями, вам явно необходимо указать их контекст каким-либо другим способом. С TypeFamilies она могла бы работать так:

class TypeFunctionDomain d where 
    type TypeFunction d :: * 

instance TypeFunctionDomain (a,b) where 
    type TypeFunction (a,b) = a 

mapAndZip3 :: (forall x. TypeFunctionDomain x => x -> TypeFunction x) 
      -> [a] -> [b] -> [c] 
        -> [(TypeFunction a, TypeFunction b, TypeFunction c)] 

Однако, это не совсем то, что вы хотите: это не было бы возможным определить в том же объеме, также TypeFunctionDomain например corrsponding к snd, а это означает, что mapAndZip3 эффективно Wouldn вообще не полиморфны, но работают только с одной функцией.

Эти проблемы могут быть решены только правильно в зависимым от типизированных языков, таких какAgda, где виды действительно являются только типы типов, и вы можете определить функции типа уровня просто, а также функции значение уровня. Но это как-то вроде цены: все функции должны быть полными функциями! Это не очень плохо, но это означает, что эти языки вообще не являются действительно Turing-complete (что потребует возможности бесконечного цикла/рекурсии, но, тем не менее, ⟂ в отношении полной оценки результата).

---

Все изменилось немного с появлением kind polymorphism etc..

Это, в отличие от, например, C++, который позволяет - хотя и с очень ужасным синтаксисом - duck-typed функции уровня, через шаблоны. Это может быть довольно приятной особенностью, но одним из следствий является то, что вы часто получаете полностью нечитаемые сообщения об ошибках (с еще меньшим отношением к реальной проблеме, чем худшие подсказки «Возможные исправления» GHC ...) при попытке создать шаблон с помощью аргумент типа вне неявного домена.

Answer 2

Проблема заключается в том, что fst не имеет требуемого типа

(forall x. x -> f x) 

Тип fst является

fst :: (a, b) -> a 

и a не в форме f (a,b). f есть переменная, которая должна быть создана с помощью конструктора типов, что-то вроде [], Maybe, Either Bool. f не может стоять ни для какой «функции типа», как Λ (a,b) -> a, он должен быть конструктором типа.

Это работает, если мы предоставляем ему функцию требуемого типа (извините, глупый пример):

{-# LANGUAGE RankNTypes #-} 

mapAndZip3 :: (forall x. x -> f x) -> [a] -> [b] -> [c] 
            -> [(f a, f b, f c)] 
mapAndZip3 f la lb lc = zipWith3 (\a b c -> (f a, f b, f c)) la lb lc 

fst0 x = (True,x) 

main = do 
    let x = mapAndZip3 (fst0) [(1 :: Int,"fruit"), (2,"martini")] 
          [("chips","fish"),("rice","steak")] 
          [(5 :: Int,"cake"),(4,"pudding")] 
    print x 

поскольку здесь fst0 имеет тип a -> ((,) Bool) a, который имеет форму x -> f x.