haskellml

Meaning of a recursive data type definition in lazy vs strict languages


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)


Solution

  • 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).