Fork me on GitHub

Utils Code Snippet

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
module Util = struct                                                          
                                                                              
  type (α,β) result =                                                         
    | Ok  of α                                                                
    | Err of β                                                                
                                                                              
  let success : α  (α,β) result = λ x  Ok  x                                
  let failure : β  (α,β) result = λ x  Err x                                
                                                                              
  let fmap : (α  β)  (α,γ) result  (β,γ) result = λ f                     
    function                                                                  
    | Ok  x  Ok (f x)                                                        
    | Err e  Err   e                                                         
  let (<$>) : (α  β)  (α,γ) result  (β,γ) result = fmap                    
                                                                              
  let liftM : (α,γ) result  (α  (β,γ) result)  (β,γ) result = λ m f       
    match m with                                                              
    | Ok  x  f x                                                             
    | Err e  Err e                                                           
  let (>>=) : (α,γ) result  (α  (β,γ) result)  (β,γ) result = liftM        
                                                                              
  let compose_left : (α  β)  (β  γ)  α  γ = λ f g x  g(f x)             
  let (>>) : (α  β)  (β  γ)  α  γ = compose_left                         
                                                                              
  let safe_find : (α  bool)  α list  α option = λ f xs                    
    let rec aux = function                                                    
      | [   ]  None                                                          
      | x::xs                                                                
         if f x then                                                          
           Some x                                                             
         else                                                                 
           aux xs                                                             
    in                                                                        
    aux xs                                                                    
                                                                              
  let string_to_chars : string  char list = λ x                             
    let rec aux acc = function                                                
      | 0                  acc                                               
      | i  aux (x.[i-1] :: acc) (i-1)                                        
    in aux [] (String.length x)                                               
                                                                              
end                                                                           

Utils Code output:

