Необходимость обертки экзистенциального типа

Оказывается, на удивление сложно правильно использовать экзистенциальные типы/типы ранга n, несмотря на очень простую идею, стоящую за ними.

Почему необходимо оборачивать экзистенциальные типы в data типы?

У меня есть следующий простой пример:

{-# LANGUAGE RankNTypes, ImpredicativeTypes, ExistentialQuantification #-}
module Main where

c :: Double
c = 3

-- Moving `forall` clause from here to the front of the type tuple does not help,
-- error is the same
lists :: [(Int, forall a. Show a => Int -> a)]
lists = [ (1, \x -> x)
        , (2, \x -> show x)
        , (3, \x -> c^x)
        ]

data HRF = forall a. Show a => HRF (Int -> a)

lists' :: [(Int, HRF)]
lists' = [ (1, HRF $ \x -> x)
         , (2, HRF $ \x -> show x)
         , (3, HRF $ \x -> c^x)
         ]

Если я закомментирую определение lists, код успешно скомпилируется. Если я не прокомментирую это, я получаю следующие ошибки:

test.hs:8:21:
    Could not deduce (a ~ Int)
    from the context (Show a)
      bound by a type expected by the context: Show a => Int -> a
      at test.hs:8:11-22
      `a' is a rigid type variable bound by
          a type expected by the context: Show a => Int -> a at test.hs:8:11
    In the expression: x
    In the expression: \ x -> x
    In the expression: (1, \ x -> x)

test.hs:9:21:
    Could not deduce (a ~ [Char])
    from the context (Show a)
      bound by a type expected by the context: Show a => Int -> a
      at test.hs:9:11-27
      `a' is a rigid type variable bound by
          a type expected by the context: Show a => Int -> a at test.hs:9:11
    In the return type of a call of `show'
    In the expression: show x
    In the expression: \ x -> show x

test.hs:10:21:
    Could not deduce (a ~ Double)
    from the context (Show a)
      bound by a type expected by the context: Show a => Int -> a
      at test.hs:10:11-24
      `a' is a rigid type variable bound by
          a type expected by the context: Show a => Int -> a at test.hs:10:11
    In the first argument of `(^)', namely `c'
    In the expression: c ^ x
    In the expression: \ x -> c ^ x
Failed, modules loaded: none.

Почему это происходит? Разве второй пример не должен быть эквивалентен первому? В чем разница между этими вариантами использования n-ранговых типов? Можно ли вообще отказаться от дополнительного определения ADT и использовать только простые типы, когда мне нужен такой полиморфизм?


polymorphism haskell existential-type higher-rank-types
person Vladimir Matveev    schedule 03.06.2012    source источник

Ответы (3)


arrow_upward
3
arrow_downward

При обработке экзистенциальных типов необходимо учитывать две проблемы:

  • Если вы храните «все, что может быть shown», вы должны сохранить то, что можно показать, а также как это показать.
  • Фактическая переменная может иметь только один единственный тип.

Во-первых, почему у вас должны быть оболочки экзистенциального типа, потому что когда вы пишете это:

data Showable = Show a => Showable a

Что на самом деле происходит, так это то, что объявляется что-то вроде этого:

data Showable a = Showable (instance of Show a) a

т.е. ссылка на экземпляр класса Show a сохраняется вместе со значением a. Без этого у вас не может быть функции, которая разворачивает Showable, потому что эта функция не знает, как показать a.

Второй момент заключается в том, почему вы иногда получаете некоторую причудливость типов и почему вы не можете связать экзистенциальные типы, например, в let привязках.

У вас также есть проблема с вашими рассуждениями в вашем коде. Если у вас есть такая функция, как forall a . Show a => (Int -> a), вы получаете функцию, которая, учитывая любое целое число, сможет создать любое отображаемое значение, которое выберет вызывающая сторона. Вероятно, вы имеете в виду exists a . Show a => (Int -> a), имея в виду, что если функция получает целое число, она вернет некоторый тип, для которого существует экземпляр Show.

person dflemstr    schedule 03.06.2012
comment
Большое спасибо за ваше объяснение. Все ответы были чрезвычайно полезны, но я думаю, что в вашем ответе мне не хватает кусочков головоломки, поэтому я отмечаю его как принятый. - person Vladimir Matveev; 03.06.2012

arrow_upward
6
arrow_downward

Ваша первая попытка не использовать экзистенциальные типы. Скорее ваш

lists :: [(Int, forall a. Show a => Int -> a)]

требует, чтобы вторые компоненты могли предоставить элемент любого отображаемого типа, который я выберу, а не только какой-то отображаемый тип, который вы выберете. Ты ищешь

lists :: [(Int, exists a. Show a * (Int -> a))]  -- not real Haskell

но это не то, что вы сказали. Метод упаковки типов данных позволяет восстановить exists из forall путем каррирования. У тебя есть

HRF :: forall a. Show a => (Int -> a) -> HRF

это означает, что для построения значения HRF необходимо предоставить тройку, содержащую тип a, словарь Show для a и функцию в Int -> a. То есть тип конструктора HRF фактически кардинирует этот нетип

HRF :: (exists a. Show a * (Int -> a)) -> HRF   -- not real Haskell

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

type HRF = forall x. (forall a. Show a => (Int -> a) -> x) -> x

но это наверное перебор.

person pigworker    schedule 03.06.2012

arrow_upward
3
arrow_downward

Примеры не эквивалентны. Первый,

lists :: [(Int, forall a. Show a => Int -> a)]

говорит, что каждый второй компонент может создавать любой желаемый тип, если он является экземпляром Show из Int.

Второй пример по модулю эквивалентен оболочке типа

lists :: [(Int, exists a. Show a => Int -> a)]

т. е. каждый второй компонент может создать некоторый тип, принадлежащий Show, из Int, но вы понятия не имеете, какой тип возвращает эта функция.

Кроме того, функции, которые вы помещаете в кортежи, не удовлетворяют первому контракту:

lists = [ (1, \x -> x)
        , (2, \x -> show x)
        , (3, \x -> c^x)
        ]

\x -> x в качестве результата выдает тот же тип, что и в качестве входных данных, так что здесь это Int. show всегда производит String, так что это один фиксированный тип. наконец, \x -> c^x производит тот же тип, что и c, а именно Double.

person Daniel Fischer    schedule 03.06.2012