Book review: Expert F#

Expert F#, by Don Syme, Adam Granicz and Antonio Cisternino, Apress

When a new programming language arrives and manages to make an impact, books about it will certainly appear. However, most often the books will be geared to beginners, to people that is either not very experienced in programming or in the programming paradigms embodied by the language. For a experienced programmer, these books stop right when the fun would begin: the advanced stuff, the corners, the details are left out.

Expert F#, as suggested by its title, is not like this: it is aimed at more experienced programmers. The book will not teach you, for instance, what is functional programming or hammer to your head the best ways to use lists, an ubiquitous data structure in functional languages. But it explains how the things work in F#, so that programmers already familiar with other functional languages will have no trouble picking it up. F# also has object-oriented capabilities, which are explained in a chapter, without however going much deep into OO concepts; the book is about the language, not the paradigms.

And it does this well. Roughly half of the book is about the language itself, the other half are examples of applications and how to use some important libraries. As I was already familiar with OCaml and Haskell, I mostly skimmed through chapters 1 to 4, reading more closely from chapters 5 (generic types) and 6 (how objects fit into F#). From chapter 7 (encapsulating and packaging your code) on, the book starts to get really interesting; the next one is about common techniques, and chapter 9 is the best in the first part, explaining language-oriented programming, an area where functional languages really shine.

There are mandatory chapters about Windows Forms (11), Web programming (14) using .NET and data access, including how to use LINQ in F#, but I really liked chapters 12 (working with symbolic representations), and 13 (concurrency and asynchronous workflows). The former includes two cool examples: a symbolic differentiator and a verifier for logic circuits based on BDDs (Binary Decision Diagrams). There are other important and advanced chapters treating topics like interoperation with C and COM, debugging and testing F# programs, and F# library design.

All in all a very good book about the best current functional language to use in the Windows platform. I have two minor quibbles about it, though: the first few chapters about the language really could be made more interesting (although it didn't affect me much, as I only skimmed them) and some of the more exciting new features of F# could be explained in more detail. Specifically, workflows and active patterns. They are quite recent additions to the language, however, and there is some additional material promised to feature in the book's site.

Anyway, I will keep this book nearby when programming in F#. It is this kind of book that you'd want to keep around, even after learning the language.

Do it yourself: Visual F# Express 2008

As noted in this post, if you want Visual Studio just to have an IDE to work with F#, you can get it for free. Now with Visual Studio 2008, Microsoft has released a bare-bones VS, without any language, that can be used with language extensions and plugins, as is the case of F#. This bare-bones VS is called Visual Studio 2008 Shell (integrated mode).

After downloading and installing VS 2008 Shell (it takes a lot of unpacking and installing), you can install F# 1.9.3.7 and voilà, you have a pretty good F# IDE in your box, without having to shell out any cash.

I tested it with F# version 1.9.3.7 in a machine running Windows XP SP2 and no previous version of Visual Studio installed, and it worked. I even compiled and ran some test projects. If it doesn't work at first, take a look at the original post.

Further news on World Domination

Don Syme blogs about taking F# forward, which means, it seems, that F# will leave the confines of MS Research and be fully integrated into Visual Studio, as a product. If this is right, it's a great step for F# as a language and for functional programming in general, as we'll have a first-class IDE, by a major vendor, shipping with a functional programming language.

F# is already a great language to use, so I look forward to it getting still greater. The next step for Microsoft is to embrace Visual Haskell and fully integrate Haskell in Visual Studio too :)

F# Performance

There's a comparison of F# versus IronPython in Robert Pickering's blog. The results show that F# has roughly the same level of conciseness and terseness of Python, while being close in performance to C#. This is a .NET-based comparison, but it would be interesting to compare F# with CPython to see where it stands. If we are to believe this discussion on the python-dev mailing list, it seems that IronPython's performance must be comparable to CPython's, so there we have it: .NET or not, F# strikes an interesting balance in the expressiveness versus performance trade-offs.

This is also my personal experience with OCaml: performance roughly comparable to C/C++, but expressive and concise like scripting languages. It is this interesting position in the expressiveness x performance curve that makes both F# and OCaml very worthwhile languages to learn and use today.

The EOPL in F# wiki

I've started moving the content for the "EOPL in F#" translation to a wiki. Unfortunately, I have also been insanely busy as of late, so there's only the beginning there. However, as I'll have more free time from now on, I intend to catch up with what's already here and then start posting more sections that I already translated. I also noticed I never posted some parts because I forgot to, so it will be added to the wiki as well. Anyway, here is the link:

EOPL in F# Wiki

The EOPL in F# thing

I have translated more of the EOPL book into F#, but the examples keep growing and proving how unfit the whole enterprise is to the blog format. I knew this from the beginning, and would prefer a wiki, but then I couldn't find a decent wiki server. I may have found one now, and if all goes well I'll link to it here after moving there some of the contents posted here. After this, I don't know if this blog will still be useful, but I'll wait and see.

EOPL - 3.2 - Exercise 3.5

Exercise 3.5 asks you to add a print primitive to the language, which prints its argument and returns the value 1. The relevant changes are simple. In module Eopl_3 only the definition of type Primitive and function apply_primitive are different:

// in eopl_3.fs (module Eopl_3)
type Primitive = AddPrim | SubtractPrim | MultPrim | IncrPrim 
               | DecrPrim | PrintPrim

let apply_primitive prim args = 
    match (prim, args) with
      (AddPrim, [a; b]) -> a + b
    | (SubtractPrim, [a; b]) -> a - b
    | (MultPrim, [a; b]) -> a * b
    | (IncrPrim, [a]) -> a + 1
    | (DecrPrim, [a]) -> a - 1
    | (PrintPrim, [a]) -> (print_endline (string_of_int a); 1)
    | _ -> failwith "Incorrect argument list for primitive" 

In the lexer specification a token for the print primitive is added:

rule token = parse
| whitespace { token lexbuf }
| '%' [^ '\n']* { token lexbuf } 
| newline       { record_newline lexbuf; token lexbuf }
| "+"         { PLUS }
| "-"         { MINUS }
| "*"  { MULT }
| "("           { LPAREN }
| ")"         { RPAREN }
| ","           { COMMA  }
| "add1" { INCR }
| "sub1" { DECR }
| "print"       { PRINT }
| id         { ID(lexeme lexbuf) }
| ['-']?digit+  { LIT (Int32.Parse(lexeme lexbuf)) }
| eof   { EOF }

And, in the parser, this token must be declared and dealt with:

%token PRINT INCR DECR LPAREN RPAREN PLUS MINUS MULT COMMA EOF

Prim: PLUS                        { AddPrim }
    | MINUS                       { SubtractPrim }
    | MULT                        { MultPrim }
    | INCR                        { IncrPrim }
    | DECR                        { DecrPrim }
    | PRINT                       { PrintPrim }

The remaining parts of these three files are the same as the previous two posts.

EOPL - 3.2 - Front-end for the first interpreter

The previous post showed the code for the interpreter, working on an abstract syntax representation of the interpreted programs. In section 3.2 a front-end is presented to permit working with a concrete syntax. The book uses SLLGEN, a tool developed by the PLT Scheme group, to generate lexers and parsers. I used fslex and fsyacc, the standard tools of F# for such purposes. Here's the lexical specification.

{
// eopl1_lex.fsl
//
// Lexical specification for the first interpreter 
// in EOPL (Essentials of Programming Languages)

open System
open Eopl1_par
open Lexing

let record_newline (lexbuf : lexbuf) = 
    lexbuf.EndPos <- lexbuf.EndPos.AsNewLinePos()

}

// These are some regular expression definitions
let digit = ['0'-'9']
let id = ['a'-'z'] ['a'-'z' '0'-'9']*
let whitespace = [' ' '\t' ]
let newline = ('\n' | '\r' '\n')

rule token = parse
| whitespace { token lexbuf }
| '%' [^ '\n']* { token lexbuf } 
| newline       { record_newline lexbuf; token lexbuf }
| "+"         { PLUS }
| "-"         { MINUS }
| "*"  { MULT }
| "("           { LPAREN }
| ")"         { RPAREN }
| ","           { COMMA  }
| "add1" { INCR }
| "sub1" { DECR }
| id         { ID(lexeme lexbuf) }
| ['-']?digit+  { LIT (Int32.Parse(lexeme lexbuf)) }
| eof   { EOF }

And the grammar to use with fsyacc.

// eopl1_par.fsy 
// Parser for the first interpreter 
// in EOPL (Essentials of Programming Languages)

%{

open Eopl_3

%}

%start start

// terminal symbols
%token  ID
%token  LIT
%token INCR DECR LPAREN RPAREN PLUS MINUS MULT COMMA EOF

%type < Eopl_3.Program > start

%%

start: Prog {  $1 }

Prog: Expr                        { Exp ($1)   }

Expr: ID                          { VarExp($1) }
    | LIT                         { LitExp($1) }
    | Prim LPAREN ArgList RPAREN  { PrimAppExp ($1, List.rev $3) }

Prim: PLUS                        { AddPrim }
    | MINUS                       { SubtractPrim }
    | MULT                        { MultPrim }
    | INCR                        { IncrPrim }
    | DECR                        { DecrPrim }
    
ArgList: Expr                     { [$1] }
       | ArgList COMMA Expr       { $3 :: $1 }

Module Eopl_3 contains all the code from the previous post, including a definition of the abstract syntax. Both specifications above were adapted from an example included in the distribution. Now we only need to run these specifications into fslex and fsyacc, and write a driver for the interpreter, a simple read-eval-print loop. Here it is.

// eopl1_main.fs
//
// Driver for the first interpreter in EOPL
// (Essentials of Programming Languages)

#light 

open Eopl_3
open Eopl1_par

open Lexing

let parse str = 
    let lexbuf = Lexing.from_string str
    let prog = 
        try
            Some (Eopl1_par.start Eopl1_lex.token lexbuf)
        with e -> 
            let pos = lexbuf.EndPos
            printf "error near line %d, character %d\n%s\n" 
                   pos.pos_cnum 
                   (pos.pos_cnum - pos.pos_bol) (e.ToString());
            None
    prog
            
let rec read_eval_print prompt = 
    let _ = print_string prompt 
    let line = read_line ()
    match line with
      "#quit" -> ()
    | _ -> match parse line with
             None -> read_eval_print prompt
           | Some p -> let v = Eopl_3.eval_program p in 
                       (print_endline (string_of_int v); 
                        read_eval_print prompt)
           
let main() = 
    read_eval_print "--> " 
    
do main()

EOPL - Section 3.1

This is the first interpreter from Chapter 3, shown in Section 3.1. It needs an implementation of environments, I chose the simplest one and attached it before the code for the interpreter.

// implementation of environments 
// (represented as lists of pairs; the first in pair is 
//  a list of symbols, the second is a list of associated values)
let list_find_position a lst = 
    let rec loop l = 
        match l with
          [] -> None
        | (x :: l') when x = a -> Some (List.length l')
        | (x :: l') -> loop l' in
    loop (List.rev lst)

let empty_env () = 
    []
    
let extend_env syms vals env =
    (syms, vals) :: env
    
let rec apply_env env sym = 
    match env with
      [] -> failwith (sprintf "No binding for %s" sym)
    | (syms, vals) :: env' -> 
        match list_find_position sym syms with 
          None -> apply_env env' sym
        | Some i -> List.nth vals i
        
// types for primitives, expressions and programs
type Primitive = AddPrim | SubtractPrim | MultPrim | IncrPrim | DecrPrim
type Expression = LitExp of int | VarExp of string 
                | PrimAppExp of (Primitive * Expression list)
type Program = Exp of Expression

let apply_primitive prim args = 
    match (prim, args) with
      (AddPrim, [a; b]) -> a + b
    | (SubtractPrim, [a; b]) -> a - b
    | (MultPrim, [a; b]) -> a * b
    | (IncrPrim, [a]) -> a + 1
    | (DecrPrim, [a]) -> a - 1
    | _ -> failwith "Incorrect argument list for primitive" 

let init_env () = 
    extend_env ["i"; "v"; "x"] [1; 5; 10] (empty_env ())
    
let rec eval_expression exp env = 
    match exp with
      LitExp datum -> datum
    | VarExp id -> apply_env env id
    | PrimAppExp (prim, rands) -> let args = eval_rands rands env in 
                                  apply_primitive prim args
and eval_rands rands env = 
    List.map (eval_rand env) rands
and eval_rand env rand = 
    eval_expression rand env

let eval_program pgm = 
    match pgm with
      Exp body -> eval_expression body (init_env()) 

EOPL - 2.3.4 - Exercise 2.25

Using the data type definitions from the previous exercise, it's easy to define the necessary additional operations and then complete the definition of the unification function.

let is_var_term t =
    match t with Id _ -> true | _ -> false
        
let unit_subst i t =
    extend_subst i t (empty_subst ())
    
let rec compose_substs s1 s2 =
    match s1 with
      EmptySub -> s2
    | ExtendedSub (i, t, s) -> ExtendedSub (i, t, compose_substs s s2)

let rec unify_term t u = 
    match t with
      Id tid -> if (is_var_term u) || 
                    (not (List.mem tid (term_all_ids u))) then
                    Some (unit_subst tid u)
                else
                    None
    | _ -> match u with
             Id _ -> unify_term u t
           | Constant udat -> 
              (match t with 
                 Constant tdat when tdat = udat -> Some (empty_subst ())
               | _ -> None)
           | App us -> (match t with
                          App ts -> unify_terms ts us 
                        | _ -> None)
and unify_terms ts us = 
    match ts, us with
      [], [] -> Some (empty_subst ())
    | ([], _) -> None
    | (_, []) -> None
    | (t :: ts', u :: us') -> 
        let subst_car = unify_term t u in
        match subst_car with
          None -> None
        | Some s -> let new_ts = subst_in_terms ts' s in
                    let new_us = subst_in_terms us' s in
                    let subst_cdr = unify_terms new_ts new_us in
                    match subst_cdr with
                      None -> None
                    | Some s' -> Some (compose_substs s s')

The occurs check is necessary, of course, to avoid infinity. I won't say more than that, to force people that arrive here looking for solutions to EOPL's exercises to think a little about it, at least.

And this concludes Chapter 2.

EOPL - 2.3.4 - Exercise 2.24

This exercise asks for an implementation of substitutions on terms, the terms being defined by a previous exercise (2.13). In F#, they are thus defined:

type Value = Integer of int | String of string
type Term = Id of string | Constant of Value | App of Term list

let rec term_all_ids t = 
    match t with
      Id s -> [s]
    | Constant _ -> []
    | App tl -> List.concat (List.map term_all_ids tl)

Function term_all_ids gets all identifiers from a term, also part of exercise 2.13. Then for the part specific to exercise 2.24, which are substitutions. I chose to use an abstract syntax tree representation, because it is more convenient in F#. Using the definition, it was easy to write the operations on substitutions.

type Subst = EmptySub | ExtendedSub of string * Term * Subst

let empty_subst () = 
    EmptySub
    
let extend_subst i t s = 
    ExtendedSub (i, t, s)
    
let rec apply_subst s i = 
    match s with
      EmptySub -> Id i
    | ExtendedSub (i', t, s') when i = i' -> t
    | ExtendedSub (_, _, s') -> apply_subst s' i

With the substitution data type completed, we can write a substitution function without any difficulties.

let rec subst_in_term s t = 
    match t with 
      Id i -> apply_subst s i
    | Constant _ -> t
    | App tl -> App (List.map (subst_in_term s) tl)

let subst_in_terms lt s = 
    List.map (subst_in_term s) lt

I guess subst_in_terms might have been intended as a little more difficult to write. I don't know. In any case, it's just a map.

EOPL - 2.3.4 - Alternative Representation

A simple representation of environments as a list of pairs (syms, vals) where syms is a list of symbols and vals is a list of values positionally associated with the symbols.

let list_find_position a lst = 
    let rec loop l = 
        match l with
          [] -> None
        | (x :: l') when x = a -> Some (List.length l')
        | (x :: l') -> loop l' in
    loop (List.rev lst)

let empty_env () = 
    []
    
let extend_env syms vals env =
    (syms, vals) :: env
    
let rec apply_env env sym = 
    match env with
      [] -> failwith (sprintf "No binding for %s" sym)
    | (syms, vals) :: env' -> 
        match list_find_position sym syms with 
          None -> apply_env env' sym
        | Some i -> List.nth vals i

EOPL - 2.3.3 - Exercise 2.20

It's simple to add new operations when the data is represented as an abstract syntax tree. Here's the operation has_association for stacks as defined in the previous exercise:

// Exercise 2.20
let rec has_association env sym = 
    match env with
      EmptyEnv -> false
    | ExtendedEnv (syms, vals, env') -> (List.mem sym syms) || 
                                        (has_association env' sym)

EOPL - 2.3.3 - Exercise 2.19

Another simple exercise.

// Exercise 2.19
type 'a Stack = EmptyStack | ExtendedStack of 'a * 'a Stack

let empty_stack () = 
    EmptyStack
    
let push elt stk = 
    ExtendedStack (elt, stk)
    
let pop stk = 
    match stk with
      EmptyStack -> failwith "Stack empty"
    | ExtendedStack (_, s) -> s
    
let top stk = 
    match stk with
      EmptyStack -> failwith "Stack empty"
    | ExtendedStack (e, _) -> e
    
let is_stack_empty stk = 
    stk = EmptyStack

EOPL - Section 2.3.3

The abstract syntax tree representation for environments is quite straightforward in F#; it is shown below.

type Value = Integer of int | String of string
type Environment = EmptyEnv 
                 | ExtendedEnv of string list * 
                                  Value list * 
                                  Environment

// helper function
let list_find_position a lst = 
    let rec loop l = 
        match l with
          [] -> None
        | (x :: l') when x = a -> Some (List.length l')
        | (x :: l') -> loop l' in
    loop (List.rev lst)

let empty_env () = 
    EmptyEnv
    
let extend_env syms vals env = 
    ExtendedEnv (syms, vals, env)
    
let rec apply_env env sym = 
    match env with
      EmptyEnv -> failwith (sprintf "No binding for %s" sym)
    | ExtendedEnv (syms, vals, env') -> 
        match list_find_position sym syms with
          None -> apply_env env' sym
        | Some i -> List.nth vals i

EOPL - 2.3.2 - Exercise 2.16

Easy one, in two versions.

Version 1

let rec list_find_last_position sym los = 
    match los with
      [] -> None
    | (s :: los') when s = sym -> 
        (match list_find_last_position sym los' with
             None -> Some 0
         |   Some i -> Some (i + 1))
    | (s :: los') -> 
        (match list_find_last_position sym los' with
             None -> None
         |   Some i -> Some (i + 1))

Version 2

let rec list_find_last_position sym los = 
    match los with
      [] -> None
    | (s :: los') -> 
        match list_find_last_position sym los' with
          None -> if s = sym then Some 0 else None
        | Some i -> Some (i + 1)

Version 2 was obtained by observing similarities in Version 1. The idea appeared in previous examples: pattern guards do not always lead to shorter code.

EOPL - 2.3.2 - Exercise 2.15

I solved this exercise in quite a "lispy" way, so it's a bit alien in F#. It works, but in a quite awkward way. The idea was to maintain the stack as a pair containing the current top element and the old stack, and this means that, in F#, each operation that adds or removes elements produces a stack with a different type than the original. An interesting consequence of this is that the stack size is reflected in its type, so that we could define functions that work on "stacks of size 3" or so on. Who needs dependent types? :)

So here's the code. It first defines a type synonym to ease working with stacks, and then the functions that implement basic operations.

type 'a stack = (unit -> 'a) * (unit -> bool)

let empty_stack () = 
    let top () = failwith "The stack is empty, no top element" in
    let is_empty_stack () = true in
    (top, is_empty_stack)

let push elt stk = 
    let top () = (elt, stk) in
    let is_empty_stack () = false in
    (top, is_empty_stack)
    
let pop stk = 
    let oldstk : 'a stack = snd ((fst stk) ()) in
    let top = fst oldstk in
    let is_empty_stack = snd oldstk in
    (top, is_empty_stack)
    
let is_empty_stack stk = 
    let empty = snd stk in empty ()
    
let top stk = 
    let t = fst stk in fst (t ())

And it is used like this: you must assign a type for the empty_stack call, otherwise you are nagged by the value restriction again. That's where the type synonym comes in handy:

> let (x : int stack) = (empty_stack());;

val x : int stack

Then you can push elements into x. Note how the type of the result is different from int stack, even considering type synonyms.

> push 3 x;;
val it : (unit -> int * int stack) * (unit -> bool)
       = (<fun:push@173>, <fun:push@174>)
> push 4 (push 3 x);;
val it : (unit -> int * 
            ((unit -> int * int stack) * (unit -> bool))) * 
         (unit -> bool) 
       = (<fun:push@173>, <fun:push@174>)
> 

If you pop elements, the types get back to what they were, obviously. A funny side-effect of this strange definition is that top and pop don't work on empty stacks because of type-checking, not any run-time checking -- so that the failwith in the definition of empty_stack will never be executed. Empty stacks have actually a different type.

There must be a more type-friendly implementation of stacks using a procedural representation, but I decided to leave it for now and publish this solution because it is quite interesting by itself (although almost unusable in real code).

EOPL - 2.3.2 - Procedural Representation

Section 2.3 is about strategies for representing data types. In section 2.3.1 an abstract interface for environments is presented, and then in section 2.3.2, Figure 2.3 shows a procedural implementation for the environment interface. Translated into F#, Figure 2.3 would be like the following:

let find_index a lst = 
    let rec loop l = 
        match l with
          [] -> raise Not_found
        | (x :: l') when x = a -> List.length l'
        | (x :: l') -> loop l' in
    loop (List.rev lst)
        
let list_find_position sym los = 
    if List.mem sym los then
        Some (find_index sym los)
    else
        None
        
let empty_env () = 
    fun sym -> failwith (sprintf "No binding for %s" sym)

let apply_env env sym = 
    env sym
    
let extend_env syms vals env = 
    fun sym -> match list_find_position sym syms with
                 None -> apply_env env sym
               | Some i -> List.nth vals i

In this case, function find_list_position is redundant, because find_index does not take a predicate, so it's less generic than the version in the book. It shouldn't be a problem at this point, though. Function find_index reverses the list, we can write a version that does without that:

let rec find_index2 a lst = 
    match lst with 
      [] -> raise Not_found
    | (x :: lst') when x = a -> 0
    | (x :: lst') -> 1 + find_index2 a lst'

EOPL - 2.2.2 - Exercise 2.12

This one asks you to implement alpha, beta and eta conversion on lambda-calculus expressions based on the substitution function of the previous exercise. For this we need a function to see if an identifier occurs free in an expression, similar to the one presented on section 1.3 and easy enough. The conversion functions can then be implemented quite simply:

let rec occurs_free v exp =
   match exp with
     Identifier i when v = i -> true
   | Lambda (x, e) when v <> x -> occurs_free v e
   | App (e1, e2) -> (occurs_free v e1) || (occurs_free v e2)
   | Prim (p, e1, e2) -> (occurs_free v e1) || (occurs_free v e2)
   | _ -> false

let alpha_conversion exp new_id =
   match exp with
     Lambda (id, body) when not (occurs_free new_id body) ->
         Lambda (new_id, lambda_calculus_subst body (Identifier new_id) id)
   | _ -> exp
  
let beta_conversion exp =
   match exp with
     App (Lambda (id, body), e) -> lambda_calculus_subst body e id
   | _ -> exp
  
let eta_conversion exp =
   match exp with
     Lambda (id, App (e, Identifier id'))
     when (id=id') && (not (occurs_free id e)) -> e
   | _ -> exp

These conversion functions simply return the same expression if they aren't of the right form. They could signal an error, depending on the application.

EOPL - 2.2.2 - Exercise 2.11

Exercise 2.11 asks you to correct the definition of a substitution function on the lambda-calculus, to avoid variable capture. To do that, we need function fresh-id from the previous exercise, but alas, we can't use it as is, because it is also asked to extend the definition of a lambda-calculus expression to includes literals and primitives. Nevertheless, it's an easy exercise.

To define the new lambda-calculus expression type, we first define a type to specify primitives:

type Primitive = Sum | Mult

type LPExp = Identifier of string | Lambda of string * LPExp
          | App of LPExp * LPExp | Literal of int
          | Prim of Primitive * LPExp * LPExp

And here is the code for auxiliary functions and the substitution function:

let rec all_ids exp =
   match exp with
     Identifier i -> [i]
   | Lambda (x, e) -> x :: (all_ids e)
   | App (e1, e2) -> (all_ids e1) @ (all_ids e2)
   | _ -> []
  
let fresh_id exp s =
   let syms = all_ids' exp in
   let rec loop n =
       let sym = s + (string_of_int n) in
       if List.mem sym syms then loop (n + 1) else sym in
   loop 0
         
let rec lambda_calculus_subst exp subst_exp subst_id =
   let rec subst exp =
       match exp with
         Identifier id when id = subst_id -> subst_exp
       | Identifier id -> exp
       | Lambda (id, body) when id = subst_id -> exp
       | Lambda (id, body) ->
           let id'=fresh_id body id in
           let body'=lambda_calculus_subst body (Identifier id') id in
           Lambda (id', subst body')
       | App (e1, e2) -> App (subst e1, subst e2)
       | Literal l -> exp
       | Prim (p, e1, e2) -> Prim (p, subst e1, subst e2) in
   subst exp

The substitution function always does an alpha conversion (substitution of the identifier bound by the lambda) unless the bound identifier is the same as the one being substituted for. This surely works, as alpha conversion doesn't change the meaning of a lambda expression. An alternative would be to alpha convert only when a capture would occur, but this would require a further check like

if List.mem id (all_ids body) then
 // do alpha conversion
else
 // just simple substitution

It would make the code bigger, but not better. Both versions require linear scans of the body, so the efficiency shouldn't differ much between them.