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