Соответствие типам с высоким родом в SYB - PullRequest
Новая
       22

Соответствие типам с высоким родом в SYB

1 голос
/ 04 февраля 2020

В общем, мне интересно, есть ли способ написать обобщенный c сгиб, который обобщает функцию, которая применяет тип forall, такой как: 

f :: forall a. Data (D a) => D a -> b

при некотором типе данных D для которого instance Data (D a) (возможно, с ограничениями на a). Чтобы быть конкретным, рассмотрим что-то даже такое простое, как False `mkQ` isJust, или, как правило, запрос к конструктору типа данных с более высоким родом. Аналогично, рассмотрим преобразование mkT (const Nothing), которое затрагивает только один конкретный тип с более высоким родом.

Без явных сигнатур типов они завершаются ошибкой с No instance for Typeable a0, что, вероятно, является ограничением мономорфизма в действии. Справедливо. Однако, если мы добавим явные подписи типов: 

t :: GenericT
t = mkT (const Nothing :: forall a. Data a => Maybe a -> Maybe a)
q :: GenericQ Bool
q = False `mkQ` (isJust :: forall a. Data a => Maybe a -> Bool)

, вместо этого нам скажут, что тип внешних подписей forall неоднозначен: 

Could not deduce (Typeable a0)
   arising from a use of ‘mkT’
from the context: Data a
   bound by the type signature for:
              t :: GenericT
The type variable ‘a0’ is ambiguous

Я не могу обернуть свою голова вокруг этого. Если я правильно понимаю, что a0 - это переменная в t :: forall a0. Data a0 => a0 -> a0, как она может быть более двусмысленной, чем, скажем, mkT not? Во всяком случае, я бы ожидал, что mkT будет жаловаться, потому что именно он взаимодействует с isJust. Кроме того, эти функции являются более полиморфными c, чем ветвление на конкретных типах.

Мне любопытно узнать, является ли это ограничением доказательства внутреннего ограничения isJust :: Data a => ... - я понимаю, что любой тип Экземпляр Data, населенный Maybe a, также должен иметь Data a, чтобы быть действительным по ограничению экземпляра instance Data a => Data (Maybe a).

1 Ответ

1 голос
/ 04 февраля 2020

tldr: вам нужно создать другую функцию.

mkT имеет следующую подпись: 

mkT :: (Typeable a, Typeable b) => (a -> a) -> (b -> b)

И вы хотите применить ее к функции polymorphi c введите (forall x. Maybe x -> Maybe x). Это невозможно: невозможно создать экземпляр a в (a -> a) для получения (forall x. Maybe x -> Maybe x).

Это не просто ограничение системы типов, реализация mkT не будет поддерживать такой экземпляр также.

mkT просто сравнивает конкретные типы a и b на равенство во время выполнения. Но то, что вы хотите, это иметь возможность проверить, равен ли b Maybe x для некоторых x. Логика c, которая для этого требуется, существенно сложнее. Но это, безусловно, все еще возможно.

Ниже mkT1 сначала сопоставляет тип b с шаблоном App, чтобы узнать, является ли b приложением некоторого типа g y и затем проверяет равенство g и f: 

-- N.B.: You can add constraints on (f x), but you must do the same for b.
mkT1 :: (Typeable f, Typeable b) => (forall x. f x -> f x) -> (b -> b)
mkT1 h =
  case typeRep @b of
    App g y ->
      case eqTypeRep g (typeRep @f) of
        Just HRefl -> h
        _ -> id
    _ -> id

Скомпилируемый пример также с mkQ1: 

{-# LANGUAGE ScopedTypeVariables, RankNTypes, TypeApplications, GADTs #-}

import Type.Reflection

mkT1 :: forall f b. (Typeable f, Typeable b) => (forall x. f x -> f x) -> (b -> b)
mkT1 h =
  case typeRep @b of
    App g y ->
      case eqTypeRep g (typeRep @f) of
        Just HRefl -> h
        _ -> id
    _ -> id

mkQ1 :: forall f b q. (Typeable f, Typeable b) => (forall x. f x -> q) -> (b -> q) -> (b -> q)
mkQ1 h =
  case typeRep @b of
    App g y ->
      case eqTypeRep g (typeRep @f) of
        Just HRefl -> const h
        _ -> id
    _ -> id

f :: Maybe x -> String
f _ = "matches"

main :: IO ()
main = do
  print (mkQ1 f (\_ -> "doesn't match") (Just 3 :: Maybe Int))  -- matches
  print (mkQ1 f (\_ -> "doesn't match") (3 :: Int))             -- doesn't match
...