Transcript Slides

Advanced Functional Programming
Advanced Functional
Programming
Tim Sheard
Oregon Graduate Institute of Science & Technology
Lecture: Staged computation
•Difference between Haskell and ML
•Intro to MetaML
•Using staging to control evaluation order
Lecture 17
Tim Sheard
1
Advanced Functional Programming
Differences in Types
type variables and type application
type variables and type application
'a Tree
Tree a
type constructors
type constructors
int, string, bool
Int, String, Bool
tuples
tuples
(int * string * int)
(Int, String, Bool)
Lecture 17
Tim Sheard
2
Advanced Functional Programming
Differences
comments
(* Data definitions *)
-- data definitions
Type constructors are post fix
datatype 'a Tree
= Tip of 'a
note use of "of"
| Fork of
('a Tree)*('a Tree)
data Tree a
= Tip a
| Fork
(Tree a) (Tree a)
constructor functions are always uncurried
(use tuples)
'a = type variable
constructors are not
capitalized
Lecture 17
Tim Sheard
3
Advanced Functional Programming
difference 2
(* function definitions *)
-- function definitions
note use of "fun"
fun fact n =
if n=0
then 1
else n * (fact (n-1));
fun depth (Tip a) = 0
| depth (Fork(x,y)) =
1 + max (depth x,
depth y);
use "bar" (|) to
separate clauses
Lecture 17
equality is double =
fact n =
if n==0
then 1
else n * (fact (n-1))
depth (Tip a) = 0
depth (Fork x y) =
1 + max (depth x)
(depth y)
primitives more likely to be
curried in Haskell
Tim Sheard
4
Advanced Functional Programming
Differences between Haskell & ML
Data List a = []
| (:) a (list a)
Datatype ‘a list =
[] | (op ::) of ‘a * (‘a list)
map f [] = []
map f (x:xs)=(f x):(map f xs)
fun map f [] = …
| map f (x::xs) =
pi = 3.14159
val pi = 3.14159
\ x -> x + 1
fn x => x + 1
Lecture 17
Tim Sheard
5
Advanced Functional Programming
Some Primitives
- op +;
val it = fn:int * int -> int
- op *;
val it = fn:int * int -> int
- op -;
val it = fn:int * int -> int
Main> :t (+)
(+) :: Num a => a -> a -> a
Main> :t (*)
(*) :: Num a => a -> a -> a
Main> :t (-)
(-) :: Num a => a -> a -> a
- op @;
val it =
fn:'a list *
- length;
val it = fn:'a
- op ::;
val it = fn:'a
- hd;
val it = fn:'a
- tl;
val it = fn:'a
Main> :t (++)
(++) :: [a] -> [a] -> [a]
'a list -> 'a list
list -> int
* 'a list -> 'a list
list -> 'a
list -> 'a list
Lecture 17
Main> :t length
length :: [a] -> Int
Main> :t (:)
(:) :: a -> [a] -> [a]
Main> :t head
head :: [a] -> a
Main> :t tail
tail :: [a] -> [a]
Tim Sheard
6
Advanced Functional Programming
Differences 3
(* variable definition *)
use val to declare
variables
val tree1 =
Fork(Fork(Tip 1,Tip 2),
Tip 3);
Lecture 17
-- variable definition
tree1 =
Fork (Fork (Tip 1) (Tip 2))
(Tip 3)
Tim Sheard
7
Advanced Functional Programming
functions
fn x => x + 1
\ x -> x + 1
let fun f x = x + 1
in f 7 end
let f x = x + 1
in f 7
has type in ML is :
has type in Haskell is ::
datatype T = ...
data T = ...
datatype ('a,'b) T = ...
= (in MetaML only)
'a ('b T)
data T b a = ...
Lecture 17
Tim Sheard
8
Advanced Functional Programming
case expressions
case x of
[] => 5
| (x::xs) => len xs + m3
Lecture 17
case x of
[] -> 5
(x:xs) -> len xs + m3
Tim Sheard
9
Advanced Functional Programming
Differences 4
(* booleans *)
-- booleans
No capitals
- true;
val it = true : bool
- false;
val it = false : bool
Main> :t True
True :: Bool
Main> :t False
False :: Bool
(* mutual recursion *)
-- mutual recursion
fun
|
and
|
even
even
odd
odd
0
n
0
n
=
=
=
=
true
odd (n-1)
false
even (n-1);
use of "and" must separate
mutually recursive functions
Lecture 17
all functions are implicitly
mutually recursive
even
even
odd
odd
0
n
0
n
=
=
=
=
True
odd (n-1)
False
even (n-1)
Tim Sheard
10
Advanced Functional Programming
Intro to MetaML
Lecture 17
Tim Sheard
11
Advanced Functional Programming
Controlling Evaluation Order
We want more than just the correct result!
We want to control other resources such as
time and space without resorting to tricks
or unnatural programming styles.
Mechanism - Control Evaluation Order
Lecture 17
Tim Sheard
12
Advanced Functional Programming
Traditional Approaches
Fixed evaluation order with language extensions
Lazy - Outermost
add strictness annotations
Strict - Innermost
add annotations like force and delay
Encode laziness using lambda in a strict setting
datatype 'a lazylist =
lazyNil
| lazyCons of 'a * (unit -> 'a lazylist);
fun count n = lazyCons(n, fn () => count (n+1))
Lecture 17
Tim Sheard
13
Advanced Functional Programming
Limitations
None of these approaches allow
computation under a lambda! This is
sometimes just what is needed. For
example:
fun power n =
(fn x => if n=0
then 1
else x * (power (n-1) x))
power 2;
Lecture 17
Tim Sheard
14
Advanced Functional Programming
Example reduction
(power 2)
unfold the definition
(fn x => if 2=0 then 1 else x * (power (2-1) x))
perform the if, under the lambda
(fn x => x * (power (2-1) x))
unfold power again
(fn x => x * ((fn x => if 1=0
then 1
else x * (power (1-1) x))
x))
use the beta rule to apply the explicit lambda to x
Lecture 17
Tim Sheard
15
Advanced Functional Programming
Example (cont.)
(fn x => x * (if 1=0 then 1 else x * (power (1-1) x)))
perform the if
(fn x => x * (x * (power (1-1) x)))
unfold power again
(fn x => x * (x * ((fn x => if 0=0
then 1
else x * (power (0-1) x)))
x))
use the beta rule to apply the explicit lambda to x
(fn x => x * (x * (if 0=0 then 1
else x * (power (0-1) x))))
perform the if
(fn x => x * (x * 1))
Lecture 17
Tim Sheard
16
Advanced Functional Programming
Solution - Use richer annotations
Brackets: < e >
no reductions allowed in e
delay computation
if e:t then <e> : <t> (pronounced code of t)
Escape:
~ e
Run:
run e
relax the no reduction rule of brackets above
Escape may only occur inside Brackets
splice code together to build larger code
remove outermost brackets
force computations which have been delayed
Lecture 17
Tim Sheard
17
Advanced Functional Programming
Calculus
A calculus describes equivalences between
program fragments.
The rules of a calculus can be applied in any
order.
An implementation applies the rules in some
fixed order.
Traditional rules
beta – (fn x => e) v
 e[v/x]
