% Unprogramming a permutation machine

stack([],[],[]) --> [].
stack([push|Instrs],[I|IS],SS) --> stack(Instrs,IS,[I|SS]).
stack([pop|Instrs],IS,[S|SS]) --> [S], stack(Instrs,IS,SS).

% ?- phrase(stack(Instructions, [1,2,3,4,5], []), [1,2,4,3,5], []).
% Instructions = [push, pop, push, pop, push, push, pop, pop, push, pop] .

Tail Call Optimization doesn't exist in Haskell

It's well known that since Haskell programs are evaluated lazily, the
considerations for writing recursive code are different to those of a strict
language.

> cat (zero,plus) [] = zero
> cat (zero,plus) (x:xs) = x `plus` cat (zero,plus) xs

> cat' (zero,plus) [] acc = acc
> cat' (zero,plus) (x:xs) acc = cat' (zero,plus) xs (acc `plus` x)

> loads = [1..1000000]

*Main> cat (0,(+)) loads
*** Exception: stack overflow
*Main> cat' (0,(+)) loads 0
*** Exception: stack overflow


Since normal numbers in haskell are strict, I'm going to use lazy numbers here
(The hope is that any results should apply to lazy structures in general, and
avoid having to take strictness into account).

> data N = Z | S N     deriving Show

> zero = Z
> plus (S x) y = S (plus x y)
> plus   Z   y = y

> lots = take 1000000 . iterate S $ Z

