Объединение поликодированной переменной количественной оценки с кортежным типом

Question

У меня есть следующий класс, представляющий категории, в которых класс объекта представлен видом, а каждый класс hom представлен типом, индексированным типами вышеупомянутого типа.

{-# LANGUAGE GADTs, DataKinds, KindSignatures, PolyKinds #-}

type Hom o = o -> o -> *

class GCategory (p :: Hom o)
  where
  gid :: p a a
  gcompose :: p b c -> p a b -> p a c

простой пример экземпляра:

instance GCategory (->)
  where
  gid = id
  gcompose = (.)

Теперь я хочу смоделировать товарные категории. В качестве простой отправной точки вот тип, моделирующий морфизмы категории, соответствующей продукту-> с собой:

data Bifunction ab cd
  where
  Bifunction :: (a -> c) -> (b -> d) -> Bifunction '(a, b) '(c, d)

вот соответствующие операции:

bifunction_id :: Bifunction '(a, a') '(a, a')
bifunction_id = Bifunction id id

bifunction_compose :: Bifunction '(b, b') '(c, c') -> Bifunction '(a, a') '(b, b') -> Bifunction '(a, a') '(c, c')
bifunction_compose (Bifunction f1 g1) (Bifunction f2 g2) = Bifunction (f1 . f2) (g1 . g2)

но когда я пытаюсь вставить операции в экземпляр класса:

instance GCategory Bifunction
  where
  gid = bifunction_id
  gcompose = bifunction_compose

Я столкнулся со следующей проблемой:

• Couldn't match type ‘a’ with ‘'(a0, a'0)’
  ‘a’ is a rigid type variable bound by
    the type signature for:
      gid :: forall (a :: (*, *)). Bifunction a a
    at /tmp/ghc-mod29677/Bifunction29676-49.hs:28:3-5
  Expected type: Bifunction a a
    Actual type: Bifunction '(a0, a'0) '(a0, a'0)
• In the expression: bifunction_id
  In an equation for ‘gid’: gid = bifunction_id
  In the instance declaration for ‘GCategory Bifunction’
• Relevant bindings include
    gid :: Bifunction a a
      (bound at /tmp/ghc-mod29677/Bifunction29676-49.hs:28:3)

Я считаю, что важная часть сообщения заключается в следующем:

  Expected type: Bifunction a a
    Actual type: Bifunction '(a0, a'0) '(a0, a'0)

в частности, что он не может унифицировать тип forall x y. Bifunction '(x, y) '(x, y) с типом forall (a :: (*, *)). Bifunction a a.

Отбросив большую часть специфичных для домена вещей, мы остаемся со следующим минимальным воспроизведением проблемы:

{-# LANGUAGE GADTs, DataKinds, KindSignatures, PolyKinds, RankNTypes #-}

module Repro where

data Bifunction ab cd
  where
  Bifunction :: (a -> c) -> (b -> d) -> Bifunction '(a, b) '(c, d)

bifunction_id :: Bifunction '(a, a') '(a, a')
bifunction_id = Bifunction id id

bifunction_id' :: Bifunction a a
bifunction_id' = bifunction_id

Есть ли способ объединить bifunction_id с участием bifunction_id' над?

---

Альтернативный подход, который я пробовал, - использовать семейства типов, но это все еще не решает проблему полностью:

{-# LANGUAGE GADTs, DataKinds, KindSignatures, PolyKinds, RankNTypes, TypeFamilies #-}

module Repro where

type family Fst (ab :: (x, y)) :: x
  where
  Fst '(x, y) = x

type family Snd (ab :: (x, y)) :: y
  where
  Fst '(x, y) = y

data Bifunction ab cd = Bifunction (Fst ab -> Fst cd) (Snd cd -> Snd cd)

bifunction_id :: Bifunction '(a, a') '(a, a')
bifunction_id = Bifunction id id

-- This still doesn't work
-- bifunction_id' :: Bifunction a a
-- bifunction_id' = bifunction_id

-- But now I can do this successfully
bifunction_id' :: Bifunction a a
bifunction_id' = Bifunction id id

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

Answer 1

forall (x :: k) (y :: l). p '(x, y) менее общий, чем forall (a :: (k, l)). p a, в основном потому, что есть такие вещи (k, l) которые не являются парами.

type family NotAPair :: () -> () -> () -> (k, l)

(Обратите внимание, что семейство типов не имеет параметров, это не то же самое, что NotAPair (u :: ()) (v :: ()) (w :: ()) :: ()). ЕслиNotAPair '() '() '() :: (k, l) были фактически парой '(,) x y, то получилась бы такая ерунда: '(,) ~ NotAPair '(), x ~ '(), y ~ '().

См. Также Вычисления с невозможными типами https://gelisam.blogspot.com/2017/11/computing-with-impossible-types.html

И даже если "все доброе (k, l) являются парами ", существуют разные способы сделать этот факт доступным на языке. Если вы сделаете это неявным, чтобы вы могли, например, неявно преобразовать forall x y. p '(x, y) в forall a. p a, вы можете (или не можете) сделать проверку типов неразрешимой. Если вы сделаете это явным образом, вам придется поработать, чтобы написать это преобразование (например, Coq).

Answer 2

В gid @Bifunctionопределение, у вас есть тип a :: (Type, Type). (,) имеет только один конструктор, поэтому мы можем сделать вывод, что должен существовать x :: Type а также y :: Type такой, что a ~ '(x, y). Однако это рассуждение невозможно выразить в Haskell. В основном, когда у вас есть пара типа-уровень (что-то типа(i, j)) в Haskell, вы не можете предположить, что на самом деле это пара (что-то вроде '(x, y)). Это приводит к поломке вашего кода: у вас естьBifunction id id :: forall x y. Bifunction '(x, y) '(x, y), но вам нужен Bifunction a a, и у вас просто нет правила набора текста, которое позволяет предположить, что a ~ (x, y) для некоторых x, y. Когда вы используете альтернативное, странное определениеBifunction, тогда вы получите Bifunction id id :: forall a. Bifunction a a (потому что это тип возвращаемого конструктора), и он работает в основном потому, что Fst а также Snd являются "частичными" функциями.

Лично я бы просто добавил в качестве аксиомы "все пары на самом деле являются парами".

data IsTup (xy :: (i, j)) =
    forall (x :: i) (y :: j). xy ~ '(x, y) => IsTup
-- could also write
-- data IsTup (xy :: (i, j)) where
--     IsTup :: forall (x :: i) (y :: j). IsTup '(x, y)
isTup :: forall xy. IsTup xy
isTup = unsafeCoerce IsTup

bifunction_id :: Bifunction '(a, x) '(a, x)
bifunction_id = Bifunction id id
bifunction_compose :: Bifunction '(b, y) '(c, z) -> Bifunction '(a, x) '(b, y) -> Bifunction '(a, c) '(x, z)
bifunction_compose (Bifunction fl fr) (Bifunction gl gr) = Bifunction (fl . gl) (fr . gr)

instance GCategory Bifunction where
   gid :: forall a. Bifunction a a -- necessary to bind a
   -- usage of axiom: isTup produces a "proof" that a is actually a pair and
   -- matching against IsTup "releases" the two components and the equality 
   gid | IsTup <- isTup @a = bifunction_id
   gcompose :: forall a b c. Bifunction b c -> Bifunction a b -> Bifunction a c
   gcompose
     | IsTup <- isTup @a, IsTup <- isTup @b, IsTup <- isTup @c
     = bifunction_compose