Commentary and Examples

val x = [1, 2, 3, 4];

(* After each value I'll include a comment saying what the
PolyML terminal prints, e.g.:

val x = [1, 2, 3, 4]: int list
*)

fun f x y = x + y;

(*
val f = fn: int -> int -> int
*)

fun g x y = let
  in
    print ("1st arg: " ^ Int.toString x ^ "\n");
    print ("2nd arg: " ^ Int.toString y ^ "\n");
    x + y
  end;

(*
val g = fn: int -> int -> int
*)

fun h x = let
    val _ = print ("1st arg: " ^ Int.toString x ^ "\n")
    fun h1 y = let
      in
        print ("2nd arg: " ^ Int.toString y ^ "\n");
        x + y
      end
  in
    h1
  end;

(*
val h = fn: int -> int -> int
*)

(* All these functions have the same type but produce additional
I/O effects at different times. BTW, we don't have to use this
very explicit style, here's another way to write h:
*)

val h2 = (fn x => (print ("1st arg: " ^ Int.toString x ^ "\n");
  (fn y => (print ("2nd arg: " ^ Int.toString y ^ "\n");
    x + y))));


map (f 1) [1, 2, 3];

(*
val it = [2, 3, 4]: int list
*)

map (g 1) [1, 2, 3];

(*
1st arg: 1
2nd arg: 1
1st arg: 1
2nd arg: 2
1st arg: 1
2nd arg: 3
val it = [2, 3, 4]: int list
*)

map (h 1) [1, 2, 3];

(*
1st arg: 1
2nd arg: 1
2nd arg: 2
2nd arg: 3
val it = [2, 3, 4]: int list
*)

(*
The h function was given its 1st argument just once, but its 2nd
argument on three different occasions. This almost highlights a
major implementation challenge for the language: when (h 2 3) is
evaluated, the language must carefully manage the first phase of
computing (h 2) and then the second phase of computing (h 2) 3.
This ought to be skipped for a function like f, that needs both
arguments to do anything, but h and f have the same type, so the
language needs to do non-type analysis to tell them apart.
*)

-- If you want to print diagnostics, you can import debug
-- tracing. Because evaluation order is wacky, read the
-- results with care.
import Debug.Trace


-- In Haskell, the type [Int] may be infinite.

f :: () -> Int
f () =
    -- Fully evaluating xs would never finish.
    let xs = [1 ..] in
    12

-- The type list is equivalent to:

data List2 a = Nil2 | Cons2 a (List2 a)
  deriving (Show, Eq)

-- In our slides and inference rules etc, a type like
-- List2 would come with an induction scheme.

countForeverFromList2 :: Integer -> List2 Integer
countForeverFromList2 i = traceShow ("i is", i)
  (Cons2 i (countForeverFromList2 (i + 1)))

countForeverList2 :: List2 Integer
countForeverList2 = countForeverFromList2 1

-- This is a contradiction! We should be able to prove
-- that there is a greatest element in countForeverList2
-- by induction. That means that these aren't really
-- inductive datatypes in the usual sense.


-- In Haskell, laziness is permitted at every *constructor*.
-- e.g. we can construct Cons2 1 countForeverList2,
-- and a Cons2 actually gets created, even though its second
-- argument can't be fully evaluated. Each argument to Cons2
-- may be *thunk*. A thunk is a lot like a closure, it carries
-- an environment around so a computation can be run in the
-- right context.

-- You could convert a lazy language into a strict language,
-- by replacing every lazy value of type a with a strict value
-- of type () -> a. For instance, a lazy list/sequence in
-- a strict language might have a Cons constructor of type
-- LCons :: a -> (() -> LList a) -> LList a

-- So what happens? Like in function closures (() -> a), we
-- need to capture the environment. Because the language is
-- pure, evaluation order doesn't matter, so we can put off
-- evaluating the actual list, saving any environment args
-- as necessary as we would in exporting a function.


-- Here is another demo of laziness. This function doesn't
-- look useful, but it can be used to produce a result. The
-- key thing is that f has to be the kind of function that
-- lets us learn something without fully inspecting its
-- argument value x.

fixpoint :: (a -> a) -> a -> a
fixpoint f x = f (fixpoint f x)

v1 = fixpoint (\xs -> [1, 2] ++ xs) []

-- Nothing like the above could be useful in a strict semantics.