In what condition we should use `[ ] a` in a type declaration?

  • A+
Category:Languages

I just see an expression

fmap_List :: (a -> b) -> [] a -> [] b -- "[] a" means "[a]", for types. fmap_List f [] = [] fmap_List f (x:xs) = f x : fmap_List f xs 

Since [] a means [a], why we don't put [a] directly instead? Are there some special cases we should use [] a?

 


It’s just avoiding the syntactic sugar [a] as a way of illustrating that the f type parameter of fmap :: Functor f => (a -> b) -> f a -> f b is being replaced with the type constructor [], just like any other type constructor.

That is, you might write the type [a] as [] a when you want to emphasise the relationship to a signature that’s polymorphic over some type constructor, like fmap:

fmap       :: Functor f => (a -> b) ->     f a ->     f b  -- f = [] fmap_List  ::              (a -> b) ->    [] a ->    [] b fmap_List = fmap  -- f = Maybe fmap_Maybe ::              (a -> b) -> Maybe a -> Maybe b fmap_Maybe = fmap 

Or join:

join      :: Monad m =>  m ( m a) ->  m a join_List ::            [] ([] a) -> [] a 

This is exactly the same as [[a]] -> [a], just making it clearer that m = [].

[] a is the type constructor [] applied to the type variable a. [] a or [a] has the kind *, the kind of types that are inhabited by values, such as Int, Char, Maybe Int, or Either String Int. [] has kind * -> *, the kind of types that take a type argument and produce a type as a result, such as [], Maybe, Identity, or Either e.

You can see this for example in the definition of instance Monad []—we’re giving the constructor [] (of kind * -> *) as an argument to Monad (of kind (* -> *) -> Constraint), not a type (of kind *) made with that constructor such as instance Monad ([] a). This is just like using Maybe instead of Maybe a, Maybe Int, Maybe String, &c.

Using the TypeApplications pragma, you can explicitly apply polymorphic functions to type arguments, e.g. in GHCi:

> :set -XTypeApplications  > :type fmap @[] fmap @[] :: (a -> b) -> [a] -> [b]  > :type fmap @Maybe fmap @Maybe :: (a -> b) -> Maybe a -> Maybe b  > :type fmap @[] @Int @Char fmap @[] @Int @Char :: (Int -> Char) -> [Int] -> [Char]  > :type fmap @[] @_ @Bool fmap @[] @_ @Bool :: (a -> Bool) -> [a] -> [Bool] 

This is very useful for figuring out how to use polymorphic functions, or documenting which container or monad you’re using such a function with, by specialising a type to a (more) concrete instance:

> :type traverse traverse :: (Traversable t, Applicative f) => (a -> f b) -> t a -> f (t b)  > :type traverse @[] @IO traverse @[] @IO :: (a -> IO b) -> [a] -> IO [b] 

And you can also ask GHCi for the kind of a type to get a better understanding of kinds:

> :kind Either Either :: * -> * -> *  > :kind Either String Either String :: * -> *  > :kind Either String Int Either String Int :: *  > :kind [] [] :: * -> *  > :kind [] Int [] Int :: *  > :kind [Int] [Int] :: *  > :kind Functor Functor :: (* -> *) -> Constraint  > :kind Num Num :: * -> Constraint 

Comment

:?: :razz: :sad: :evil: :!: :smile: :oops: :grin: :eek: :shock: :???: :cool: :lol: :mad: :twisted: :roll: :wink: :idea: :arrow: :neutral: :cry: :mrgreen: