Типовая рекурсия и PolyKinds

Question

Я пытаюсь реализовать полиморфную функцию, которая по существу пересекает тип, накапливая Tag значение. Я хотел бы, чтобы пользователи могли делать, например, rec ((1,2), ('a', 3)),

{-# LANGUAGE KindSignatures, PolyKinds, FlexibleInstances #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE UndecidableInstances #-}
import Data.Proxy

newtype Tag (a :: k) = Tag Int
    deriving (Eq, Read, Show)

-- My users only have to define their own instances of this class...
class Tagged (a :: k) where
  tag :: Tag a

-- ...like these:
instance Tagged Int where
  tag = Tag 1

instance Tagged Char where
  tag = Tag 2

instance Tagged (,) where
  tag = Tag 3


-- While this is a morally "closed" class; implementing recursion over
-- components of types. This is what I'm struggling with:
class Rec (a :: k) where
  rec :: proxy a -> Tag a

instance (Rec ab, Rec c)=> Rec (ab c) where
  rec _ = let Tag ab = rec Proxy :: Tag ab
              Tag c = rec Proxy :: Tag c
           in Tag (ab * c)

instance {-# OVERLAPPABLE #-} Tagged a=> Rec a where
  rec _ = tag :: Tag a

Я возился с этим по-разному, и в текущем воплощении получить ошибку (для обоих ab а также c, в первую очередь):

    • Could not deduce (Tagged ab) arising from a use of ‘rec’
      from the context: (Rec ab, Rec c)
        bound by the instance declaration at flook.hs:26:10-37
    • In the expression: rec Proxy :: Tag ab
      In a pattern binding: Tag ab = rec Proxy :: Tag ab
      In the expression:
        let
          Tag ab = rec Proxy :: Tag ab
          Tag c = rec Proxy :: Tag c
        in Tag (ab * c)
   |
27 |   rec _ = let Tag ab = rec Proxy :: Tag ab
   |                        ^^^^^^^^^

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

Есть ли способ заставить это работать или лучший подход?

Answer 1

Я думаю, вы должны пропустить два занятия. Достаточно одного.

Недостатком является то, что ваши пользователи не смогут писать экземпляры, соответствующие instance Tagged (Maybe Int) в вашем дизайне, которые делают что-то особенное для составных типов... но они уже не могли их использовать, так как экземпляр приложения для Rec всегда будет перекрывать его в любом случае.

Итак, без лишних слов:

{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE UndecidableInstances #-}

import Data.Tagged

class Rec a where rec :: Tagged a Int

-- it is still possible for users to define their own instances for base types
instance Rec Int  where rec = 1
instance Rec Char where rec = 2
instance Rec (,)  where rec = 3

instance (Rec ab, Rec c) => Rec (ab c) where
  rec = retag (rec :: Tagged ab Int) * retag (rec :: Tagged c Int)

В ghci:

> rec :: Tagged ((Int, Int), Char) Int
Tagged 18