if
– if true then x else y  x
– if false then x else y  y
delta – 5 + 2
7
Lecture 17
Tim Sheard
18
Advanced Functional Programming
Rules for code
Introduction rule for code
<e>
1st elimination rule for code
(escape-bracket elim)
< … ~<e> … > ---> < … e … >
~<e> must appear inside enclosing brackets
e must be escape free
<e> must be at level 0
2nd elimination rule for code
(run-bracket elim)
run <e> ---> e
provided e has no escapes
the whole expression is at level 0
Lecture 17
Tim Sheard
19
Advanced Functional Programming
Power example revisited
(* power : int -> <int> -> <int> *)
fun power n =
fn x => if n=0
then <1>
else < ~x * ~(power (n-1) x) >
(* ans : < int -> int > *)
val ans = < fn z => ~(power 2 <z>) >;
Lecture 17
Tim Sheard
20
Advanced Functional Programming
<fn z => ~ (power 2 <z>) >
<fn z => ~(if 2=0
then <1>
else < ~<z> * ~(power (2-1) <z>) >)>
<fn z => ~< ~<z> * ~(power (2-1) <z>) >>)
<fn z => ~< z * ~(power (2-1) <z>) >>)
<fn z =>
~< z * ~(if 1=0
then <1>
else < ~<z> * ~(power (1-1) <z>) >) >>)
Lecture 17
Tim Sheard
21
Advanced Functional Programming
<fn z => ~< z * ~< ~<z> * ~(power (1-1) <z>) >>>
<fn z => ~< z * ~< z * ~(power (1-1) <z>) >>>
<fn z => ~< z * ~< z * ~(power 0 <z>) >>>
<fn z => ~< z * ~< z * ~<1> >>>
<fn z => ~< z * ~< z * 1 >>>
<fn z => ~< z * z * 1 >>
<fn z => z * z * 1>
Lecture 17
Tim Sheard
22
Advanced Functional Programming
MetaML: Meta-programming
Meta-Programming: Programs that write
programs
What Infrastructure is possible in a language designed to
help support the algorithmic construction of other
programs?
Advantages of meta-programs
capture knowledge
efficient solutions
design ideas can be communicated and shared
Lecture 17
Tim Sheard
23
Advanced Functional Programming
Types of meta-programs
Static generators
Generate code which is then “written to disk” and processed by
normal compilers etc.
Two kinds
Homogeneous systems
object language = meta-language
Heterogeneous systems
object-language different from meta-language
Run-time generators
Staged Programs
Programs that generate other programs, and then execute the
programs they generated
MetaML is a staged programming language which does run-time
code generation
Lecture 17
Tim Sheard
24
Advanced Functional Programming
MetaML & the Mustang Project
Theory
Semantics of staged programs
What does it mean to have a staged program?
How can we tell if a staged program computes the
same result as its unstaged counterpart?
Calculus of programs - Rules for reasoning
Staged type systems
A static type system keeps bad programs from
executing by throwing away bad programs by
refusing to compile them.
A staged program admits more bad things.
E.g. using a variable before it is defined, or
executing a program before its complete, for
example.
Staged languages need richer type systems to throw
away these bad programs.
Automatic staging
partial evaluation
Lecture 17
Tim Sheard
25
Advanced Functional Programming
MetaML & the Mustang Project
Tools
Staged Languages
MetaML
reflective: obj-lang = meta-lang = ML
multi-stage
Heterogeneous (meta-lang=ML, obj-lang varies, 2
stage)
Lecture 17
Tim Sheard
26
Advanced Functional Programming
Building pieces of code
-| <23>;
val it = <23> : <int>
-| <length [1,2,3]>;
val it = <%length [1,2,3]> :<int>
-| <23 + 5>;
val it = <23 %+ 5> : <int>
-| <fn x => x + 5>;
val it = <(fn a => a %+ 5)> : <int -> int>
-| <fn x => <x + 1>>;
val it = <(fn a => <a %+ 1>)> : <int -> <int>>
Lecture 17
Tim Sheard
27
Advanced Functional Programming
Let’s try it !
Run MetaML
Lecture 17
Tim Sheard
28
Advanced Functional Programming
Composing pieces of code
-| val x = <2>;
val x = <2> : <int>
-| val y = <44 + ~x>;
val y = <44 %+ 2> : <int>
-| fun pair x = <( ~x, ~x )>;
val pair = Fn : ['b].<'b > -> <('b
* 'b )>
-| pair <11>;
val it = <(11,11)> : <(int * int)>
Lecture 17
Tim Sheard
29
Advanced Functional Programming
Executing constructed code
-| val x = <34 + 2>;
val x = <34 %+ 2> : ['a].<int>
-| run x;
val it = 36 : int
-| fun id x = x;
val id = Fn : ['a].'a
-> 'a
-| val q = <1 + ~(id <2+3>) >;
val q = <1 %+ 2 %+ 3> : <int>
-| run q;
val it = 6 : int
Lecture 17
Tim Sheard
30
Advanced Functional Programming
Multi-stage code
-| val z = <fn n => <n + 1>>;
val z = <(fn a => <a %+ 1>)> : <int -> <int>>
-| val f = run z;
val f = Fn : int -> <int>
-| f 12;
val it = <%n %+ 1> : <int>
-| run it;
val it = 13 : int
Lecture 17
Tim Sheard
31
Advanced Functional Programming
The lift operator
-| <4+1>;
val it = <4 %+ 1> : <int>
-| lift (4+1);
val it = <5> : <int>
-| val z = <fn n => < ~(lift n) + 1>>;
val z = <(fn a => <~(lift a) %+ 1>)> :<int ->
<int>>
-| run z;
val it = Fn
-| it 5;
val it =
: int -> <int>
<5 %+ 1>: <int>
-| run it;
val it = 6 : int
Lecture 17
Tim Sheard
32
Advanced Functional Programming
Lift v.s. lexical capture
Lift cannot be used on functions
-| lift id;
Error: The term: id
Non Qualified type, not liftable: ? -> ?
Lift makes code readable
-| fun f x = <(x, ~(lift x))>;
val f = Fn : ['b^].'b -> <('b * 'b )>
-| f 3;
val it = <(%x,3)> : <(int * int)>
Lexical capture is more efficient
-| lift [1+3,4,8-4];
val it = <4 :: (4 :: (4 :: [])))> : <int list >
Lecture 17
Tim Sheard
33