example.levy

# This example file can be run with levy as
#
# ./levy.byte example.levy
#
# or interactively from the levy toplevel as
#
# levy> $use "example.levy"


# Basic arithmetic: 
2 + 2 ;;
2 * 3 ;;
2 - 4 ;;
-4 + -3 ;; # There's no unary minus, but there are negative integer constants

# Conditional statement (the then and else clauses must be
# computations):

if 5 < 3 then return 1 else return 5 ;;
if 2 = 2 then return 1 else return 5 ;;

# Function are written like in MiniHaskell (they map from
# values to computations):

fun n : int -> return (n + 3) ;;

fun n : int -> if n < 0 then return (0 - n) else return n ;;

# The syntax for fixpoint is like in MiniHaskell. The factorial function:

rec f : int -> F int is fun n : int ->
  if n = 0 then
    return 1
  else
    ((force f) (n - 1) to m in return (n * m)) ;;

# Features specific to call-by-push-value:

# return

return 42 ;;

# thunk

thunk (if 3 < 5 then return 1 else return 2) ;;

# force

force (thunk (if 3 < 5 then return 1 else return 2)) ;;

# let binding is written like this (Paul uses "be" in place of "=")

let x = 3 + 5 in return (x * x) ;;

# sequencing

return (3 + 5) to x in  return (x * x) ;;

# The above would be written in Haskell's do notation as
#
# do x <- return (3 + 5)
#    return (x * x)
#

# free and forgetful types

fun x : int -> return x ;;
fun x : U F int -> force x ;;
fun x : U F U F int -> (force x to y in force y) ;;
fun x : U F U F U F int -> (force x to y in force y to z in force z) ;;
fun x : int -> return (thunk (return x)) ;; 
fun x : int -> return (thunk (return (thunk (return x)))) ;; 

# For convenience we have top-level definitions of values ("let x = e" instead
# of "let x = e in ..." and top-level execution of computations ("do x = e" 
# instead of "e to x in ..."): 

let a = 5 ;;

let b = 10 + a ;;

let c = thunk (return b) ;;

do d = force c ;;

do e = return (a + d) ;;

do f = (fun x : int -> return (x + 2)) 19 ;;