Diagrammatic
execution models forfunctional programming
Koko Muroya(RIMS, Kyoto University& University of Birmingham)

Steven W. T. Cheung
Dan R. Ghica(University of Birmingham)

Lambda World CadizMuroya
2018 (RIMS,(Cadiz),25 October
2018
Kyoto
U. & U. B’ham.)What happens when you run a functional
program by hand?

2

Muroya (RIMS, Kyoto U. & U. B’ham.)

Running a functional program by hand(* computing the identity function in OCaml *)(fun _ -> fun x -> fun x) ((fun y -> y) (fun z -> z))-- computing the identity function in Haskell(\_ -> \x -> x) ((\y -> y) (\z -> z))(λw. λx. x) ((λy. y) (λz. z))

3

Muroya (RIMS, Kyoto U. & U. B’ham.)

Running a functional program by hand(* computing the identity function in OCaml *)(fun _ -> fun x -> fun x) ((fun y -> y) (fun z -> z))(*(fun _ -> fun x -> x) ((fun y -> y) (fun z -> z)) *)(* => (fun _ -> fun x -> x) (fun z -> z)*)(* => fun x -> x*)call-by-value
evaluation

4

Muroya (RIMS, Kyoto U. & U. B’ham.)

Running a functional program by hand-- computing the identity functionin Haskell(\_ -> \x -> x) ((\y -> y) (\z -> z))-(\_ -> \x -> x) ((\y -> y) (\z -> z))-- => \x -> xcall-by-need(lazy)
evaluation

5

Muroya (RIMS, Kyoto U. & U. B’ham.)

Running a functional program by handcall-by-value
evaluation(* computing the identity function in OCaml *)(fun _ -> fun x -> fun x) ((fun y -> y) (fun z -> z))(*(fun _ -> fun x -> x) ((fun y -> y) (fun z -> z)) *)(* => (fun _ -> fun x -> x) (fun z -> z)*)(* => fun x -> x*)call-by-need(lazy)
evaluation-- computing the identity functionin Haskell(\_ -> \x -> x) ((\y -> y) (\z -> z))-(\_ -> \x -> x) ((\y -> y) (\z -> z))-- => \x -> xSame result,but different steps!
6

Muroya (RIMS, Kyoto U. & U. B’ham.)

Let’s run a functional program with a bitof formality...

7

Muroya (RIMS, Kyoto U. & U. B’ham.)

Running a functional program, formallyby change of configuration● program● “focus”(* computing the identity function in OCaml *)(fun _ -> fun x -> fun x) ((fun y -> y) (fun z -> z))call-by-value
evaluation8

Muroya (RIMS, Kyoto U. & U. B’ham.)

Running a functional program, formallyby change of configuration● program● “focus”(* computing the identity function in OCaml *)(fun _ -> fun x -> fun x) ((fun y -> y) (fun z -> z))call-by-value
evaluation

9

Muroya (RIMS, Kyoto U. & U. B’ham.)

Running a functional program, formallyby change of configuration● program● “focus”(* computing the identity function in OCaml *)(fun _ -> fun x -> fun x) ((fun y -> y) (fun z -> z))call-by-value
evaluation10

Muroya (RIMS, Kyoto U. & U. B’ham.)

Running a functional program, formallyby change of configuration● program● “focus”(* computing the identity function in OCaml *)(fun _ -> fun x -> fun x) (fun z -> z)call-by-value
evaluation

11

Muroya (RIMS, Kyoto U. & U. B’ham.)

Running a functional program, formallyby change of configuration● program● “focus”(* computing the identity function in OCaml *)(fun _ -> fun x -> fun x) (fun z -> z)call-by-value
evaluation

12

Muroya (RIMS, Kyoto U. & U. B’ham.)

Running a functional program, formallyby change of configuration● program● “focus”(* computing the identity function in OCaml *)fun x -> fun x

call-by-value
evaluation

13

Muroya (RIMS, Kyoto U. & U. B’ham.)

Running a functional program, formallyby change of configuration● program● “focus”-- computing the identity functionin Haskell(\_ -> \x -> x) ((\y -> y) (\z -> z))call-by-need(lazy)
evaluation
14

Muroya (RIMS, Kyoto U. & U. B’ham.)

Running a functional program, formallyby change of configuration● program● “focus”-- computing the identity functionin Haskell(\_ -> \x -> x) ((\y -> y) (\z -> z))call-by-need(lazy)
evaluation15

Muroya (RIMS, Kyoto U. & U. B’ham.)

Running a functional program, formallyby change of configuration● program● “focus”-- computing the identity functionin Haskell\x -> xcall-by-need(lazy)
evaluation
16

Muroya (RIMS, Kyoto U. & U. B’ham.)

Running a functional program, formally● program● “focus” determining
evaluation strategy

by change of configuration(* computing the identity function in OCaml *)(fun _ -> fun x -> fun x) ((fun y -> y) (fun z -> z))(*(fun _ -> fun x -> x) ((fun y -> y) (fun z -> z)) *)(* => (fun _ -> fun x -> x) ((fun y -> y) (fun z -> z)) *)(* => (fun _ -> fun x -> x) (fun z -> z)*)(* => (fun _ -> fun x -> x) (fun z -> z)*)(* => fun x -> x*)-- computing the identity function in Haskell(\_ -> \x -> x) ((\y -> y) (\z -> z))-(\_ -> \x -> x) ((\y -> y) (\z -> z))-- => \x -> x
17

