Объединяющая поликлиническая переменная количественного определения с типом кортежей - PullRequest
5 голосов
/ 22 сентября 2019

У меня есть следующий класс, представляющий категории, где класс объекта представлен видом, а каждый класс 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

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

Ответы [ 2 ]

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

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).

1 голос
/ 22 сентября 2019

В определении gid @Bifunction у вас есть тип a :: (Type, Type).(,) имеет только один конструктор, поэтому мы можем сделать вывод, что должны существовать x :: Type и y :: Type такие, что a ~ '(x, y).Однако это рассуждение не может быть выражено в Хаскеле.По сути, если у вас есть пара уровня типа (что-то типа (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
...