Обобщение расширения типа по семейству данных - PullRequest
Новая
       38

Обобщение расширения типа по семейству данных

3 голосов
/ 21 сентября 2019

Я пишу библиотеку, в которой я расширяю несколько типов * -> * -> * на семейства типов k -> k -> k (для определенных k), используя семейство данных: 

{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE TypeOperators #-}
-- ...

type family (+) = (c :: k -> k -> k) | c -> k where
  (+) = Either
  (+) = Sum_
infixl 6 +

data family Sum_ (a :: j -> k) (b :: j -> k) :: j -> k
newtype instance Sum_ a b x = Sum1 { getSum1 :: a x + b x }
newtype instance Sum_ a b x y = Sum2 { getSum2 :: a x y + b x y }
newtype instance Sum_ a b x y z = Sum3 { getSum3 :: a x y z + b x y z }

type family (×) = (p :: k -> k -> k) | p -> k where
  (×) = (,)
  (×) = Product_
infixl 7 ×

data family Product_ (a :: j -> k) (b :: j -> k) :: j -> k
newtype instance Product_ a b x = Product1 { getProduct1 :: a x × b x }
newtype instance Product_ a b x y = Product2 { getProduct2 :: a x y × b x y }
newtype instance Product_ a b x y z = Product3 { getProduct3 :: a x y z × b x y z }

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

type family Extension (base :: * -> * -> *) = (p :: k -> k -> k) | p -> k where
  Extension base = base
  Extension base = Extension_ base

data family Extension_ (base :: * -> * -> *) (a :: j -> k) (b :: j -> k) :: j -> k
newtype instance Extension_ base a b x = Extension1 { getExtension1 :: Extension base (a x) (b x) }
newtype instance Extension_ base a b x y = Extension2 { getExtension2 :: Extension base (a x y) (b x y) }
newtype instance Extension_ base a b x y z = Extension3 { getExtension3 :: Extension base (a x y z) (b x y z) }

type (+) = Extension Either
infixl 6 +

type (×) = Extension (,)
infixl 7 +

type (^) = Extension (Dual (->))
infixr 8 ^

К сожалению,кажется, что это нарушает инъективность, поскольку GHC понимает это (хотя, насколько я могу судить, есть только один возможный k для каждого Extension base): 

src/Extension.hs:36:3: error:
    • Type family equation violates injectivity annotation.
      RHS of injective type family equation is a bare type variable
      but these LHS type and kind patterns are not bare variables: ‘*’
        Extension base = base
          -- Defined at src/Extension.hs:36:3
    • In the equations for closed type family ‘Extension’
      In the type family declaration for ‘Extension’
   |
36 |   Extension base = base
   |   ^^^^^^^^^^^^^^^^^^^^^

src/Extension.hs:36:3: error:
    • Type family equations violate injectivity annotation:
        Extension base = base
          -- Defined at src/Extension.hs:36:3
        Extension base = Extension_ base
          -- Defined at src/Extension.hs:37:3
    • In the equations for closed type family ‘Extension’
      In the type family declaration for ‘Extension’
   |
36 |   Extension base = base
   |   ^^^^^^^^^^^^^^^^^^^^^

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

Есть ли другой способ, которым я могу захватить иповторно использовать шаблон Extension?

...