31

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?

tomahh
  • 13,441
  • 3
  • 49
  • 70
Crazycolorz5
  • 747
  • 6
  • 12
  • 7
    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. – Benjamin Hodgson Oct 04 '16 at 16:38
  • 1
    Your `HList` type is usually called a co-list. – Cactus Oct 05 '16 at 03:29

3 Answers3

26

  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.

Community
  • 1
  • 1
user2407038
  • 14,400
  • 3
  • 29
  • 42
  • 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. – gardenhead Oct 04 '16 at 21:31
  • 1
    @gardenhead 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. – Benjamin Hodgson Oct 04 '16 at 22:00
  • 1
    @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. – gardenhead Oct 04 '16 at 23:08
  • 1
    @gardenhead 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. – user2407038 Oct 04 '16 at 23:43
  • 1
    @gardenhead 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. – user2407038 Oct 04 '16 at 23:46
  • @user2407038 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. – gardenhead Oct 04 '16 at 23:49
  • @gardenhead 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`. – user2407038 Oct 04 '16 at 23:56
  • @user2407038 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. – gardenhead Oct 05 '16 at 00:07
  • 3
    @gardenhead 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? – user2297560 Oct 05 '16 at 00:54
  • @user2297560 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. – gardenhead Oct 05 '16 at 01:01
  • @gardenhead 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. – user253751 Oct 07 '16 at 21:54
  • @immibis But then the interpreter would have to determine if the program will halt... – gardenhead Oct 07 '16 at 21:57
  • @gardenhead 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? – user253751 Oct 07 '16 at 22:00
  • @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. – gardenhead Oct 07 '16 at 23:45
19

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.

Benjamin Hodgson
  • 42,952
  • 15
  • 108
  • 157
  • 1
    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? – Crazycolorz5 Oct 04 '16 at 17:24
  • 1
    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 – Benjamin Hodgson Oct 04 '16 at 17:47
6

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 ;-) ]

chi
  • 111,837
  • 3
  • 133
  • 218