CSC448: Type Checking Revisited: Simple Functional Language [116/133]

Consider a simple functional language:

M, N ::= n                    (n is a number)
       | s                    (s is a string)
       | x                    (x is a variable)
       | []                   (the empty list)
       | M :: N               (cons M onto the list N)
       | if M then N1 else N2
       | fun f x => M         (function that can call itself recursively using f inside M)
       | M N                  (application of a function to an argument)
       | let x = M in N       (bind the result of evaluating M to x inside N)
        

We might assume some builtin functions:

head : 'a list -> 'a
tail : 'a list -> 'a list
add : int -> (int -> int)
is_zero : int -> boolean
length : 'a list -> int
        

Aside: how would we translate the higher-order type int -> (int -> int) to a Java type?