// This program is in Microsoft F# .Net: get from fsharp.org

module Lambdacalc
open System;
(*
   To load script into interactive interpreter:
   start dotnet fsi
   #load "lambdacalc.fsx";;
   open Lambdacalc;;

   lambda x.A is written fun x -> A in F#
   lambda x.lambda y.A is fun x y -> A, or fun x -> fun y -> A

   ETA CONVERSION: one thing we sometimes need in F# is eta-conversion:
   f = fun x -> f x, or A = lambda x. A x
*)

// Pure Typed Lambda Calculus in F#

let I = fun x -> x;  // lambda x.x, see inferred type below
let K = fun x y -> x; 
let S = fun x y z -> x z (y z);

// Note that fun x y -> y is same as fun x -> fun y -> x, but not the same
// as fun (x,y) -> y.  The (,) indicates a PAIR, which is built-in to F#.
// All functions are "Curried" by default.

let TRUE (x:'a) (y:'a) = x;
let FALSE (x:'a) (y:'a) = y;

// call-by-value if-else
let IFELSE0 = fun a b c -> (a b c);
// simulated call-by-name if-else
let IFELSE = fun a b c -> (a b c)(); // apply dummy lambda

IFELSE TRUE (fun ()-> 1) (fun() -> 1/0);; // doesn't crash

// boolean operators:
let AND = fun x y -> x y FALSE
let OR = fun x y -> x TRUE y
let NOT = fun x -> x FALSE TRUE

// cons pairs and lists
let CONS x y = (x,y);
let CAR (x,y) = x;
let CDR (x,y) = y;

type List<'T> = NIL | Node of 'a * List<'T>

// Recursion, unlike in the untyped-case, must be added to the typed
// lambda calculus as an external (extra) constant:

let rec FIX M = M (FIX M);

// Note that FIX can be defined because F# already supports recursive
// definitions (let rec), so it already has something equivalent built-in.


// Church Numerals
let church2 = fun f x -> f (f x);
let church3 = fun f x -> f (f (f x));
let ONE = fun f x -> f x;
let SUCC = fun n f x -> n f (f x);
let ADD = fun m n f x -> m f (n f x);
let TIMES = fun m n f x -> m (n f) x;
let EXPT = fun m n -> n m;
let ISZERO = fun n -> n (fun x -> FALSE) TRUE
let BASE x = CONS ZERO ZERO x
let NEXT = fun p -> CONS (CDR p) (SUCC (CDR p))
let PRED = fun n -> CAR (n NEXT BASE)
let SUBTRACT = fun m n -> n PRED m;

let Sum = FIX (fun f n ->
  match n with
    | NIL -> 0
    | Node(x,rest) -> (+) x (f rest));;
    

(*  Inferred Types:  (printed up on #load "lambdacalc.fsx")

  val I : x:'a -> 'a
  val K : x:'a -> y:'b -> 'a
  val S : x:('a -> 'b -> 'c) -> y:('a -> 'b) -> z:'a -> 'c
  val TRUE : ('a -> 'b -> 'a)
  val ZERO : x:'a -> ('b -> 'b)
  val FALSE : ('a -> 'b -> 'b)
  val IFELSE0 : a:('a -> 'b -> 'c) -> b:'a -> c:'b -> 'c
  val IFELSE : a:('a -> 'b -> unit -> 'c) -> b:'a -> c:'b -> 'c
  val AND : x:('a -> ('b -> 'c -> 'c) -> 'd) -> y:'a -> 'd
  val OR : x:(('a -> 'b -> 'a) -> 'c -> 'd) -> y:'c -> 'd
  val NOT : x:(('a -> 'b -> 'b) -> ('c -> 'd -> 'c) -> 'e) -> 'e
  val CONS : x:'a -> y:'b -> s:('a -> 'b -> 'c) -> 'c
  val CAR : p:(('a -> 'b -> 'a) -> 'c) -> 'c
  val CDR : p:(('a -> 'b -> 'b) -> 'c) -> 'c
  val NIL : ('a -> 'b -> 'b)
  val ISNIL :
    p:(('a -> 'b -> 'c -> 'd -> 'e -> 'e) -> ('f -> 'g -> 'f) -> 'h) -> 'h       
  val church2 : f:('a -> 'a) -> x:'a -> 'a
  val church3 : f:('a -> 'a) -> x:'a -> 'a
  val ONE : f:('a -> 'b) -> x:'a -> 'b
  val SUCC : n:(('a -> 'b) -> 'b -> 'c) -> f:('a -> 'b) -> x:'a -> 'c
  val ADD : m:('a -> 'b -> 'c) -> n:('a -> 'd -> 'b) -> f:'a -> x:'d -> 'c
  val TIMES : m:('a -> 'b -> 'c) -> n:('d -> 'a) -> f:'d -> x:'b -> 'c
  val EXPT : m:'a -> n:('a -> 'b) -> 'b
  val ISZERO : n:(('a -> 'b -> 'c -> 'c) -> ('d -> 'e -> 'd) -> 'f) -> 'f        
  val FIX : M:('a -> 'a) -> 'a

  // functions that don't take arguments (not pure lambda calculus) are
  // of type unit -> .. and those that don't return values are of type
  // .. -> unit.
*)


// convert built-in numbers to church numerals
let rec tochurch n =
  match n with
    | 0 -> ZERO
    | n -> SUCC (tochurch (n-1));;

let fromchurch n = n (fun x -> x+1) 0;

let church5 = tochurch 5
let fromchurch5 = fromchurch church5
let nottrue = fromchurch ZERO
let notfalse = fromchurch ONE
let r x = ISZERO ZERO x
//printfn "%d" fromchurch5;  // prints 5
//printfn "%d" (fromchurch (fun x-> ISZERO ZERO x))
let tobool x = x true false;
printfn "%A" (tobool TRUE);
printfn "%A" (tobool FALSE);
let frombool x = if x then TRUE else FALSE;
printfn "%A" (tobool r);
let r2 = ISZERO ONE;
printfn "%A" (tobool r2);