[Solved]: Which fixpoint is Haskell list type?

ignougroup
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:

Best Answer from StackOverflow

Question Source : http://cs.stackexchange.com/questions/30481  Ask a Question  Download Related Notes/Documents