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

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

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

{-# 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 проверять типы таким образом, что пользователю требуется меньше аннотаций типов.

завершить ответ @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

Но в Идрисе вы'не

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