Вывод общего экземпляра класса типов из серии более мелких?

название этого, по общему признанию, не очень описательное, но я не знаю, как еще описать это в коротком названии. Буду признателен за любые рекомендации!

Я собираюсь представить очень упрощенную версию моей проблемы :)

Итак, у меня есть класс типов

class Known f a where
    known :: f a

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

Так что, очевидно, есть экземпляр для Proxy:

instance Known Proxy a where
    known = Proxy

Что мы можем использовать:

> known :: Proxy Monad
Proxy

Но есть также экземпляр для типа, подобного HList:

data Prod f :: [k] -> * where
    PNil :: Prod f '[]
    (:<) :: f a -> Prod f as -> Prod f (a ': as)

infixr 5 (:<)

Где Prod f '[a,b,c] будет примерно эквивалентно кортежу (f a, f b, f c). Тот же функтор, разные типы.

Написать экземпляр достаточно просто:

instance Known (Prod f) '[] where
    known = PNil
instance (Known f a, Known (Prod f) as) => Known (Prod f) (a ': as) where
    known = known :< known

Что работает довольно хорошо: (при условии, что экземпляр Show)

> known :: Prod Proxy '[1,2,3]
Proxy :< Proxy :< Proxy :< PNil

Но я в том случае, когда мне нужно сделать "полиморфную" функцию для всех as... но GHC это не нравится.

asProds :: forall as. Proxy as -> Prod Proxy as
asProds _ = known :: Prod Proxy as

Выходит с этой ошибкой:

No instance for (Known (Prod f) as)
  arising from a use of 'known'

Что, я думаю, говорит о том, что GHC не может показать, что будет экземпляр, который он выберет, который будет работать для любого as, или у него нет стратегии создания known для этого экземпляра.

Я, как человек, знаю, что это так, но есть ли способ заставить это работать? Все экземпляры находятся "в рамках" и доступны... но как я могу сказать GHC, как сконструировать его таким образом, чтобы он был удовлетворен?


person Justin L.    schedule 04.12.2015    source источник


Ответы (1)


Если для класса нет ограничений, вы не можете использовать его методы. Просто добавьте ограничение:

asProds :: forall as. Known (Prod Proxy) as => Proxy as -> Prod Proxy as
asProds _ = known :: Prod Proxy as  

Обратите внимание, что GHC может вывести этот тип:

asProds (_ :: Proxy as) = known :: Prod Proxy as
-- inferred constraint

Поскольку типы стираются, нет ничего, из чего можно было бы создавать экземпляры во время выполнения при отсутствии словаря для начала. Вполне может быть логически верным, что существуют экземпляры для всех обитателей вида, но для запуска программ нам нужны словари - конструктивные доказательства.

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

person András Kovács    schedule 04.12.2015
comment
Ах. К сожалению, избегание такого ограничения является причиной, по которой я прохожу через это в первую очередь. Но! Моя проблема изначально заключалась в том, что мне нужно было указать (Applicative (Foo ns), Foldable (Foo ns)) и т. д. для всех моих экзистенциалов, и я думал, что просто имея это, я смогу избавиться от всего этого. Но теперь я вижу, что могу просто заменить все эти различные ограничения ограничением Known. Не избежать ограничений, но теперь просто иметь одну универсальную возможность намного чище, спасибо! - person Justin L.; 04.12.2015
comment
@ДжастинЛ. Вы также можете использовать синонимы ограничения: type Known ns = (Applicative (Foo ns), Foldable (Foo ns), ...). - person Alexey Romanov; 04.12.2015
comment
@AlexeyRomanov мне все еще кажется, что это очень нестандартно и не по-хаскельски. Я мог бы добавить кучу экземпляров, которые имеют только очень редкое/необычное и неясное использование, которые не имеют никакого отношения к фактическому конструктору данных для типа... это не имеет ничего общего с неясными классами в все. И мне пришлось бы добавлять класс и дублировать работу каждый раз, когда я пишу новый экземпляр. - person Justin L.; 05.12.2015