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:
Does Haskell not distinguish between inductive and coinductive types? If so, what's the formalization for that? If not, then which is [a]?
Is HList coinductive? If so, how can a coinductive type contain finite values?
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 justHList
?
HList
type is usually called a co-list. – Cactus