Разрешение вызова функции в экзистенциальном типе

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

{-# LANGUAGE ExistentialQuantification #-}

data Showable = forall a. Show a => MkShowable a

pack :: Show a => a -> Showable
pack = MkShowable

instance Show Showable where
    show (MkShowable x) = show x

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

showSomething :: Bool -> Showable
showSomething True = pack 1
showSomething False = pack "ABC"

main :: IO ()
main = do
  x <- getLine
  let y = read x
  print $ showSomething y

Этот код (который работает нормально) запрашивает у пользователя ввод (который должен быть «Истина» или «Ложь»), а затем выводит 1, если это правда, или "ABC", если это ложь.

Но я не могу полностью понять, как система это делает. Математически это имеет смысл. Но я не понимаю, как компьютер может это решить. Мне кажется, что система во время выполнения принимает решение о том, следует ли вызывать экземпляр show Int или функцию show String, но это подразумевает существование чего-то вроде виртуальных таблиц C++, о которых я не думаю, что в Haskell есть концепция.

Мой вопрос: как это решить? Система не может знать заранее, собираюсь ли я ввести true или false, поэтому она не может знать, какой show вызывать во время компиляции, но она явно работает в обоих случаях.


types haskell existential-type
person Silvio Mayolo    schedule 13.12.2014    source источник
comment
Да, классы типов преобразуются в дополнительный аргумент, похожий на словарь, который содержит реализации методов для конкретного экземпляра. Этот аргумент передается каждой функции с сигнатурой Showable =>.   -  person arrowd    schedule 13.12.2014
comment
Вот потрясающее видео, SPJ говорит об этом: youtube.com/watch?v=6COvD8oynmI   -  person arrowd    schedule 13.12.2014
comment
В GHC есть что-то точное, похожее на C++ vtables. (Хотя обычно мы называем их словарями методов.)   -  person MathematicalOrchid    schedule 13.12.2014

Ответы (2)


arrow_upward
6
arrow_downward

Одним из способов реализации классов типов является передача словаря функций, реализующих класс типов под капотом. Например, функция с подписью

f :: Show a => T

будет переведено на

f' :: (a -> String) -> T

компилятором, и всякий раз, когда show используется внутри f, он заменяется дополнительным аргументом (на самом деле функций было бы больше, все, что объявлено в Show).

Точно так же тип данных

forall a . Show a => MkShowable a

будет переведено на

forall a . MkShowable' (a -> String) a

Таким образом, преобразованный код может выглядеть так:

{-# LANGUAGE ExistentialQuantification #-}

data Showable' = forall a . MkShowable' (a -> String) a

pack' :: Show a => a -> Showable'
pack' = MkShowable' show

instance Show Showable' where
    show (MkShowable' f x) = f x

showSomething :: Bool -> Showable'
showSomething True = pack' 1
showSomething False = pack' "ABC"

Когда вызывается pack, реализация show также передается конструктору, чтобы она была доступна при необходимости.

person Petr    schedule 13.12.2014

arrow_upward
2
arrow_downward

Ага. Совокупность языковых функций (большинство из них — расширения) в Haskell можно рассматривать как реализацию многих концепций, объединенных в сложный монолит «класса» объектно-ориентированного программирования, но отдельно как отдельные черты. Экзистенциальные типы с ограничениями классов типов в основном являются виртуальными таблицами!

Чтобы show (MkShowable x) работало без каких-либо других ограничений, MkShowable x должно содержать достаточно информации, чтобы знать, как show x. Это именно то, что он делает; хотя у него только одно поле, на самом деле он содержит дополнительную информацию.

По сути, это то же самое, что и функция foo :: Show a => a; foo x = show x, которая имеет только один параметр, но на самом деле должна получить достаточно дополнительной информации, чтобы знать, как show x; он не может быть «жестко подключен», потому что foo, вероятно, используется в нескольких разных типах. Но там, где foo требует, чтобы вызывающая сторона передала эту информацию извне (и система типов обеспечивает это), значение Showable содержит точно такую ​​же информацию, чтобы можно было извлечь ее для передачи в такие функции, как foo.

Итак, теперь с этой возможностью, в отличие от ExistentialQuantification, проблема определения того, какой экземпляр show вызывать, заключается в простом выборе между двумя значениями одного и того же типа (которые содержат экземпляр Show для некоторого неизвестного типа вместе со значением того же типа), что легко сделать; знание времени компиляции о том, какой из них требуется, не требуется.

person Ben    schedule 13.12.2014
comment
К сожалению, во время компиляции сведения о том, какой из них используется, используются, даже если они доступны. Я отправил отчет об этом, но, к сожалению, похоже, что для исправления потребуется довольно значительная реструктуризация. - person dfeuer; 13.12.2014