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