Muroya (RIMS, Kyoto U. & U. B’ham.)Goodness of formality
prove program equivalence (validate compiler optimisations)● “When are two programs the same?”● result modelled by observable transitions & final
configuration18

Muroya (RIMS, Kyoto U. & U. B’ham.)Goodness of formality
prove program equivalence (validate compiler optimisations)● “When are two programs the same?”● result modelled by observable transitions & final
configuration
analyse execution cost
● “How much time/space does it take to run a program?”● time cost modelled by number and cost of transitions● space cost modelled by size of configurations

19

Muroya (RIMS, Kyoto U. & U. B’ham.)Goodness of formality
prove program equivalence (validate compiler optimisations)● “When are two programs the same?”● result modelled by observable transitions & final
configuration
analyse execution cost
● “How much time/space does it take to run a program?”● time cost modelled by number and cost of transitions● space cost modelled by size of configurations
guarantee “correctness” of implementation● “Does a compiler work as intended?”● implementation derived as abstract machine
20

Muroya (RIMS, Kyoto U. & U. B’ham.)Now we use diagrams to run afunctional program with formality!

21

Muroya (RIMS, Kyoto U. & U. B’ham.)Conventional approaches● program● “focus” determining
evaluation strategy

running a program bychange of configuration

Diagrammatic approachrunning a program bychange of diagram configuration● diagram representation of program● “token” determining evaluation
strategy
22

Muroya (RIMS, Kyoto U. & U. B’ham.)

Running a functional program with diagramsby change of diagram configuration● diagram representationof program● “token” determining
evaluation strategy

name-free23

Muroya (RIMS, Kyoto U. & U. B’ham.)

Running a functional program with diagramsby change of diagram configuration● diagram representationof program● “token” determining
evaluation strategy

name-free[DEMO]
On-line visualiser for lambda-calculus
https://koko-m.github.io/GoI-Visualiser/● call-by-name, call-by-need (lazy)● call-by-value: left-to-right, right-to-left
24

Muroya (RIMS, Kyoto U. & U. B’ham.)● name-free● environment
included

Goodness of diagrams

25

Muroya (RIMS, Kyoto U. & U. B’ham.)Goodness of diagrams
visualise interesting properties of programs● name-free● environment
included● call-by-value vs. call-by-need (lazy)● on-demand copying with intermediate sharing● patterns in divergence○ (λx. x x) (λx. x x)
○ (λx. x x x) (λx. x x x)

26

Muroya (RIMS, Kyoto U. & U. B’ham.)Goodness of diagrams
visualise interesting properties of programs● name-free● environment
included● call-by-value vs. call-by-need (lazy)● on-demand copying with intermediate sharing● patterns in divergence○ (λx. x x) (λx. x x)
○ (λx. x x x) (λx. x x x)
answer (conventional) questions from new perspectives● “When are two programs the same?”● “How much time/space does it take to run a program?”● “Does a compiler work as intended?”27

Muroya (RIMS, Kyoto U. & U. B’ham.)More goodness of diagrams

28

Muroya (RIMS, Kyoto U. & U. B’ham.)More goodness of diagrams
support textual-and-visual programming

guide language design for unconventional/new programming
paradigms (to be presented by Steven)29

Muroya (RIMS, Kyoto U. & U. B’ham.)Towards textual-and-visual programming“We’d like not just text or diagram,but both!”diagrammaticalprogramtextual program(λw. λx. x) ((λy. y) (λz. z))

30

Muroya (RIMS, Kyoto U. & U. B’ham.)Towards textual-and-visual programming“We’d like not just text or diagram,but both!”diagrammaticalprogramtextual program(λw. λx. x) ((λy. y) (λz. z))✔
(grammar)form / edit?
(validity criteria)✔

execute✔

✔

debug!

31

Muroya (RIMS, Kyoto U. & U. B’ham.)OCaml Visual Debugger
https://fyp.jackhughesweb.com/ by Jack Hughes
for a subset of OCaml●●●●arithmetic (int), comparison (bool)
conditional (if), recursion (let rec)lists, pairs
pattern-matchingfeatures●●●●interactive diagram viewgo forwards/backwards & pause/resume & jump steps
breakpoint on diagramstats
32

Muroya (RIMS, Kyoto U. & U. B’ham.)OCaml Visual Debugger
visualise interesting properties of programs● sorting algorithms comparison○ bubble-sort vs. insert-sort
https://www.youtube.com/watch?v=bZMSwo0zL
io&t=130s○ merge-sort vs. insert-sort
https://www.youtube.com/watch?v=U1NI-mWeNe0● tail-recursion vs. non tail-recursion
https://www.youtube.com/watch?v=R4yCV5Ts1gk&t=14s

33

Muroya (RIMS, Kyoto U. & U. B’ham.)More goodness of diagrams
support textual-and-visual programming● “We’d like not just text or diagram, but both!”● We’ve got OCaml Visual Debugger● … and want a text-and-diagram editor!
guide language design for unconventional/new programming
paradigms (to be presented by Steven)34

Muroya (RIMS, Kyoto U. & U. B’ham.)More goodness of diagrams
support textual-and-visual programming● “We’d like not just text or diagram, but both!”● We’ve got OCaml Visual Debugger● … and want a text-and-diagram editor!
guide language design for unconventional/newprogramming paradigms (to be presented by Steven)35

Muroya (RIMS, Kyoto U. & U. B’ham.)