Are Lists Inductive or Coinductive in Haskell?

Question

So I've been reading about coinduction a bit lately, and now I'm wondering: are Haskell lists inductive or coinductive? I've also heard that Haskell doesn't distinguish the two, but if so, how do they do so formally?

Lists are defined inductively, data [a] = [] | a : [a], yet can be used coinductively, ones = a:ones. We can create infinite lists. Yet, we can create finite lists. So which are they?

Related is in Idris, where the type List a is strictly an inductive type, and is thus only finite lists. It's defined akin to how it is in Haskell. However, Stream a is a coinductive type, modeling an infinite list. It's defined as (or rather, the definition is equivalent to) codata Stream a = a :: (Stream a). It's impossible to create an infinite List or a finite Stream. However, when I write the definition

codata HList : Type -> Type where
    Nil : HList a
    Cons : a -> HList a -> HList a

I get the behavior that I expect from Haskell lists, namely that I can make both finite and infinite structures.

So let me boil them down to a few core questions:

1. Does Haskell not distinguish between inductive and coinductive types? If so, what's the formalization for that? If not, then which is [a]?

2. Is HList coinductive? If so, how can a coinductive type contain finite values?

3. What about if we defined data HList' a = L (List a) | R (Stream a)? What would that be considered and/or would it be useful over just HList?

Eolian

Haskell has no notion of inductive or coinductive types. (It doesn't really need one because it's a partial and lazy language.) So it doesn't really make sense to ask whether a given Haskell type is inductive or coinductive. – Confiteor

Your HList type is usually called a co-list. – Literalminded

Answer 1

1. Due to laziness, Haskell types are both inductive and coinductive, or, there is no formal distinguishment between data and codata. All recursive types can contain an infinite nesting of constructors. In languages such as Idris, Coq, Agda, etc. a definition like ones = 1 : ones is rejected by the termination checker. Laziness means that ones can be evaluated in one step to 1 : ones, whereas the other languages evaluate to normal form only, and ones does not have a normal form.

2. 'Coinductive' does not mean 'necessarily infinite', it means 'defined by how it is deconstructed', wheras inductive means 'defined by how it is constructed'. I think this is an excellent explanation of the subtle difference. Surely you would agree that the type

   codata A : Type where MkA : A

   cannot be infinite.

