Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

implementation of sequenceA using traverse

Tags:

types

haskell

sequenceA is implemented as following in Data.Traversable

 sequenceA :: Applicative f => t (f a) -> f (t a)
 sequenceA = traverse id

I have trouble understanding the type of traverse id. traverse has the type: traverse :: Applicative f => (a -> f b) -> t a -> f (t b) Its first parameter is of type: (a -> f b) But in the case of sequenceA, the type of the id function is (a -> a). Where is f?

like image 423
user12457 Avatar asked Jun 10 '17 13:06

user12457


1 Answers

Let's first of all say that id has the type id :: c -> c to make things less complicated. The a in a type signature of a function is local in the sense that the a of id :: a -> a has nothing to do with the a in traverse :: Applicative f => (a -> f b) -> t a -> f (t b). a is just a type parameter.

So now we have the expression:

traverse id

with:

traverse :: Applicative f => (a -> f b) -> t a -> f (t b)
id       ::                   c -> c

I wrote the c -> c part at the same columns of the a -> f b part to show how the Haskell type system interacts. It now derives that:

a   ~ c
f b ~ c

So that means that a ~ c ~ f b and since type equality, like every equality relationship is transitive, it thus also means that a ~ f b. So now Haskell specializes traverse id into:

traverse id :: Applicative f => t a -> f (t b)
traverse id :: Applicative f => t (f b) -> f (t b) -- a ~ f b

So hence the type. The id type in traverse id has type id :: f b -> f b.

like image 83
Willem Van Onsem Avatar answered Nov 19 '22 15:11

Willem Van Onsem