Как определить тип конструктора списка, закодированного Скоттом?

Question

Списки, закодированные по Скотту, можно определить следующим образом:

      newtype List a =
    List {
      uncons :: forall r. r -> (a -> List a -> r) -> r
    }

В отличие от версии ADT, это и тип, и конструктор данных. Кодировка Скотта определяет АТД посредством сопоставления с образцом, что, по сути, означает удаление одного уровня конструкторов. Вот полная операция без неявных аргументов:

      uncons :: r -> (a -> List a -> r) -> List a -> r
--    Nil ^    ^^^^^^^^^^^^^^^^^^ Cons
uncons nil cons (List f) = f nil cons

Это имеет смысл. принимает константу, продолжение и Listи производит любую ценность.

Однако тип конструктора данных не имеет для меня особого смысла:

      List :: (forall r. r -> (a -> List a -> r) -> r) -> List a

Я вижу, что у этого есть своя область применения, но это не очень полезно. Почему rа также List aперевернулся по сравнению с uncons? И зачем дополнительные скобки в LHS?

Я, наверное, путаю тип и уровень термина здесь.

Answer 1

Что такое? Как вы говорите, это вещь, которая при наличии константы (что делать, если список пуст) и продолжения (что делать, если список не пуст), делает одну из этих вещей. В типах он принимает и и производит .

Итак, как нам составить список? Что ж, нам нужна функция, которая лежит в основе такого поведения. То есть нам нужна функция, которая сама принимает и a -> List a -> rи что-то с ними делает (предположительно, либо возвращает напрямую, либо вызывает функцию на каком-то aа также List a). Тип этого будет выглядеть примерно так:

      List :: (r -> (a -> List a -> r) -> r) -> List a
--         ^ the function that _takes_ the nil and continuation and does stuff with them

Но это не совсем правильно, что становится ясно, если мы используем явное:

      List :: forall a r. (r -> (a -> List a -> r) -> r) -> List a

Помните, что должна быть возможность работать для любого , но с этой функцией на самом деле предоставляется заранее. Действительно, нет ничего плохого в том, что кто-то специализируется на этом типе, скажем, , что приводит к:

      List :: forall a. (Int -> (a -> List a -> Int) -> Int) -> List a

Но это нехорошо! Это только когда-либо сможет производить Intс! Вместо этого мы ставим forall внутри первого набора круглых скобок, указывая, что создатель Listдолжна предоставлять функцию, которая может работать на любом rа не конкретное. Это дает тип:

      List :: (forall r. r -> (a -> List a -> r) -> r) -> List a

Answer 2

^{(Мой комментарий перенесен в этот ответ по запросу.)}

Данный

      newtype List a =
    List {
      uncons :: forall r. r -> (a -> List a -> r) -> r
    }

давайте запишем несколько списков. Обратите внимание, что списки по сути являются функциями двух параметров ( \nil cons -> ...).

      -- []
empty = List (\nil _ -> nil)

-- [True]
-- True : []
-- (:)  True []
-- cons True nil
list1 = List (\_ cons -> cons True (List (\nil _ -> nil)))

-- [True, False]
-- True : False : []
-- (:)  True ((:)  False [])
-- cons True (cons False nil)
list2 = List (\_ cons -> 
           cons True (List (\_ cons' -> 
               cons' False (List (\nil _ -> nil)))))