HASKELL.SG

The Mathematics of Functors (by Dr. Shaun Martin)

Jan 24, 2014 · 7:30 PM
The Office

About the Venue:

http://www.theoffice.com.sg/where.php

Introduction:

We are happy to be able to invite Dr. Shaun Martin to give us a talk in pure mathematics. This talk would be about why functors are invented, how you can do some cool things with them. And its relation with Haskell.

Speaker Profile:

Dr Shaun Martin is the co-founder of Applied Cognitive Science: a company that uses cognitive science, behavioral economics and data science to build predictive models for strategic planning, innovation, and public policy.

Prior to founding Applied Cognitive Science he worked in academia: holding lecturing and research positions at MIT and at the Institute for Advanced Study at Princeton. He holds a DPhil from Oxford University.

Join or login to comment.

Hit enter to add your reply

Edwin J. P.

To follow up on my question about the automatic derivation of functors in haskell.. Is there a result that says, there is a unique instance of a functor for single parametric types? Perhaps that's why automatic derivation of functors is possible in haskell.

0 · January 24, 2014
- View all 8 replies
- Sönke H.
  
  I've tried to come up with a counter-example. The only thing I found so far are parametric types where there is no valid functor instance at all, whether derived or written manually. For example: data T a = T (a -> Int) .
  
  0 · January 31, 2014
- Edwin J. P.
  
  It is possible to write a functor instance for that which typechecks in haskell:
  
  data T a = T (a -> Int)
  
  instance Functor T where
  fmap _ _ = T (\_ -> 0)
  
  0 · January 31, 2014
- Herng Y.
  
  Edwin, your example doesn't satisfy the Identity law among the following laws that Functor instances should satisfy:
  
  (Identity) fmap id == id
  (Composition) fmap (f . g) == fmap f . fmap g
  
  1 · January 31, 2014
- Sönke H.
  
  Yes, I was talking about instances that satisfy the laws. When you allow instances that don't do that it's also easy to find types with two possible (i.e. non-unique) functor instances.
  
  0 · January 31, 2014
- Herng Y.
  
  The problem with the type T is that it's "in the wrong direction" - to illustrate that, T can be the instance of the Cofunctor class! (defined in http://hackage.haskel...)
  
  instance Cofunctor T where
  cofmap (a -> b) -> T b -> T a
  cofmap f (T bfunc) = T (bfunc . f)
  
  0 · January 31, 2014
- Herng Y.
  
  To answer Edwin's original question, here is a *sufficient condition* for a parametric type "P a" to have a "good" Functor instance (not only typechecks, also satisfies Functor laws) to be guaranteed:
  
  - It has an "extraction function" ext :: P a -> a
  - It has a "construction function" con :: a -> P a
  
  We usually have these easily when we define our own types, such as
  
  data Usual a = Usual {ext :: a} -- record syntax
  In this case, con = Usual. Then
  
  instance Functor P where
  fmap f ap = cons (f (ext ap))
  
  But this doesn't work for "data T a = T (a -> Int)" because neither the ext nor con functions have natural definitions. In a sense for each "a" there are "too many possible (a -> Int)", which is the fundamental problem.
  
  Then again I don't know whether this is *necessary*, nor is it how Functor instance derivation works.
  
  0 · January 31, 2014
- Edwin J. P.
  
  Hmm. I realize my mistake. Perhaps -XDeriveFunctor uses some type of constraint solver to see if both laws are satisfied and if it can't find one it just spits an error and gives up.
  
  0 · January 31, 2014
- Herng Y.
  
  If Haskell allows "ad-hoc polymorphism" (http://en.wikipedia.o...), or more specifically allows a function to inspect the type of one of its arguments, then I can define a type that has one Functor law-abiding instance for every integer k.
  
  data MorphInt a = MorphInt a
  instance Functor MorphInt where
  fmap f (MorphInt a) = if (f :: Int -> Int) (MorphInt (f (a - k)) + k) (MorphInt (f a))
  
  fmap here handles the type (Int -> Int) differently from other types (ad-hoc polymorphism: http://en.wikipedia.o...).
  
  0 · January 31, 2014
A former member

Interesting talk

0 · January 25, 2014
Edwin J. P.

To answer the question about the philosophy behind using category theoretic constructs in Haskell: category theory has done an excellent job to unify various brands of mathematics. People like to believe it will do the same for all knowledge including complex software we use daily. Such unification implies a more precise specification of common Design Patterns software engineers have discovered by trial and error. A precise specification of design patterns implies automatic methods to verify whether the patterns were followed by a novice programmer working on your code base. Ultimately software engineers aim to achieve the Hilbert's trams humanist dream of automatic reasoning and obsolescence of the human mind and it's pretentious superiority in this universe. But first we have to achieve Djikstra's dream of finding better solutions to managing complexity in software engineering and category theory could be an answer to that.

3 · January 24, 2014
Yogesh S.

This should be interesting. Will it be possible to give a general idea? Like category theory etc.

1 · January 6, 2014