Haskell: ограничение равенства в экземпляре

Question

Я читал объявление ClassyPrelude и попал сюда:

instance (b ~ c, CanFilterFunc b a) => CanFilter (b -> c) a where
    filter = filterFunc

Затем автор упомянул, что это не сработает:

instance (CanFilterFunc b a) => CanFilter (c -> c) a where
    filter = filterFunc

Что имеет смысл для меня, так как c полностью не связано с ограничением слева.

Однако то, что не упомянуто в статье и что я не понимаю, это то, почему это не сработает:

instance (CanFilterFunc b a) => CanFilter (b -> b) a where
    filter = filterFunc

Может ли кто-нибудь объяснить, почему это отличается от первого упомянутого определения? Возможно, полезный пример вывода типа GHC будет полезен?

Answer 1

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

Нам нужны следующие расширения:

{-# LANGUAGE FlexibleInstances, TypeFamilies #-}

Давайте определим класс, который проще, чем CanFilterс одним параметром. Я определяю две копии класса, потому что я хочу продемонстрировать разницу в поведении между двумя экземплярами:

class Twice1 f where
  twice1 :: f -> f

class Twice2 f where
  twice2 :: f -> f

Теперь давайте определим экземпляр для каждого класса. За Twice1мы фиксируем переменные типа, чтобы они были одинаковыми напрямую, и для Twice2мы разрешаем им быть разными, но добавляем ограничение равенства.

instance Twice1 (a -> a) where
  twice1 f = f . f

instance (a ~ b) => Twice2 (a -> b) where
  twice2 f = f . f

Чтобы показать разницу, давайте определим другую перегруженную функцию, например:

class Example a where
  transform :: Int -> a

instance Example Int where
  transform n = n + 1

instance Example Char where
  transform _ = 'x'

Теперь мы находимся в точке, где мы можем увидеть разницу. Как только мы определим

apply1 x = twice1 transform x
apply2 x = twice2 transform x

и спросить GHC для предполагаемых типов, мы получаем, что

apply1 :: (Example a, Twice1 (Int -> a)) => Int -> a
apply2 :: Int -> Int

Это почему? Ну, экземпляр для Twice1 срабатывает только тогда, когда тип источника и цели функции совпадают. За transform и данный контекст, мы этого не знаем. GHC будет применять экземпляр только при совпадении правой части, поэтому мы остаемся с неразрешенным контекстом. Если мы попытаемся сказать apply1 0, будет ошибка типа, говорящая о том, что по-прежнему недостаточно информации для устранения перегрузки. Мы должны явно указать тип результата, который будет Int в этом случае, чтобы пройти.

Однако в Twice2, экземпляр для любого типа функции. GHC немедленно разрешит его (GHC никогда не возвращает обратно, поэтому, если экземпляр явно совпадает, он всегда выбирается), а затем попытается установить предварительные условия: в этом случае ограничение равенства, которое затем вынуждает тип результата быть Int и позволяет нам решить Example ограничение тоже. Мы можем сказать apply2 0 без дальнейших аннотаций типа.

Так что это довольно тонкий момент в разрешении экземпляров GHC, и здесь ограничение равенства помогает контролеру типов GHC таким образом, что пользователю требуется меньше аннотаций типов.

Answer 2

Чтобы завершить ответ @kosmikus

То же самое относится и к purescript - вам нужно ограничение равенства для правильного определения типа (вы можете попробовать здесь http://try.purescript.org/)

module Main where

import Prelude

-- copied from https://github.com/purescript/purescript-type-equality/blob/master/src/Type/Equality.purs
class TypeEquals a b | a -> b, b -> a where
  to :: a -> b
  from :: b -> a

instance refl :: TypeEquals a a where
  to a = a
  from a = a

-----------------

class Twice1 f where
  twice1 :: f -> f

class Twice2 f where
  twice2 :: f -> f

instance mytwice1 :: Twice1 (a -> a) where
  twice1 f = f >>> f

instance mytwice2 :: TypeEquals a b => Twice2 (a -> b) where
  twice2 f = f >>> from >>> f

class Example a where
  transform :: Int -> a

instance exampleInt :: Example Int where
  transform n = n + 1

instance exampleChar :: Example Char where
  transform _ = 'x'

{--
-- will raise error
--   No type class instance was found for Main.Twice1 (Int -> t1)

apply1 x = twice1 transform x

-- to resolve error add type declaration
apply1 :: Int -> Int

--}

-- compiles without error and manual type declaration, has type Int -> Int automatically
apply2 x = twice2 transform x

---

Но в idris вы не

module Main

import Prelude

interface Twice f where
  twice : f -> f

Twice (a -> a) where
  twice f = f . f

interface Example a where
  transform : Int -> a

Example Int where
  transform n = n + 1

Example Char where
  transform _ = 'x'

-- run in REPL to see that it derives properly:

-- $ idris src/15_EqualityConstraint_Twice_class.idr
-- *src/15_EqualityConstraint_Twice_class> :t twice transform
-- twice transform : Int -> Int

-- Summary:
-- in idris you dont need equality constaint to derive type of such functions properly