Количественные ограничения по сравнению с (закрытыми) типами семейств - PullRequest
2 голосов
/ 06 июня 2019

Я пытаюсь использовать подход этого поста к данным с более высокой степенью родства без висячих Identity функторов для случайного случая вместе с получением количественного ограничения:

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE QuantifiedConstraints, StandaloneDeriving, UndecidableInstances #-}
module HKD2 where

import Control.Monad.Identity

type family HKD f a where
    HKD Identity a = a
    HKD f        a = f a

data Result f = MkResult
    { foo :: HKD f Int
    , bar :: HKD f Bool
    }

deriving instance (forall a. Show a => Show (HKD f a)) => Show (Result f)

Этот результатв яростно противоречивом сообщении об ошибке:

Не удалось вывести Show (HKD f a) из контекста: forall a. Show a => Show (HKD f a)

Есть ли способ сделать это, не затягиваяоб этом и делают

deriving instance (Show (HKD f Int), Show (HKD f Bool)) => Show (Result f)

?

1 Ответ

3 голосов
/ 06 июня 2019

Я не думаю, что вы можете сделать это, но я, безусловно, могу ошибаться.В вашем примере вы пропускаете дополнительное ограничение Show (f a) для его завершения:

deriving instance (forall a. (Show a, Show (f a)) => 
   Show (HKD f a)) => Show (Result f)

Но это будет означать, что экземпляр Show для f a не может зависеть от a, чтоможет быть истинным для конкретных f, но не для всех.

Edit

Но в то же время можно написать что-то подобное без TypeFamilies:

data Bar f = MkBar (f Int)

deriving instance (forall a . Show a => Show (f a)) => Show (Bar f)

Итак, я не уверен, почему GHC не может понять это.

Edit 2

Вот интересныйнаблюдение, это компилирует:

type family HKD f a where
    -- HKD Identity a = a
    HKD f Int = Int
    HKD f a = f a

data Result f = MkResult
    { foo :: HKD f Int
    , bar :: HKD f Bool
    }

deriving instance (forall a. Show a => Show (f a)) => Show (Result f)

и работает как ожидалось:

λ> show $ MkResult 5 (Just True)
"MkResult {foo = 5, bar = Just True}"

Итак, похоже, что совпадение на f каким-то образом портит проверку типов.

Стоит отметить, что ограничение Show (HDK f a) даже для упрощенного примера также дает ту же ошибку времени компиляции, что и в вопросе:

deriving instance (forall a. Show a => Show (HKD f a)) => Show (Result f)
...