3. This is an interesting one - as opposed to HList, which you can never 'know' if it is finite or infinite (specifically, you can discover in finite time if a list is finite, but you can't compute that it is infinite), HList' gives you a simple way to decide in constant time if your list is finite or infinite.

Combustion

Can you explain how Haskell has both types? I'm pretty sure this isn't true. Every type in Haskell is lazy. So Haskell cannot represent inductive types like the natural numbers. It's simply impossible. – Logic

@Logic In my understanding it's not so much that all Haskell types are "both inductive and coinductive", but more that Haskell has neither inductive nor coinductive types. You can't represent coinductive types like Stream either. This is more a consequence of partiality than of laziness in my opinion. – Confiteor

@BenjaminHodgson What does partiality have to do with Stream? The data type type Stream = Nil | Cons nat * Stream should be the type of infinite streams under a lazy dynamics. How can a datatype be partial? Partiality only refers to functions. – Logic

@Logic Keep in mind that pretty much all formal treatment of Haskell as a system of logic relies on assumptions, such as undefined not coming into play, nor seq. I say that [] is both the inductive and coinductive list because you can write equivalent programs on Haskell lists to those in e.g. Agda or Coq which operate on both inductive and coinductive lists. – Combustion

@Logic And if you accept the afformentioned assumptions, you can really represent the naturals with data Nat = Z | S !Nat (note the strictness annotation) for which the definition inf = S inf is not generative, and more specifically is just equivalent to undefined. The same works for lists, I suppose: data FiniteList = Nil | Cons a !(FiniteList a) - this again makes things like ones non-generative and you get finite lists or bottom. – Combustion

@Combustion I am not very familiar with Haskell, so this strictness annotation is news to me. If Haskell has both eager and lazy types, then of course it can represent natural numbers. But I still stand by my claim that the standard definition of the naturals is not correct in Haskell. Again, due to my unfamiliarity with Haskell, I was not aware of undefined. But if it's just the bottom type then I don't see how it comes into the picture. – Logic

@Logic Typical presentations probably rely on the assumption that the infinite natural number not be constructed. This isn't much different than the assumption that undefined not be used in a program, which is the bare minimum for any other formal treatment of Haskell. undefined means that even if you correctly axiomize the natural numbers, your type will still be inhabited by a value which is not a natural number, namely undefined. – Combustion

@Combustion I don't think that's true. There are semantics of type systems that don't use undefined as an explicit value. For example, one can consider partial functions as the underlying domain. Then a function N -> N that doesn't halt on input x simply is not defined on x, instead of being defined with value undefined. Moreover, in an operational semantics, there is no need to even consider such notions as non-halting computation. Their meaning is given by their lack of termination. – Logic

@Logic Are you talking about a real programming language or a theoretical semantics that has the magical ability to tell when a function halts for any arbitrary input? – Supportable

@Supportable I'm not sure what you mean. Of course I'm not assuming that we can solve the Halting problem. I'm saying that in an operational semantics one does not need any "undefined" value, because the computation will never reach a value. – Logic

@Logic I'm sure it would be easy enough to modify a Haskell interpreter so that it enters an infinite loop instead of raising an "undefined" error, but pragmatically, that's less useful than raising the error. – Linder

@immibis But then the interpreter would have to determine if the program will halt... – Logic

@Logic No; with that modification it will always not halt when encountering undefined, instead of sometimes halting and sometimes not halting. Thus you can never have undefined as a value, you can only have a computation that never terminates. Isn't that what you wanted? – Linder

@immibis Maybe I misunderstood you? I think the confusion stems from using three different meanings of "bottom": a type, a construct in Haskell of that type, and a special value in certain denotational semantics. These are not the same thing. – Logic

Answer 2

In a total language like Coq or Agda, inductive types are those whose values can be torn down in finite time. Inductive functions must terminate. Coinductive types, on the other hand, are those whose values can be built up in finite time. Coinductive functions must be productive.

Systems that are intended to be useful as proof assistants (like Coq and Agda) must be total, because non-termination causes a system to be logically inconsistent. But requiring all functions to be total and inductive makes it impossible to work with infinite structures, thus, coinduction was invented.

So the purpose of inductive and coinductive types is to reject possibly non-terminating programs. Here's an example in Agda of a function which is rejected because of the productivity condition. (The function you pass to filter could reject every element, so you could be waiting forever for the next element of the resulting stream.)

filter : {A : Set} -> (A -> Bool) -> Stream A -> Stream A
filter f xs with f (head xs)
... | true = head xs :: filter f (tail xs)
... | false = filter f (tail xs)  -- unguarded recursion

Now, Haskell has no notion of inductive or coinductive types. The question "Is this type inductive or coinductive?" is not a meaningful one. How does Haskell get away without making the distinction? Well, Haskell was never intended to be consistent as a logic in the first place. It's a partial language, which means that you're allowed to write non-terminating and non-productive functions - there's no termination checker and no productivity checker. One can debate the wisdom of this design decision but it certainly renders induction and coinduction redundant.

Instead, Haskell programmers are used to reasoning informally about a program's termination/productivity. Laziness lets us work with infinite data structures, but we don't get any help from the machine to ensure that our functions are total.

Confiteor

In Agda, is it possible to define a structure similar to HList? In that case, are productivity constraints still imposed (as it is codata), and thus filter would still be invalid? That is, the introduction of Nil doesn't affect its validity? – Eolian

That's right. Coinductive lists can still be infinite (though unlike streams they might not be), so filter would still be rejected because it wouldn't be productive for all its inputs – Confiteor

Answer 3

To interpret type-level recursion one needs to find a "fixed point" for the CPO-valued list functor

F X = (1 + A_bot * X)_bot

If we reason inductively, we want the fixed point to be "least". If coinductively, "greatest".

Technically, this is done by working in the embedding-projection subcategory of CPO_bot, taking e.g. for the "least" the colimit of the diagram of embeddings

0_bot |-> F 0_bot |-> F (F 0_bot) |-> ...

generalizing the Kleene's fixed point theorem. For the "greatest" we would take the limit of the diagram of the projections

0_bot <-| F 0_bot <-| F (F 0_bot) <-| ...

It however turns out that the "least" is isomorphic to the "greatest", for any F. This is the "bilimit" theorem (see e.g. Abramsky's "Domain Theory" survey paper).

Perhaps surprisingly, it turns out that the inductive or coinductive flavor comes from the liftings applied by F instead of the least/greatest fixed points. For instance, if x is the smashed product and # is the smashed sum,

F X = 1_bot # (A_bot x X)

would have as a bilimit the set of finite lists (up to iso).

[I hope I got the liftings right -- these are tricky ;-) ]

Agrippina