*Main> cat (zero,plus) lots
S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S^C(S (S (S (S Interrupted.
*Main> cat' (zero,plus) lots Z
*** Exception: stack overflow


Another example is an infinite loop:

*Main> let f x = f x in f []
^CInterrupted.
*Main> let f x = f (():x) in f []
^CInterrupted.

Both continue happily, the second takes up huge amounts of memory but it does
not stack overflow.

Haskell evaluation is like graph reduction, a program is a graph which you tug
on the end until you get a weak head normal form, in these cases you never get
one, but the program/graph is stored on the heap, in the second case that data
gets bigger and bigger (it might even get swapped to the hard disk after a
while).

That's why they didn't crash, and it had nothing to do with tail calls or tail
call optimization,  cat (zero,plus) lots  didn't do any tail call and that
didn't crash. The reason any stack overflow occurs is that the program which
reduces the graph (on the heap) has a stack, that program in my case GHC is
written in C (the RTS) and when it delves deep into an expression such as
1 + (2 + (3 + (4 + ...)))   that is what builds up stack.



So why does something like:

> spam = putStr "SPAM " >> spam

never crash?

Since (>>) is in tail position (spam is not a tail call), again, tail calls have
nothing to do with this.  m >> n  in this case means do m throw away the result
then do n, it must get thrown to the garbage collector (unlike the  f (():x)
example where the value can't be collected).



That's all fine, but we still haven't been able to sum  [1..1000000]  together.
So to recap, building up a huge expression on the heap is fine (as in the
cat (zero,plus) lots  example) but walking deep into an expression without
getting any constructors is dangerous.

> kat' (zero,plus) [] acc = acc
> kat' (zero,plus) (x:xs) acc = acc'plus'x `seq` kat' (zero,plus) xs acc'plus'x
>  where acc'plus'x = acc `plus` x

*Main> cat' (0,(+)) loads 0
*** Exception: stack overflow
*Main> kat' (0,(+)) loads 0
500000500000


> -- And a huge thanks to everyone that I talked about this with
> -- for bending my mind :)

Correctness of an Expression Compiler in Coq

This is based on Correctness Of A Compiler For Arithmetic Expressions and A type-correct, stack-safe, provably correct expression compiler in Epigram

Require Import List.

Fixpoint Tuple (types : list Set) : Type :=
  match types with
    | nil => unit
    | t::ts => (t * Tuple ts)%type
  end.

Inductive Exp : Set -> Type :=
| Num : nat -> Exp nat
| Boo : bool -> Exp bool
| Sum : Exp nat -> Exp nat -> Exp nat
| Eql : Exp nat -> Exp nat -> Exp bool
| Iff : forall (a : Set), Exp bool -> Exp a -> Exp a -> Exp a.

Fixpoint nat_eq_bool (x y : nat) {struct x} : bool :=
  match x, y with
    | O, O => true
    | S x', S y' => nat_eq_bool x' y'
    | _,_ => false
  end.

Fixpoint eval (a : Set) (e : Exp a) : a :=
  match e in Exp t return t with
    | Num n => n
    | Boo b => b
    | Sum p q => eval _ p + eval _ q
    | Eql x y => nat_eq_bool (eval _ x) (eval _ y)
    | Iff _ b t e => if eval _ b then eval _ t else eval _ e
  end.

(* example *)
Eval compute in
  (eval _
    (Iff _ (Eql (Num 7) (Sum (Num 4) (Num 3)))
      (Sum (Num 5) (Num 8))
      (Num 0))).

Notation "x --> y" := (x,y) (at level 120, right associativity).

Inductive INST : list Set * list Set -> Type :=
| PUSHN : forall s, nat -> INST (s --> nat::s)
| PUSHB : forall s, bool -> INST (s --> bool::s)
| SUM : forall s, INST (nat::nat::s --> nat::s)
| EQL : forall s, INST (nat::nat::s --> bool::s)
| COND : forall s, forall a, INST (bool::a::a::s --> a::s).

Inductive stack : list Set -> Type :=
| snil : stack nil
| scons : forall p q, INST (p --> q) -> stack p -> stack q.

Fixpoint compile
  (a : Set) (e : Exp a)
  (tail : list Set) (rest : stack tail)
  { struct e } : stack (a::tail) :=
  match e in Exp a return stack (a::tail) with
    | Num n =>
      scons _ _ (PUSHN _ n) rest
    | Boo b =>
      scons _ _ (PUSHB _ b) rest
    | Sum u v =>
      scons _ _ (SUM _)
      (compile _ u _
        (compile _ v _ rest))
    | Eql x y =>
      scons _ _ (EQL _)
      (compile _ x _
        (compile _ y _ rest))
    | Iff a b t e =>
      scons _ _ (COND _ _)
      (compile _ b _
        (compile _ t _
          (compile _ e _ rest)))
  end.

Definition evinst :
  forall p q,
    forall (i : INST (p --> q)),
      Tuple p -> Tuple q :=
      fun p q i =>
        match i in INST pq return Tuple (fst pq) -> Tuple (snd pq) with
          | PUSHN _ n => fun s =>
            (n, s)
          | PUSHB _ b => fun s =>
            (b, s)
          | SUM _ => fun s =>
            match s with
              | (u, (v, s)) => (u + v, s)
            end
          | EQL _ => fun s =>
            match s with
              | (x, (y, s)) => (nat_eq_bool x y, s)
            end
          | COND _ _ => fun s =>
            match s with
              | (b, (t, (e, s))) =>
                (if b then t else e, s)
            end
        end.

Fixpoint evstack typs (program : stack typs)
  { struct program } : Tuple typs :=
  match program in stack typs return Tuple typs with
    | snil => tt
    | scons t ts i is => evinst _ _ i (evstack _ is)
  end.

Eval compute in
  (evstack _ (compile _
    (Iff _ (Eql (Num 7) (Sum (Num 4) (Num 3)))
      (Sum (Num 5) (Num 8))
      (Num 0)) nil snil)).

Lemma eval_correct :
  forall a (e : Exp a),
    forall typs (program_tail : stack typs),
      (eval a e, (evstack typs program_tail))
      =
      evstack (a::typs) (compile a e typs program_tail).
Proof.
  induction e.
  
  reflexivity.
  
  reflexivity.
  
  intros.
  unfold compile; fold compile; simpl.
  rewrite <- IHe1.
  rewrite <- IHe2.
  reflexivity.
  
  intros.
  unfold compile; fold compile; simpl.
  rewrite <- IHe1.
  rewrite <- IHe2.
  reflexivity.
  
  intros.
  unfold compile; fold compile; simpl.
  rewrite <- IHe1.
  rewrite <- IHe2.
  rewrite <- IHe3.
  reflexivity.
Qed.