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

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

class C a

instance C Int

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

Использование обычного Dict GADT для фиксации ограничений

{-# 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

typeclass haskell gadt constraint-kinds
person Cirdec    schedule 09.01.2015    source источник

Ответы (2)


arrow_upward
1
arrow_downward

Один из способов — сохранить все словари-предки в вашем типе 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 отражать структуру ваших экземпляров.

person Daniel Wagner    schedule 09.01.2015

arrow_upward
1
arrow_downward

Открытый вариант ответа Даниэля Вагнера будет использовать 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)'
person Cirdec    schedule 09.01.2015