[Solved]: Which fixpoint is Haskell list type?

Problem Detail: 

Let's say that lists are defined as

List a = Nil | Cons a (List a) 

Then, in Haskell is List x the greatest or least fixpoint? I'm asking because the lfp should exclude infinite lists (but you can build them in Haskell), whereas the gfp should exclude finite ones.

Asked By : miniBill

Answered By : Sterling Clover

The proper thing is to setup

data ListF a x = Nil | Cons a x 

Now you can write

newtype Mu f= Mu (forall a.(f a->a)->a) data Nu f   = forall a. Nu a (a->f a) 

In Haskell we can observe that Mu ListF and Nu ListF coincide. So, it can be either (!). (one source on this claim: http://www.cs.ox.ac.uk/jeremy.gibbons/publications/adt.pdf)

Additionally, we can prove things by induction on all lists and get proofs that work as long as we limit ourselves to caring about finite ones, as described here: http://www.cs.ox.ac.uk/jeremy.gibbons/publications/fast+loose.pdf

Two other references on this are:

• http://homepages.inf.ed.ac.uk/wadler/papers/free-rectypes/free-rectypes.txt (which is a historically pivotal document)

• http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.37.1418 (which is an excellent exposition)

Best Answer from StackOverflow

Question Source : http://cs.stackexchange.com/questions/30481

 Ask a Question

 Download Related Notes/Documents