Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

instance of "Type constructed with type argument" need not be constructed with data of that type, in Haskell

Tags:

types

haskell

In Haskell, a type constructor can take a type argument, of course.

A function a -> b, when looked at as a "type with a funny constructor name", has type (->) a b. That makes it a type constructor (->) with two arguments, a and b. This is frequently encountered in the "reader" pattern as in its Functor and Applicative instances:

instance Functor ((->) a) where
  fmap = (.)


instance Applicative ((->) a) where
  pure = const
  (<*>) f g x = f x (g x)

When I first tried to understand uses of this instance, as in fmap (+1) (*2) 3 (=== (+1) . (*2) $ 3 === 3*2+1 === 7)

my reaction was "Ok, (+1) has type Int -> Int, which is (->) Int Int, so that matches Functor.... but where is the Int? I make a Maybe Int by calling Just 1, but I don't ever make a (->) Int Int by applying anything to an Int. In fact, I destroy a ((->) Int Int) by applying it to an Int! (Yeah, there's Nothing, but that seems... degenerate.)"

This all works (of course), as long as I remember that just because a type is built from a constructor+argument, that doesn't mean its values are built from a correspondingly typed constructor+argument. And some of the most interesting and powerful (and tricky to understand) type constructors are like this ((->), Lens, Arrow, etc)

(OK, really it's Num a => a, not Int, but let's ignore that, not relevant)

Is there a name for this concept? What is the appropriate mental model for thinking about type constructors, without leaning on the misleading and disempowering crutch interpretation "Foo a is a structure Foo containing value(s) of type a)?

like image 369
misterbee Avatar asked Oct 01 '22 23:10

misterbee


1 Answers

This concept is known as a contravariant functor, on in Haskell-speak a Contravariant type.

class Contravariant f where
  contramap :: (b -> a) -> f a -> f b

-- compare
class Functor f where
  fmap :: (a -> b) -> f a -> f b

More generally, we can think of type variables in a type as having contravariant or covariant nature (at its simplest). For instance, by default we have

newtype Reader t a = Reader (t -> a)

instance Functor (Reader t) where
  fmap ab (Reader ta) = Reader (ab . ta)

Which indicates that the second type parameter to Reader is covariant, while if we reverse the order

newtype RevReader a t = RevReader (t -> a)

instance Contravariant (RevReader a) where
  contramap st (RevReader ta) = RevReader (ta . st)

A useful intuition for Contravariant types is that they have the ability to consume zero, one, or many values of the contravariant parameter instead of containing zero, one, or many values of the covariant parameter like we often think of when considering Functors.

Combining these two notions is the Profunctor

class Profunctor p where
  dimap :: (a -> b) -> (c -> d) -> p b c -> p a d

which, as we notice, demands that p is of kind * -> * -> * where the first type parameter is contravariant and the second covariant. This class well characterizes the (->) type constructor

instance Profuntor (->) where
  dimap f g h = g . h . f

Again, if we think of contravariant type parameters as being consumed and covariant ones as being produced this is quite amenable of the typical intuition around (->) types.

A few more examples of types which contravariant parameters include Relation

newtype Relation t = Relation (t -> t -> Bool)

instance Contravariant Relation where
  contramap g (Relation pred) = Relation $ \a b -> pred (g a) (g b)

Or Fold which represents a left fold as a data type

newtype Fold a b = Fold b (a -> Fold a b)

instance Profunctor Fold where
  dimap f g (Fold b go) = Fold (g b) (go . f)

sumF :: Num a => Fold a a
sumF = go 0 where
  go n = Fold n (\i -> go (n + i))

With Fold a b we see that it consumes an arbitrary number of a types to produce one b type.

Generally what we find is that while it's often the case that we have covariant and "container" (strictly positive) types where values of some type c a are produced from a constructor of type a -> c a and some filler values a, in general that doesn't hold. In particular we have covariant types like that, but also contravariant ones which are often processes which somehow consume values of their parameterized type variables, or even more exotic ones like phantom types which utterly ignore their type variables

newtype Proxy a = Proxy -- need no `a`, produce no `a`

-- we have both this instance
instance Functor Proxy where
  fmap _ Proxy = Proxy

-- and this one, though both instances ignore the passed function
instance Contravariant Proxy where
  contramap _ Proxy = Proxy

and... "nothing special" type variables which cannot have any sort of nature, usually because they're being used as both covariant and contravariant types.

data Endo a = Endo (a -> a)

-- no instance Functor Endo or Contravariant Endo, it needs to treat
-- the input `a` differently from the output `a` such as in 
--
-- instance Profunctor (->) where

Finally, a type constructor which takes multiple arguments may have different natures for each argument. In Haskell, the final type parameter is usually treated specially, though.

like image 156
J. Abrahamson Avatar answered Oct 13 '22 10:10

J. Abrahamson