Haskell: Equality constraint in instance

user_525980 0
Viewed 2783

I was reading through the announcement of ClassyPrelude and got to here:

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

The writer then mentioned that this would not work: 

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

Which makes sense to me, as c is completely unrelated to the constraint on the left.

However, what isn't mentioned in the article and what I don't understand is why this wouldn't work:

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

Could someone explain why this is different to the first mentioned definition? Perhaps a worked example of GHC type inference would be helpful?

haskell
2 Answers

to complete the @kosmikus answer

same applies to purescript - you need equality constraint to derive type properly (you can try here 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

But in idris you don't

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
user_35743790
Related