# Which fixpoint is Haskell list type?

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.

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:

• I think you are missing an x in that datatype declaration... Oct 9 '14 at 6:21
• There's a reason Jeremy called that paper "fast & loose". This answer is exactly the sort of denial I am talking about. It's the greatest fixed point, end of story. Jeremy's first linked paper is about that, for instance. Oct 13 '14 at 7:09

It's the greatest fixed point, or the final coalgebra, depending on how you set things up. In Haskell it is impossible to define the datatype of finite lists because Haskell does not have inductive types, only the coinductive ones. Many people are in denial about this particular issue.

• Many people are in denial? Oct 2 '14 at 3:39
• Sure, I meet people who try to prove things by induction on lists, trees, etc. in Haskell. They pretend all these datatypes are inductive. Oct 2 '14 at 20:18
• And you can't prove things by induction on lists? Oct 3 '14 at 8:40
• You cannot prove properties of the type [a] in Haskell by induction. You can do it for a subset of the values, namely the finite lists. But this is not what [a] is. Oct 9 '14 at 18:07