Как QuanifiedConstraints переводятся в стиль передачи словаря - PullRequest
Новая
       8

Как QuanifiedConstraints переводятся в стиль передачи словаря

0 голосов
/ 01 октября 2018

QuantifiedConstraints 1 находится в GHC 8.6, я читаю Классы типов деривации (раздел 7) 2 , где этобыл впервые предложен.Однако я не могу понять, с практической точки зрения, как QuantifiedConstraints переводятся в словари.Ниже приводится выдержка из статьи.

Нам нужен способ упростить предикат f (GRose f a).Хитрость заключается в том, чтобы взять «константное» объявление экземпляра, которое мы приняли для Binary (List a) выше, и абстрагироваться над ним: 

instance (Binary a,
          forall b. (Binary b) => Binary (f b)
         ) => Binary (GRose f a) where
  showBin (GBranch x ts ) = showBin x ++ showBin ts

Теперь, а также (Binary a),контекст также содержит полиморфный предикат.Этот предикат можно использовать для сокращения предиката Binary (f (GRose f a)) до Binary (GRose f a), и у нас есть для этого объявление экземпляра.

В операционном плане предикат (Binary a) в контексте соответствует передачесловарь для класса Binary.Предикат forall b. Binary b => Binary (f b) соответствует передаче словарного преобразователя в функцию.

В частности, я не могу сказать следующее:

1) Уменьшить предикат Binary (f (GRose f a)) доBinary (GRose f a)

2) Предикат соответствует передаче словарного преобразователя в функцию.

1 Ответ

0 голосов
/ 01 октября 2018

Для регулярных ограничений карта перевода 

class Colored a where
   isRed :: a -> Bool

foo :: Colored a => T

в 

newtype ColoredDict a = CD (a -> Bool)

foo :: ColoredDict a -> T

Аналогично, 

bar :: (forall a. Colored a => Colored [a]) => U

можно перевести как 

bar :: (forall a. ColoredDict a -> ColoredDict [a]) -> U

2) Предикат соответствует передаче словарного преобразователя в функцию.

Первый аргумент bar - это "словарный преобразователь", который упоминает OP.

bar включает в себя тип ранга 2, но Haskell использует их в течение длительного времени.

1) Уменьшите предикат Binary (f (GRose f a)) до Binary (GRose f a)

Дело в том, что каждый раз, когда bar необходимо разрешить ограничение Colored [t], он может использовать квантифицированное ограничение и вместо этого попытаться разрешить более простое ограничение Colored a.

...