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.

EOPL - 2.2.2 - Exercise 2.10

Chapter 2 includes examples and exercises for parsing and unparsing textual representations (e.g. parse-expression on page 51). The parsing functions assume a Scheme reader, and just convert from a list representation to an abstract syntax-tree representation based on define-datatype. The unparsing functions do the converse, from the syntax-tree representation to a list representation. As we don't have a list reader in F#, I skipped the examples and exercises related to parsing and unparsing. I also skipped other exercises that I felt wouldn't add much.

So here is Exercise 2.10 about generating fresh identifiers for renaming of variables that might be captured. I first defined a type for lambda-calculus expressions.

type Exp = Identifier of string | Lambda of string * Exp
        | App of Exp * Exp

Then there's all-ids and a converted version of fresh-id:

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 Identifier sym in
   loop 0