Вывод обычного экземпляра typeclass из серии меньших?

Question

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

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

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

class Known f a where 
    known :: f a 

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

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

instance Known Proxy a where 
    known = Proxy 

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

> known :: Proxy Monad 
Proxy 

Но есть также экземпляр для this HList-like type:

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) кортеж. Тот же Functor, разные типы.

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

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

Который работает довольно хорошо: (предполагая Показать экземпляр)

> 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, как его построить так, как это выполняется?

Answer 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 

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

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