Связанные типы и элементы контейнера

Question

Я думаю, что я мог бы спросить об этом в Haskell-Cafe в какой-то момент, но проклят, если я смогу найти ответ сейчас ... Поэтому я прошу его снова здесь, поэтому, надеюсь, в будущем я смогу найти ответ!

Haskell является фантастическим при работе с параметрическим полиморфизмом. Но проблема в том, что не все параметрическое. В качестве тривиального примера предположим, что мы хотим извлечь первый элемент данных из контейнера. Для параметрического типа, что тривиальное:

 
class HasFirst c where 
    first :: c x -> Maybe x 

instance HasFirst [] where 
    first [] = Nothing 
    first (x:_) = Just x 

Теперь попробуйте и написать экземпляр для ByteString. Вы не можете. Его тип не упоминает тип элемента. Вы также не можете написать экземпляр для Set, потому что для него требуется ограничение Ord, но глава класса не упоминает тип элемента, поэтому вы не можете его ограничить.

типы Ассоциированные обеспечивают аккуратный способ, чтобы полностью устранить эти проблемы:

 
class HasFirst c where 
    type Element c :: * 
    first :: c -> Maybe (Element c) 

instance HasFirst [x] where 
    type Element [x] = x 
    first [] = Nothing 
    first (x:_) = Just x 

instance HasFirst ByteString where 
    type Element ByteString = Word8 
    first b = b ! 0 

instance Ord x => HasFirst (Set x) where 
    type Element (Set x) = x 
    first s = findMin s 

Теперь у нас есть новая проблема, однако. Рассмотрим пытается «исправить» Functor так, что он работает для всех типов контейнеров:

 
class Functor f where 
    type Element f :: * 
    fmap :: (Functor f2) => (Element f -> Element f2) -> f -> f2 

Это не работает. В нем говорится, что если у нас есть функция от типа элемента f до типа элемента f2, тогда мы можем включить f в f2. Все идет нормально. Однако, по-видимому, нет , чтобы требовать, чтобы f и f2 были одинаковым контейнером!

Согласно существующему Functor определению, мы имеем

 
fmap :: (x -> y) -> [x] -> [y] 
fmap :: (x -> y) -> Seq x -> Seq y 
fmap :: (x -> y) -> IO x -> IO y 

Но мы не имеют fmap :: (x -> y) -> IO x -> [y]. Это совершенно невозможно. Но определение класса выше позволяет это.

Кто-нибудь знает, как объяснить системе типа, что я имел в виду ?

Редактировать

Вышеуказанные работы по определению способ вычисления типа элемента от типа контейнера. Что произойдет, если вы попытаетесь сделать это наоборот? Определить функцию для вычисления типа контейнера из типа элемента? Легко ли это получается?

Answer 1

Ну, проблема в том, что неясно, что означает пересмотренный Functor. Например, рассмотрите ByteString. A ByteString может быть отображен только путем замены каждого элемента Word8 на элемент того же типа. Но Functor предназначен для параметрических отображаемых структур. На самом деле существуют два противоречивых понятия картирования:

• Жесткое картографирование (т.превращая каждый элемент структуры без изменения его типа)
• параметрического отображения (т.е. преобразование каждого элемента структуры любого типа)

Таким образом, в этом случае вы не можете объяснить систему типа, что вы имели в виду, потому что это не имеет большого смысла. Вы можете, однако, изменить то, что вы имеете в виду :)

Жесткого отображения легко выразить с семьями типа:

class RigidMap f where 
    type Element f :: * 
    rigidMap :: (Element f -> Element f) -> f -> f 

Насколько параметрическим отображением, есть несколько способов сделать это. Самый простой способ - сохранить текущий Functor как есть. Вместе эти классы охватывают такие структуры, как ByteString, [], Seq и т. Д. Однако все они падают на Set и Map из-за ограничения Ord на значения. К счастью, constraint kinds расширение идет в GHC 7.4 позволяет нам решить эту проблему:

class RFunctor f where 
    type Element f a :: Constraint 
    type Element f a =() -- default empty constraint 
    fmap :: (Element f a, Element f b) => (a -> b) -> f a -> f b 

Здесь мы говорим, что каждый экземпляр должен иметь связанный ограничение класса типов. Например, экземпляр Set будет иметь Element Set a = Ord a, чтобы обозначить, что Set s может быть сконструирован только в том случае, если для типа доступен экземпляр Ord. Все, что может появиться в левой части =>, принимается. Мы можем определить наши предыдущие экземпляры точно так, как они были, но мы также можем сделать Set и Map:

instance RFunctor Set where 
    type Element Set a = Ord a 
    fmap = Set.map 

instance RFunctor Map where 
    type Element Map a = Ord a 
    fmap = Map.map 

Однако, это очень раздражает, чтобы использовать два отдельных интерфейсов для жесткого отображения и ограниченного параметрического отображения. На самом деле, не последнее ли обобщение первого? Рассмотрим разницу между Set, которая может содержать только экземпляры Ord и ByteString, которые могут содержать только Word8. Неужели мы можем выразить это как еще одно ограничение?

Мы применяем тот же трюк делается для HasFirst (т.е. дать примеры для всей структуры и использовать тип семьи, чтобы выставить тип элемента), и ввести новое связано ограничение семьи:

class Mappable f where 
    type Element f :: * 
    type Result f a r :: Constraint 
    map :: (Result f a r) => (Element f -> a) -> f -> r 

Идея здесь заключается в том, что Result f a r выражает ограничения, необходимые для типа значения (например, Ord a), а также сдерживает результирующий тип контейнера, однако ему необходимо; предположительно, для обеспечения того, чтобы он имел тип одного сорта контейнера a. Например, Result [a] b r предположительно потребует, чтобы r было [b], а Result ByteString b r потребует, чтобы b было Word8, а r - ByteString.

Тип семей уже дает нам то, что нам нужно, чтобы выразить «есть» здесь: ограничение равенства типов. Мы можем сказать, что требуют, чтобы a и b были одного типа. Разумеется, мы можем использовать это в определениях семейств ограничений. Итак, у нас есть все, что нам нужно; по случаям:

instance Mappable [a] where 
    type Element [a] = a 
    type Result [a] b r = r ~ [b] 
    -- The type in this case works out as: 
    -- map :: (r ~ [b]) => (a -> b) -> [a] -> r 
    -- which simplifies to: 
    -- map :: (a -> b) -> [a] -> [b] 
    map = Prelude.map 

instance Mappable ByteString where 
    type Element ByteString = Word8 
    type Result ByteString a r = (a ~ Word8, r ~ ByteString) 
    -- The type is: 
    -- map :: (b ~ Word8, r ~ ByteString) => (Word8 -> b) -> ByteString -> r 
    -- which simplifies to: 
    -- map :: (Word8 -> Word8) -> ByteString -> ByteString 
    map = ByteString.map 

instance (Ord a) => Mappable (Set a) where 
    type Element (Set a) = a 
    type Result (Set a) b r = (Ord b, r ~ Set b) 
    -- The type is: 
    -- map :: (Ord a, Ord b, r ~ Set b) => (a -> b) -> Set a -> r 
    -- (note the (Ord a) constraint from the instance head) 
    -- which simplifies to: 
    -- map :: (Ord a, Ord b) => (a -> b) -> Set a -> Set b 
    map = Set.map 

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

Отказ от ответственности: Я еще не пробовал GHC 7.4, поэтому я не знаю, действительно ли кто-то из них собирает или работает, но я думаю, что основные идеи звучат.

Answer 2

Вы хотите constraint kinds, доступный в ghc 7.4.