Докажите, что ограничение для компонента продукта выполняется из того факта, что оно выполняется для продукта

У меня есть класс C с экземплярами для одного типа и для кортежей.

class C a

instance C Int

instance (C a, C b) => C (a, b)

Используя нормальный Dict ГАДТ для захвата ограничений

{-# LANGUAGE GADTs #-}
{-# LANGUAGE ConstraintKinds #-}

data Dict c where
    Dict :: c => Dict c

можно ли доказать C a от C (a, b)?

fstDict :: Dict (C (a, b)) -> Dict (C a)
fstDict Dict = ???

Я подозреваю, что немедленный ответ "нет", так как fstDict Dict = Dict недостаточно, и есть несколько других возможностей. Есть ли способ изменить C так что ограничения для компонентов продуктов могут быть восстановлены из ограничения на продукт?

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

data DSL a b where
    DSL :: (Dict C a -> DSL' a b) -> DSL a b

data DSL' a b where
    DSL' :: (C a, C b) => ... -> DSL' a b
Источник

2 ответа

Решение

Открытый вариант ответа Даниэля Вагнера будет использовать TypeFamily позволить каждому типу, который реализует класс, указать контекст, в котором он нуждается.

{-# LANGUAGE GADTs #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ScopedTypeVariables #-}

import GHC.Exts (Constraint)
import Data.Proxy

data Dict c where
    Dict :: c => Dict c

Класс позволяет каждому типу указывать дополнительное ограничение Ctx a что нужно типу. cdict Функция заставляет контекст следовать из C и обеспечивает способ получить в основе Ctxбез включения их в Ctx например, для продуктов.

class C a where
    type Ctx a :: Constraint
    cdict :: Proxy a -> CDict a

CDict тогда Dict который содержит как ограничение C a а также любой дополнительный контекст Ctx a тип a потребности

type CDict a = Dict (C a, Ctx a)

Int экземпляр не нуждается в дополнительном контексте

instance C Int where
    type Ctx Int = ()
    cdict _ = Dict

Экземпляр кортежа нуждается в обоих C a а также C b

instance (C a, C b) => C (a, b) where
    type Ctx (a, b) = (C a, C b)
    cdict _ = Dict

Мы можем написать fstCDict для кортежей.

fstCDict :: forall a b. CDict (a, b) -> CDict a
fstCDict Dict = case cdict (Proxy :: Proxy a) of Dict -> Dict

Неверный экземпляр

Если мы попытаемся написать неправильный экземпляр C что магически вызывает Show экземпляры

instance (C a) => C (Maybe a) where
    type Ctx (Maybe a) = (C a, Show a)
    cdict _ = Dict

Это приводит к ошибке компилятора

    Could not deduce (Show a) arising from a use of `Dict'
    from the context (C a)
      bound by the instance declaration ...
    Possible fix:
      add (Show a) to the context of the instance declaration
    In the expression: Dict
    In an equation for `cdict': cdict _ = Dict
    In the instance declaration for `C (Maybe a)'
Источник

Один из способов - сохранить все словари предков в вашем Dict тип:

data CDict a where
    IntDict :: C Int => CDict Int
    PairDict :: C (a, b) => CDict a -> CDict b -> CDict (a, b)

fstCDict :: CDict (a, b) -> CDict a
fstCDict (PairDict fst snd) = fst

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

Источник
Другие вопросы по тегам