Ошибка при попытке определить тип Relation [(a, b)] как экземпляр класса Category - PullRequest
Новая
       31

Ошибка при попытке определить тип Relation [(a, b)] как экземпляр класса Category

3 голосов
/ 24 мая 2019

Я изучаю некоторые возможные реализации подмножества R AxB, каждая со своими ограничениями и возможностями. Я также хотел бы, когда это возможно, определить их как экземпляры класса Category или Semigroupoid.

Я выбрал список пар, поскольку, что касается операции составления списков, он только помещает типы элементов пары в ограничение, являющееся экземплярами класса Eq.

Теперь я застрял в этом сообщении об ошибке компилятора: «Нет экземпляра для (Eq a), возникающего из-за использования‘ ° ’»

Что не так? 

{-# LANGUAGE GADTs #-}

module RelationT where

import Data.List
import Control.Category as Cat

data RelationT a b where
  Id :: RelationT a a
  RT :: (Eq a, Eq b) => [(a,b)] -> RelationT a b

instance Category RelationT where
  id = Id
  Id . r = r
  r . Id = r
  r1 . r2 = r1 ° r2 -- error:  No instance for (Eq a) arising from a use of ‘°’

(°) :: (Eq a, Eq b, Eq t) => RelationT t b -> RelationT a t -> RelationT a b
RT r1 ° RT r2 = RT $ nub $ go r1 r2
    where
    go [] r =  []
    go r [] =  []
    go xys2 ( ((x1,y1): xys1)) =  go2 x1 y1 xys2 [] ++ go xys2  xys1
        where
        go2 x y [] acc = acc
        go2 x y ((w,z):wzs) acc
          | y == w = go2 x y wzs ((x,z):acc)
          | otherwise = go2 x y wzs acc

-- ex. RT [(1,'a'),(4,'b'),(5,'c'),(10,'d')] ° RT [(3,10),(1,5),(1,1)]
-- > RT [(3,'d'),(1,'c'),(1,'a')]

1 Ответ

2 голосов
/ 24 мая 2019

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

(°) :: RelationT t b -> RelationT a t -> RelationT a b

Информация (Eq a, Eq b, Eq c) будет все еще доступна в теле функции, поскольку вы сопоставили с шаблоном RT r1 и RT r2там, который, если успешно, свидетельствует о том, что все типы имеют экземпляр Eq.

Это говорит: по моему опыту, этот трюк хранения ограничения в GADT быстро приводит к неприятностям, когда вы хотите сделать больше вовлеченнымвещи с вашей категорией.Проблема в том, что стандартный класс Category на самом деле не подходит для такого типа отношения, потому что он поддерживает только те категории, которые имеют точно такие же объекты, как Hask - т.е. всеХаскель типы.Но ваша категория отношений действительно имеет только сопоставимые по равенству типы в качестве объектов;с помощью дополнительного конструктора Id вы принудительно расширяете его, чтобы также включить отношения между неэквивалентными типами, но есть только отношение идентичности доступно ... это довольно хрупкий взлом.

Правильным выходом является использование класса типов, который позволяет категориям иметь более ограниченное представление об объектах для начала.Самый простой способ сделать это - виды ограничений .Из моего constrained-categories пакета : 

{-# LANGUAGE TypeFamilies, ConstraintKinds #-}
import GHC.Exts (Constraint)

class Category k where
  type Object k o :: Constraint
  id :: Object k a => k a a
  (.) :: (Object k a, Object k b, Object k c)
         => k b c -> k a b -> k a c

Тогда вы можете сделать экземпляр 

data RelationT a b where
  Id :: RelationT a a
  RT :: [(a,b)] -> RelationT a b

instance Category RelationT where
  type Object RelationT o = Eq o
  id = Id
  (.) = (°)
...