Reading "Category Theory for Programmers" I am trying to recreate the Functor typeclass instance for Op.
{-# LANGUAGE TypeSynonymInstances #-}
module Type.Op where
import Data.Functor.Contravariant ( Contravariant, contramap )
type Op r a = a -> r
-- data Op r a = (->) a r
instance Contravariant (Op r) where
contramap f g = g . f
The compilation produces the following error:
• The type synonym ‘Op’ should have 2 arguments, but has been given 1
• In the instance declaration for ‘Contravariant (Op r)’
|
10 | instance Contravariant (Op r) where
| ^^^^^^^^^^^^^^^^^^^^
What should I do ? For the normal Functor
I would have used a partial type the same way...
CodePudding user response:
Let's consider a simpler class
class Unftor f where
unfmap :: (a -> a) -> f a -> f a
instance Unftor ((->) x) where
unfmap f g = f . g
Now, if what you tried to do were possible, I could also write
instance Unftor (Op r) where
unfmap f g = g . f
...but wait, let's look at the signatures in each case
instance Unftor ((->) x) where
unfmap :: (a -> a) -> (x -> a) -> (x -> a)
instance Unftor (Op r) where
unfmap :: (a -> a) -> Op r a -> Op r a
Since Op
is just a type synonym, that would be the same as
instance Unftor (\a -> (a -> r)) where
unfmap :: (a -> a) -> (a -> r) -> (a -> r)
Now, picking the special case that all types are Int
,
unfmap :: (Int -> Int) -> (Int -> Int) -> (Int -> Int)
unfmap f g = f . g -- from `instance Unftor ((->) x)`
unfmap :: (Int -> Int) -> (Int -> Int) -> (Int -> Int)
unfmap f g = g . f -- from `instance Unftor (Op r)`
...the same signature! But somehow the compiler is supposed to keep them apart??
That doesn't work.
What you need to do instead is make Op
a distinguishable type that's merely isomorphic to a -> r
. That's exactly what newtypes are there for (data
would also work):
newtype Op r a = Op {getOp :: a -> r}
instance Contravariant (Op r) where
contramap (Op f) g = Op $ g . f
CodePudding user response:
Remember that type synonyms are not types in their own right. They merely allow you to give new labels to existing things, and then talk about them using the labels instead of referring to them directly.
Type synonyms are completely transparent to most type system features, which can only work by substituting the definition of the synonym. A type synonym isn't a thing that "really exists" in order to have a class instance or not. That's why vanilla Haskell doesn't let you declare instances using type synonyms at all.
The TypeSynonymInstances
extension doesn't actually change this fundamental picture; all it does is let you declare instances for the underlying types used in the definition of a synonym, but using the synonym to refer to it. That sentence was a mouthful; example time:
{-# LANGUAGE TypeSynonymInstances, FlexibleContexts, FlexibleInstances #-}
data List a = a `Cons` List a | Nil
type Str = List Char
instance Eq Str
where x `Cons` xs == y `Cons` ys
= x == y && xs == ys
Nil == Nil = True
_ == _ = False
Here I've defined a new list type, and a new string synonym (much like the built in type String = [Char]
, but I didn't want existing instances to get in the way). Then I declared instance Eq Str
. But this doesn't really make an instance for Str
; it makes an instance for List Char
. All TypeSynonymInstances
did was let me use my label Str
as a standin for writing List Char
in the instance declaration; nothing more. The results are exactly the same as if I had written instance Eq (List Char)
. You can clearly see the distinction when I then do something like this:
isEmpty :: Eq (List a) => List a -> Bool
isEmpty xs = xs == Nil
The definition of isEmpty
needs an Eq (List a)
instance, but it doesn't itself know about Str
or Char
. This should not be usable if instance Str
was somehow different than instance (List Char)
. But with no other instances declared, I can still call isEmpty ('x' `Cons` Nil)
; GHC doesn't even need me to say whether I consider that a List Char
or a Str
because they are the same thing, and Eq Str
is the same thing as Eq (List Char)
.
If you think about it, defining a type synonym and then wanting to give it its own instances (separate from the underlying type) is a little bit like trying to say "let x = 5, and then we'll define what negation means for x by saying -x = -50". x isn't a new thing, it's just a name for 5. x neither needs nor can have its own definition of negation, because 5 already has one.
Now, lets bring this back to the OP's Op
type synonym. Synonyms are allowed to be more complicated than just a label for an existing type; they can be parameterised labels, like type Op r a = a -> r
. However it's still fundamentally true that Op
"doesn't really exist". Any time I use Op Foo Bar
I'm really just talking about Bar -> Foo
. And there is no sense in which instances for Op
can actually exist; only instances for the underlying type constructor ->
that is used in its definition.
For example, this fails with a duplicate instance error:
{-# LANGUAGE TypeSynonymInstances, FlexibleContexts, InstanceSigs #-}
type Op r a = a -> r
class Silly t
where silly :: t -> Bool
instance Silly (a -> r)
where silly :: (a -> r) -> Bool
silly _ = True
instance Silly (Op r a)
where silly = False
Op r a
already has an instance for Silly
, because a -> r
has one. I can't make any instances for Op
that I don't want regular ->
to have, and vice versa.
Now lets consider instance Contravariant (Op r)
. This can't "really" be declaring an instance for Op r
, only for the thing that's a synonym for. So we need something to substitute for Op r
to know what instance we're declaring, but what? Op r a
is well-defined; it means a -> r
. But to expand just Op r
we need to be able to partially apply ->
to its second argument. That's not something you can even really express directly in Haskell1. So it's certainly not something you can make an instance of a type class.
To avoid problems like this, type synonyms must be supplied with all of their parameters. This means that the compiler can "look through" the synonym to see what types you're really talking about. Partially applied type synonyms aren't guaranteed to be meaningful at all, so GHC normally forbids them.2 In the cases where a partially applied synonym could expand to something sensible, you just have to write the expansion yourself to declare an instance.
In cases like this where the partially applied synonym can't expand to something sensible, you just can't declare the instance. You can always use a newtype
rather than a type synonym; since these create real new types, not just labels for existing types, there's no problem with them being partially applied:
newtype Op r a = Op { getOp :: a -> r }
instance Contravariant (Op a) where
contramap :: (r' -> r) -> (Op a r -> Op a r')
contramap f g = Op (getOp g . f)
A new type is what you need anyway if you don't want the underlying type constructor to also get the instance (i.e. you want an instance for Op
without also making an instance for ->
).
Indeed, the Data.Functor.Contravariant
module already defines Op
as a newtype
(and this Contravariant
instance), precisely because the class system can only work with partial application of type constructors "in the right order". Op
only exists to be a version of ->
that takes its parameters in the opposite order so that instances can be declared. If partial application of ->
to its second argument was possible, there would be no need for Op
, we'd just write something like:
instance Contravariant (-> r)
where contramap f g = g . f
Then we'd be able to write fmap ( 1) func
or contramap ( 1) func
depending on whether we wanted to post-process func's result with ( 1)
or pre-process func's argument with ( 1)
. But Haskell's type system does not support this.
1 At the value level we have operator sections, and so could write (-> r)
. That's really just shorthand for a function defined as \a -> a -> r
though, whereas we have direct syntactic support for partial application to first arguments. Regardless, we don't have operator sections at the type
level.
2 In some contexts GHC is clever and can work with partially applied synonyms, if you turn on LiberalTypeSynonyms
. It does this by basically waiting to see if the type expression the partially-applied synonym appears in eventually provides the missing arguments, so that everything becomes well defined. For example this works:
{-# LANGUAGE LiberalTypeSynonyms #-}
type Op r a = a -> r
type OnInt f = f Int
foo :: OnInt (Op String)
-- foo :: (Op String) Int
-- foo :: Op String Int
-- foo :: Int -> String
foo x = show x
Op String
isn't a well defined type expression on its own at all, but GHC temporarily ignores that and passes this "unevaluated" to OnInt
anyway, which results in Op String Int
, which is well defined so it's okay. That still doesn't mean that Op String
is a first class type expression that we could try to make an instance for, however.