Черная магия в отражении Хаскелла

Ответ 1

Прежде чем понимать эту реализацию, вы должны понимать API. Исходная идея (отражающая произвольный указатель на уровень типа) объясняется в этой статье, которая реализована в slow "версии reflection. Поэтому я предполагаю, что вы уже знаете, как это работает, и как используется API." fast "- это еще одна реализация того же API, которая использует несколько специфический для GHC трюк, чтобы ускорить процесс. Итак:

• unsafeCoerce :: a -> b действительно применяется к трем аргументам, что означает, что b должен быть типом функции с двумя аргументами. В частности, тип этого unsafeCoerce выглядит примерно так: Magic a r -> (Proxy s -> a) -> Proxy s -> r.

• Хех. "Изоморфными".

  Более серьезно: важно понять реализацию GHC классов типов, которая включает в себя передачу словаря. Когда у вас есть что-то вроде

  class Num a where
    plus :: a -> a -> a
    negate :: a -> a
  foo :: Num a => a -> a
  foo x = plus x (negate x)
  

  Он переводится во что-то вроде

  data Num a = Num { plus :: a -> a -> a, negate :: a -> a }
  foo :: Num a -> a -> a
  foo dict x = plus dict x (negate dict x)
  

  С помощью GHC выясняется, какой словарь должен проходить в зависимости от типа при использовании foo. Обратите внимание, как функция с одним аргументом превратилась в функцию с двумя аргументами.

  Таким образом, реализация класса типа заключается в передаче дополнительного словарного аргумента. Но учтите, что в качестве оптимизации мы можем использовать newtype вместо data, когда класс имеет только один метод. Например.

  class Default a where
    def :: a
  doubleDef :: Default a => (a, a)
  doubleDef = (def, def)
  

  превращается в

  newtype Default a = Default { def :: a }
  doubleDef :: Default a -> (a, a)
  doubleDef dict = (def dict, def dict)
  

  Но это сгенерированное def оперативно unsafeCoerce.

• Magic k k, только с другим типом. Таким образом, функция unsafeCoerce (Magic k) является функцией k, с измененным типом. Это все-таки функция.

• Итак, подумайте о том, как этот класс скомпилирован (я собираюсь переключиться на Proxy с капиталом P, чтобы упростить).

  class Reifies s a | s -> a where
    reflect :: Proxy s -> a
  foo :: Reifies s a => ...
  

  превращается в

  newtype Reifies s a = Reifies { reflect :: Proxy s -> a }
  foo :: Reifies s a -> ...
  -- which is unsafeCoerce-compatible with
  foo :: (Proxy s -> a) -> ...
  

  Итак, оперативно,

  newtype Magic a r = Magic (forall s. Reifies s a => Proxy s -> r)
  

  является unsafeCoerce -совместимым с

  newtype Magic a r = Magic (forall s. (Proxy s -> a) -> Proxy s -> r)
  

• Итак, теперь мы видим, как это работает:

  reify получает два аргумента, значение :: a и функцию :: forall s. Reifies s a => Proxy s -> r. Так как функция удобно имеет ту же форму, что и Magic, мы превращаем ее в значение :: Magic a r. Оперативно Magic a r примерно такая же, как forall s. (Proxy s -> a) -> Proxy s -> r, поэтому мы можем пересечь наши пальцы и unsafeCoerce. Конечно, (Proxy s -> a) -> Proxy s -> r изоморфен a -> r, поэтому нам просто нужно передать правильную функцию (const a) и Proxy значение, и мы закончили.

• Магия всегда была в вашей функции.

Ответ 2

shachaf ответ не только лучше, чем мой, но и правильный, однако я сохраняю свои мысли здесь для потомков.

Это намного выше меня, но вот мой ответ так или иначе.

• Magic - это конструктор из 2 параметров, а unsafeCoerce - принудительное Magic k, которое имеет тип r -> Magic a r для типа const a. То, что он здесь делает, - это принуждение функции быть от одного типа к другому. Итак, третий "аргумент" на unsafeCoerce, я подозреваю, фактически является аргументом, переданным в результат unsafeCoerce (Magic k :: Magic a r) (const a)
• Похоже, что большая часть черной магии заключается в том, что экземпляры Reifies не определены, а конструктор использует экзистенциальный тип. Как бы то ни было, фактический тип экзистенциального типа встречается через unsafeCoerce.
• Он определяется в результате слияния конструктора с типом const a. Этот бит я понимаю наименее.
• Экземпляры не существуют, насколько я могу судить - экзистенциальный тип, по-видимому, занят в силу unsafeCoerce, убеждая систему типов, что независимо от того, существуют ли какие-либо экземпляры, значение типа Magic a r был создан. Независимо от того, существует ли этот тип или нет, он, похоже, "подделан", как в подделке, а не как в металлообработке.
• Первый параметр Magic - это тип reified как Proxy, я думаю.
• Магия в newtype Magic находится в этом бите: (forall (s :: *). Reifies s a => Proxy s -> r) То, что тип вещи Magic обертывается. Он указывает, что аргумент Proxy, s является экзистенциальным типом Reifies, или, так сказать, единственным фактом, о котором знает система типов, является то, что он является экземпляром Reifies. Поэтому он знает, что независимо от s, это должен быть экземпляр Reifies, и он может использовать этот экземпляр, но все, что он может сделать. Это похоже на то, что система типов очистила все другие знания о том, что такое тип, и знает только, что для значения, которое имеет значение Proxy, он может использовать на нем функцию reflect - и это. Но reflect восстанавливает значение и тип, потому что тип был закодирован в Magic, а reflect - просто unsafeCoerce функции const a. Или, по крайней мере, это то, что я собираю.

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