Что означает "существует" в системе типа Haskell?

Я пытаюсь понять ключевое слово exists по отношению к системе типа Haskell. Насколько мне известно, в Haskell по умолчанию нет такого ключевого слова, но:

расширения, которые их добавляют, в объявлениях, подобных этим data Accum a = exists s. MkAccum s (a -> s -> s) (s -> a)
Я видел документ о них и (если я правильно помню), он заявил, что ключевое слово exists не нужно для системы типов, поскольку оно может быть обобщено на forall

Но я даже не понимаю, что означает exists.

Когда я говорю, forall a . a -> Int, это означает (по моему мнению, неправильный, я думаю) "для каждого (типа) a, существует функция типа a -> Int":

myF1 :: forall a . a -> Int
myF1 _ = 123
-- okay, that function (`a -> Int`) does exist for any `a`
-- because we have just defined it

Когда я говорю exists a . a -> Int, что это может означать? "Существует хотя бы один тип a, для которого существует функция типа a -> Int"? Зачем писать такое выражение? Какая цель? Семантика? Поведение компилятора?

myF2 :: exists a . a -> Int
myF2 _ = 123
-- okay, there is at least one type `a` for which there is such function
-- because, in fact, we have just defined it for any type
-- and there is at least one type...
-- so these two lines are equivalent to the two lines above

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

P.S. Я не совсем новичок в Haskell (возможно, как второй грейдер), но мои математические основы этих вещей не хватает.

Ответ 1

Использование экзистенциальных типов, с которыми я столкнулся, с моим кодом для опосредования игры в Clue.

Мой код посредничества действует как дилер. Неважно, какие типы игроков - все, о чем он заботится, состоит в том, что все игроки реализуют крючки, указанные в классе Player.

class Player p m where
  -- deal them in to a particular game
  dealIn :: TotalPlayers -> PlayerPosition -> [Card] -> StateT p m ()

  -- let them know what another player does
  notify :: Event -> StateT p m ()

  -- ask them to make a suggestion
  suggest :: StateT p m (Maybe Scenario)

  -- ask them to make an accusation
  accuse :: StateT p m (Maybe Scenario)

  -- ask them to reveal a card to invalidate a suggestion
  reveal :: (PlayerPosition, Scenario) -> StateT p m Card

Теперь дилер мог сохранить список игроков типа Player p m => [p], но это сжимало бы все игроки должны быть одного типа.

Это слишком констриктивно. Что делать, если я хочу иметь разных игроков, каждый из которых выполнен по-разному, и запускать их друг против друга?

Поэтому я использую ExistentialTypes для создания обертки для игроков:

-- wrapper for storing a player within a given monad
data WpPlayer m = forall p. Player p m => WpPlayer p

Теперь я могу легко сохранить разнородный список игроков. Дилер все еще может легко взаимодействовать с игроков, использующих интерфейс, указанный классом Player.

Рассмотрим тип конструктора WpPlayer.

    WpPlayer :: forall p. Player p m  => p -> WpPlayer m

Кроме передней панели, это довольно стандартный haskell. Для всех типов p, удовлетворяющих контракту Player p m, конструктор WpPlayer отображает значение типа p к значению типа WpPlayer m.

Интересный бит содержит деконструктор:

    unWpPlayer (WpPlayer p) = p

Какой тип unWpPlayer? Это работает?

    unWpPlayer :: forall p. Player p m => WpPlayer m -> p

Нет, не совсем. Букет из разных типов p мог бы удовлетворить контракт Player p m с определенным типом m. И мы дали конструктору WpPlayer конкретный type p, поэтому он должен возвращать тот же самый тип. Поэтому мы не можем использовать forall.

Все, что мы действительно можем сказать, это то, что существует некоторый тип р, удовлетворяющий условию Player p m с типом m.

    unWpPlayer :: exists p. Player p m => WpPlayer m -> p

Ответ 2

Когда я говорю, forall a. a → Int, it означает (по моему мнению, неправильный, я думаю) "для каждого (типа) a, существует функция type a → Int":

Закрыть, но не совсем. Это означает, что для каждого типа a эту функцию можно считать имеющей тип a → Int ". Таким образом, a может быть специализирован для любого типа выбора вызывающего.

В случае "существует" мы имеем: "существует некоторый (конкретный, но неизвестный) тип a, такой, что эта функция имеет тип a → Int". Таким образом, a должен быть определенного типа, но вызывающий не знает, что.

Обратите внимание, что это означает, что этот конкретный тип (exists a. a -> Int) не так уж и интересен - нет полезного способа вызвать эту функцию, кроме как передать "нижнее" значение, такое как undefined или let x = x in x. Более полезной сигнатурой может быть exists a. Foo a => Int -> a. В нем говорится, что функция возвращает определенный тип a, но вы не узнаете, какой тип. Но вы знаете, что это экземпляр Foo, поэтому вы можете сделать что-то полезное с ним, несмотря на то, что не знаете его "истинного" типа.

Ответ 3

Это означает, что "существует тип a, для которого я могу предоставить значения следующих типов в моем конструкторе". Обратите внимание, что это отличается от того, что "значение a есть Int в моем конструкторе"; в последнем случае я знаю, что такое тип, и я мог бы использовать свою собственную функцию, которая принимает Int в качестве аргументов, чтобы сделать что-то еще для значений в типе данных.

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

Именно по этой причине следующий тип не очень полезен:

data Useless = exists s. Useless s

Потому что я ничего не могу сделать для значения (не совсем верно, я мог бы seq его); Я ничего не знаю о его типе.

Ответ 4

UHC реализует ключевое слово exist. Вот пример из его документации

x2 :: exists a . (a, a -> Int)
x2 = (3 :: Int, id)

xapp :: (exists b . (b,b -> a)) -> a
xapp (v,f) = f v

x2app = xapp x2

И еще:

mkx :: Bool -> exists a . (a, a -> Int)
mkx b = if b then x2 else ('a',ord)

y1 = mkx True -- y1 :: (C_3_225_0_0,C_3_225_0_0 -> Int)
y2 = mkx False -- y2 :: (C_3_245_0_0,C_3_245_0_0 -> Int)

mixy = let (v1,f1) = y1
            (v2,f2) = y2
       in f1 v2

"mixy вызывает ошибку типа. Однако мы можем отлично использовать y1 и y2:"

main :: IO ()
main = do putStrLn (show (xapp y1))
          putStrLn (show (xapp y2))

ezyang также хорошо пишет об этом: http://blog.ezyang.com/2010/10/existential-type-curry/