Haskell проблема с рекурсией по ADT

Question

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

Идея состояла в том, чтобы попробовать собрать cons, car, cdr для пары adt, а затем написать стандартную рекурсию для вычисления длины:

data Pair a b =  NullPair | Pair { thisCar :: a, thisCdr :: b} deriving (Eq)

cons :: a -> b -> Pair a b
cons x y = Pair { thisCar = x, thisCdr = y}

car :: Pair a b -> a
car (Pair {thisCar = x, thisCdr = y}) = x

cdr :: Pair a b -> b
cdr (Pair {thisCar = x, thisCdr = y}) = y

instance (Show a, Show b) => Show (Pair a b) where
  show NullPair = "()"
  show (Pair { thisCar=x, thisCdr=y}) = "(" ++ show x ++ " . " ++ show y ++ ")" 

Пока все хорошо:

l1 = NullPair   -- ()
l2 = cons 3 NullPair  -- (3)
l3 = cons (cons 2 NullPair) (cons 3 (cons 4 NullPair))  -- ((2) 3 4)

λ> l1
()
λ> l2
(3 . ())
λ> l3
((2 . ()) . (3 . (4 . ())))
λ> car l2
3
λ> car l3
(2 . ())
λ> cdr l2
()
λ> cdr l3
(3 . (4 . ()))
λ> cdr (cdr l3)
(4 . ())

Обратите внимание, что REPL не жаловался, когда я вошел в CDR (CDR L3). Подробнее об этом чуть позже ...

Итак, вот моя функция длины (и мы предполагаем, что входные данные представляют собой набор вложенных пар, внутренняя thisCdr которых равна NullPair) и ошибка, которую я получаю, когда пытаюсь скомпилировать ее. ,

len :: Pair a b -> Integer
len NullPair = 0
len p = 1 + len $ thisCdr p

lists.hs:117:19-27: error: …
    • Couldn't match expected type ‘Pair a0 b0’ with actual type ‘b’
      ‘b’ is a rigid type variable bound by
        the type signature for:
          len :: forall a b. Pair a b -> Integer
        at /home/nate/Documents/haskell/ProblemSets/lists.hs:115:8
    • In the second argument of ‘($)’, namely ‘thisCdr p’
      In the expression: 1 + len $ thisCdr p
      In an equation for ‘len’: len p = 1 + len $ thisCdr p
    • Relevant bindings include
        p :: Pair a b
          (bound at /home/nate/Documents/haskell/ProblemSets/lists.hs:117:5)
        len :: Pair a b -> Integer
          (bound at /home/nate/Documents/haskell/ProblemSets/lists.hs:116:1)
Compilation failed.

Моя интерпретация заключается в том, что я говорю компилятору искать что-то типа Pair ab, но он находит что-то типа b и не верит мне, что b на самом деле будет стандартом. для пары а б. Также удивительно то, что у него нет проблем с cdr (cdr l3), хотя cdr возвращает значение типа b, но ожидает значение типа Pair a b.

Итак:

1. Может кто-нибудь объяснить технически, что здесь происходит? Очевидно, я не понимаю что-то о системе типов. Или, вполне возможно, мой код содержит ошибки.
2. Есть ли что-нибудь в этом роде? Может быть, лучший метод выполнения такой рекурсии?

Большое спасибо за вашу помощь.

Answer 1

Я думаю, что ваша интерпретация в основном правильная! Позвольте мне прояснить несколько вещей.

Почему не работает ваше определение len?

Сначала, когда вы объявляете функцию с переменными типа (такими как a и * 1007) * в Pair a b), ваша функция должна работать для любого выбора a или b. Вот почему в сообщении об ошибке, которое вы видите, компилятор говорит:

...
        the type signature for:
          len :: forall a b. Pair a b -> Integer
...

forall - это нечто, неявное в Haskell, когда мы пишем Pair a b.

Итак, компилятор злится на вас, потому что вы пытаетесь использовать определенный c вид b (а именно Pair a0 b0), но ваша функция не будет работать, если b будет, скажем, Int.

Почему cdr (cdr l3) работает?

Это потому, что компилятор знает тип l3. Когда вы применяете cdr к нему, вы получаете что-то вроде Pair a b, так что второе приложение работает.

Вы можете попросить компилятор определить, какими будут типы этих функций. Обратите внимание, что им требуется более конкретный тип c, чем просто Pair a b.

Prelude> cddr x = cdr (cdr x)
Prelude> :t cddr
cddr :: Pair a1 (Pair a2 b) -> b
Prelude> caddr x = car (cdr (cdr x))
Prelude> :t caddr
caddr :: Pair a1 (Pair a2 (Pair a3 b)) -> a3

. Ситуация несколько усложняется тем, что компилятор делает вывод, что NullPair имеет очень общий тип forall a b. Pair a b. Когда он передается как аргумент , a и b могут быть выбраны так, чтобы проверялся тип выражения. Таким образом, любое произвольное использование car и cdr s на NullPair, как car (car (cdr NullPair)), будет проверять тип. Между этими forall s существует двойственность, когда они передаются функциям и когда их ожидают функции. Но если это объяснение сбивает с толку, вы можете игнорировать его сейчас.

Как обойти это?

Я бы порекомендовал сделать ваш тип данных явно рекурсивным. Это теряет некоторую общность в том, как вы можете использовать тип данных Pair, но в противном случае было бы сложно написать len.

data Pair a = NullPair | Pair{ thisCar :: a, thisCdr :: Pair a }

Теперь любая функция, которую вы пишете, будет знать, что thisCdr имеет форма Pair a.

(Вы можете заметить, что это просто определение списков с разными именами).

Если вы действительно хотите оставить определение Pair одинаковым

Я бы не рекомендовал это, но если вы действительно хотите сохранить свое определение Pair таким же, вот как вы можете это исправить.

Определите тип данных

data Fix f = Fix (f (Fix f))

Имя Fix является обычным (насколько я могу судить) для такого типа данных; Я не называю это, потому что это решение вашей проблемы. Вы можете рассматривать его как тип данных «рекурсия» (если вы знаете о функции fix, это ее аналог для типов).

Теперь мы можем использовать ее для рекурсия в Pair.

len :: Fix (Pair a) -> Integer
len (Fix NullPair) = 0
len (Fix p) = 1 + (len $ thisCdr p)

Если бы мы исследовали тип p, мы бы увидели, что это p :: Pair a (Fix (Pair a)). В общем, что-то типа Fix (Pair a) выглядит как

Fix (Pair a) = Fix (Pair a (Fix (Pair a)))
             = Fix (Pair a (Fix (Pair a (Fix (Pair a)))))
             = ...

Это дает нам «бесконечный тип», на который компилятор жаловался в вашем первом определении len. Хотя я использую кавычки, поскольку тип может быть записан конечным образом.

Обратите внимание, что Fix (Pair a) эквивалентно явно рекурсивному определению Pair, которое я предложил в разделе выше. Таким образом, в некотором смысле это то же самое решение, только с рекурсивным типом данных, сделанным более явным (или, может быть, запутанным).

Answer 2

1 + len $ thisCdr p

анализируется как

(1 + len) $ (thisCdr p)

Как вы можете догадаться, попытка добавить 1 к функции len не имеет большого смысла, а применение результата как функции почти безнадежно. То, что вы хотите, это

1 + len (thisCdr p)