10
$\begingroup$

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.

Improve this question
$\endgroup$
5
$\begingroup$

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:

Improve this answer
$\endgroup$
2
  • $\begingroup$ I think you are missing an x in that datatype declaration... $\endgroup$
    – miniBill
    Oct 9 '14 at 6:21
  • 2
    $\begingroup$ 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. $\endgroup$
    – Andrej Bauer
    Oct 13 '14 at 7:09
10
$\begingroup$

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.

Improve this answer
$\endgroup$
4
  • $\begingroup$ Many people are in denial? $\endgroup$
    – miniBill
    Oct 2 '14 at 3:39
  • 2
    $\begingroup$ Sure, I meet people who try to prove things by induction on lists, trees, etc. in Haskell. They pretend all these datatypes are inductive. $\endgroup$
    – Andrej Bauer
    Oct 2 '14 at 20:18
  • $\begingroup$ And you can't prove things by induction on lists? $\endgroup$
    – miniBill
    Oct 3 '14 at 8:40
  • 2
    $\begingroup$ 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. $\endgroup$
    – Andrej Bauer
    Oct 9 '14 at 18:07

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.