module Util :
  sig
    type ('a, 'b) result = Ok of 'a | Err of 'b
    val success : 'a -> ('a, 'b) result
    val failure : 'b -> ('a, 'b) result
    val fmap : ('a -> 'b) -> ('a, 'c) result -> ('b, 'c) result
    val ( <$> ) : ('a -> 'b) -> ('a, 'c) result -> ('b, 'c) result
    val liftM : ('a, 'c) result -> ('a -> ('b, 'c) result) -> ('b, 'c) result
    val ( >>= ) :
      ('a, 'c) result -> ('a -> ('b, 'c) result) -> ('b, 'c) result
    val compose_left : ('a -> 'b) -> ('b -> 'c) -> 'a -> 'c
    val ( >> ) : ('a -> 'b) -> ('b -> 'c) -> 'a -> 'c
    val safe_find : ('a -> bool) -> 'a list -> 'a option
    val string_to_chars : string -> char list
  end

Lambda Calculus Code Snippet

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
module LambdaCalculus = struct                                                
                                                                              
  open Printf                                                                 
  open Util   
                                                                              
  type error =                                                                
    | InvalidToken                                                            
    | NoClojureParse                                                          
    | InvalidParse                                                            
    | UnboundVariable                                                         
    | NoClojureEval                                                           
                                                                              
  type expr =                                                                 
    | Var of name                                                             
    | Lam of name * body                                                      
    | App of expr * expr                                                      
  and name  = char                                                            
  and body  = expr                                                            
                                                                              
  type token =                                                                
    | ParLeft                                                                 
    | ParRight                                                                
    | Lambda                                                                  
    | Dot                                                                     
    | Variable of char                                                        
                                                                              
  type env = (char * expr) list                                               
                                                                              
  let alphabet =                                                              
    [                                                                         
      'a';'b';'c';'d';'e';'f';'g';'h';'i';'j';'k';'l';'m';                    
      'n';'o';'p';'q';'r';'s';'t';'u';'v';'w';'x';'y';'z';                    
    ]                                                                         
                                                                               
  let rec tokenize : char list  (token list,error) result = function         
    | [       ]  [                                   ] |> success            
    | ' ' :: xs  tokenize xs                                                 
    | '(' :: xs  tokenize xs >>= λ ys  ParLeft  :: ys |> success            
    | ')' :: xs  tokenize xs >>= λ ys  ParRight :: ys |> success            
    | '^' :: xs  tokenize xs >>= λ ys  Lambda   :: ys |> success            
    | '.' :: xs  tokenize xs >>= λ ys  Dot      :: ys |> success            
    | var :: xs                                                              
       if   List.mem var alphabet                                             
       then tokenize xs >>= λ ys  Variable var   :: ys |> success            
       else InvalidToken                                |> failure            

  let rec parse_aux : token list  (expr * token list,error) result = function
    |           Variable var        :: xs  (Var var, xs) |> success          
    | Lambda :: Variable var :: Dot :: xs                                    
       parse_aux xs >>=                                                       
         λ (body,tokens)  (Lam (var,body), tokens)       |> success          
    | ParLeft                       :: xs                                    
       parse_aux xs >>=                                                       
         (λ (func,ys)                                                        
           parse_aux ys >>=                                                   
             (λ (value,zs)                                                   
               match zs with                                                  
               | ParRight :: tokens  (App (func,value), tokens) |> success   
               | __________________  NoClojureParse             |> failure   
             )                                                                
         )                                                                    
    | _________________________________  InvalidParse           |> failure   
  let parse : token list  (expr,error) result = λ xs                        
    fst <$> parse_aux xs                                                      
                                                                              
  let rec eval_aux : env  expr  (env * expr,error) result = λ env          
    function                                                                  
    | Var var                                                                
       let result =                                                           
         match safe_find (λ (v,t)  var = v) env with                         
         | Some (_,expr)  ([],expr)                 |> success               
         | None           UnboundVariable           |> failure               
       in result                                                              
    | Lam (var, body)                                                        
       (env, Lam (var, body))                        |> success               
    | App (func, value)                                                      
       eval_aux env func >>= function                                         
       | closed_env, Lam (var, body)                                         
          eval_aux env value >>= λ (_,eval_value)                            
          eval_aux ((var,eval_value) :: closed_env) body                      
       | ___________________________  NoClojureEval |> failure               
  let eval : expr  (expr,error) result = λ xs                               
    snd <$> eval_aux [] xs                                                    

  let rec pretty_printer : expr  (string,error) result = function            
    | Var var                                                                
       sprintf "%c"     var   |> success                                      
    | Lam (var,body)                                                         
       pretty_printer body >>= λ x                                           
       sprintf "^%c.%s" var x |> success                                      
    | App (func,value)                                                       
       pretty_printer func  >>= λ x                                          
       pretty_printer value >>= λ y                                          
       sprintf "(%s %s)" x y  |> success                                      
                                                                              
  let interpret : string  (string,error) result = λ x                       
    string_to_chars x |> success                                              
    >>= tokenize                                                              
    >>= parse                                                                 
    >>= eval                                                                  
    >>= pretty_printer                                                        
                                                                              
end                                                                           

Lambda Calculus Code output:

module LambdaCalculus :
  sig
    type error =
        InvalidToken
      | NoClojureParse
      | InvalidParse
      | UnboundVariable
      | NoClojureEval
    type expr = Var of name | Lam of name * body | App of expr * expr
    and name = char
    and body = expr
    type token = ParLeft | ParRight | Lambda | Dot | Variable of char
    type env = (char * expr) list
    val alphabet : char list
    val tokenize : char list -> (token list, error) Util.result
    val parse_aux : token list -> (body * token list, error) Util.result
    val parse : token list -> (expr, error) Util.result
    val eval_aux : env -> body -> (env * expr, error) Util.result
    val eval : expr -> (expr, error) Util.result
    val pretty_printer : body -> (string, error) Util.result
    val interpret : string -> (string, error) Util.result
  end

Assertions Code Snippet

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
module AssertLambdaCalculus = struct                                          
                                                                              
  open Util                                                                   
                                                                              
  let simple : bool =                                                         
    LambdaCalculus.interpret "^x.x" =                                         
      Ok "^x.x"                                                               
                                                                              
  let complex : bool =                                                        
    LambdaCalculus.interpret "((^x.^y.x ^a.(a a)) ^b.b)" =                    
      Ok "^a.(a a)"                                                           
                                                                              
  (* let omega : bool =                                                       
    LambdaCalculus.interpret "(^x.(x x) ^x.(x x))" =                          
      Ok "Infinte loop, never terminates" *)                                  
                                                                              
end

Assertions Code output:

module AssertLambdaCalculus : 
  sig 
    val simple  : bool 
    val complex : bool 
  end

AssertLambdaCalculus.simple;;
- : bool = true
AssertLambdaCalculus.complex;;
- : bool = true

References:

  • Michael Gilliland, Let’s Write a Lambda Calculus in F# video series:
comments powered by Disqus