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

Question

Я изо всех сил пытаюсь понять ключевое слово 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

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

Answer 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 определенный тип p, поэтому он должен возвращать тот же тип.Поэтому мы не можем использовать forall.

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

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

Answer 2

Когда я говорю, а -> Инт, это значит (в моем понимании, неправильный, наверное) (тип) а, есть функция введите 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 - так что вы можете сделать с ним что-то полезное, даже не зная его «истинного» типа.

Answer 3

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

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/

Answer 4

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

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

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

data Useless = exists s. Useless s

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