If I write something like
data L t = Empty | L t (L t)
in haskell this type admits infinite lists like L 1 (L 2 (L 3 (..)))
. Does an equivalent algebraic type definition in a strict language like ML also admit infinite lists? If so, is it a deficiency in the evaluation mechanism of the language that you can't actually give it an infinite list? And if not, how does ML exclude infinite lists from that type?
Secondly, from a theoretical standpoint, is the class of values in the type the least fixed point of some generator function? (c.f. the value of a recursive function definition like factorial is the lfp of an associated generator function)
In OCaml there are cyclic lists:
let rec c = 1 :: 2 :: 3 :: c
how does ML exclude infinite lists from that type?
If you forbid recursive definitions for non-function types, then there is no way to construct an infinite list.
from a theoretical standpoint, is the class of values in the type the least fixed point of some generator function?
Fixed points are indeed a common way to model types in denotational semantics. First purely symbolically, we can see that:
L a = Nil | Cons a (L a)
makes L a
a fixed point of F
:
F x = Nil | Cons a x
Indeed, we have:
L a = F (L a)
Here Nil
denotes the unit space, Cons a x
is the product of a
and x
, and |
is sum.
You get different results depending on the meaning of "space" and those operations (unit, products and sums).
If you think of those as just sets, then the smallest fixed point is the set of finite lists. The "greatest fixed point"---actually, the final coalgebra---is the set containing both finite and infinite lists.
The other common kind of space for this are domains, order structures that represent "partially computed values", notably ω-complete partial orders. With some appropriate notion of sum and product, you get the space of finite and infinite lists and their partial prefixes (⊥
, ⊥ : ⊥
, 1 : ⊥
, ⊥ : ⊥ : ⊥
...) as both the initial algebra and final coalgebra of the above F
(generalizations of "smallest fixed points" and "greatest fixed points" when talking about operations on (not of) algebraic structures).