Что означает "существует" в системе типа 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/