1
0
mirror of https://github.com/dhil/phd-dissertation synced 2026-03-13 02:58:26 +00:00

Compare commits

...

2 Commits

Author SHA1 Message Date
2cecb13d34 Update all slides 2022-11-17 15:05:18 +00:00
ed634fcaa3 Update slides 2022-11-17 11:10:29 +00:00
4 changed files with 70 additions and 30 deletions

View File

@@ -56,12 +56,12 @@ fun has(k, kvs) {
#! #!
# #
# Effect Handler Oriented Programming # Effect Handler Oriented Programming
# A Gentle Introduction # Lets build an operating system
# Daniel Hillerström # Daniel Hillerström
# Laboratory for Foundations of Computer Science # Laboratory for Foundations of Computer Science
# The University of Edinburgh, Scotland, UK # The University of Edinburgh, Scotland, UK
# #
# EPL, The University of Edinburgh # Elements of Programming Languages
# November 17, 2022 # November 17, 2022
# #
# https://dhil.net/research/ # https://dhil.net/research/
@@ -118,7 +118,7 @@ fun has(k, kvs) {
# Plotkin and Pretnar (2009) invented effect handlers. # Plotkin and Pretnar (2009) invented effect handlers.
# Separates the syntax... # Separates the syntax...
sig syn : (Int) {Op:(Int) -> Int |e}~> b sig syn : (Int) {Op:(Int) -> Int |e}~> Int
fun syn(x) { do Op(x) } fun syn(x) { do Op(x) }
@@ -152,7 +152,7 @@ fun sem(m) {
#? #?
#} #}
#? #!
# #
# Characteristics of effect handlers # Characteristics of effect handlers
# #
@@ -161,7 +161,7 @@ fun sem(m) {
# * Increase the expressiveness of user-written code # * Increase the expressiveness of user-written code
# #
# #
#! #?
#! #!
# #
@@ -185,14 +185,14 @@ fun sem(m) {
#! #!
# #
# What is an effect handler? # Some ways to think about effect handlers
# #
# Operational interpretation <--- THIS LECTURE # Operational interpretation <--- THIS LECTURE
# Resumeable exceptions # Resumeable exceptions
# Programmable and composable operating systems # Programmable and composable operating systems
# #
# Software engineering interpretation # Software engineering interpretation
# Builders for monads (monads as a design pattern) # Composable monad builders (monads as a design pattern)
# #
# Functional programming interpretation # Functional programming interpretation
# Folds over computation trees # Folds over computation trees
@@ -375,7 +375,7 @@ sig stdout : FileDescr
var stdout = 1; var stdout = 1;
sig echo : (String) {Write:(FileDescr, String) -> ()}-> () sig echo : (String) {Write:(FileDescr, String) -> ()}-> ()
fun echo(cs) { todo("implement echo") } fun echo(cs) { do Write(stdout, cs) }
#? #?
#} #}
@@ -396,7 +396,12 @@ fun echo(cs) { do Write(stdout, cs) }
# #
sig basicIO : ( () {Write:(FileDescr, String) -> ()}-> a ) -> (a, File) sig basicIO : ( () {Write:(FileDescr, String) -> ()}-> a ) -> (a, File)
fun basicIO(m) { fun basicIO(m) {
todo("implement basicIO") handle(m()) {
case ans -> (ans, "")
case <Write(fd, cs) => (resume : (()) -> (a, File))> ->
var (ans, file) = resume(());
(ans, cs ++ file)
}
} }
#? #?
#} #}
@@ -433,7 +438,7 @@ fun example0() {
} }
# #!
# #
# Dynamic semantics of handlers # Dynamic semantics of handlers
# #
@@ -445,7 +450,7 @@ fun example0() {
# ,fun(x){ handle(E[x]) { case <Op(p) => r> -> N case ... }}/r] # ,fun(x){ handle(E[x]) { case <Op(p) => r> -> N case ... }}/r]
# (if Op \notin E) # (if Op \notin E)
# #
# #?
#{ #{
#! #!
@@ -453,7 +458,7 @@ fun example0() {
# Exceptions: Premature exits # Exceptions: Premature exits
# #
sig exit : (Int) {Exit:(Int) -> Zero}-> a sig exit : (Int) {Exit:(Int) -> Zero}-> a
fun exit(n) { todo("implement exit") } fun exit(n) { switch (do Exit(n)) { } }
#? #?
#} #}
@@ -493,7 +498,7 @@ sig example1 : () -> (Int, File)
fun example1() { fun example1() {
basicIO(fun() { basicIO(fun() {
status(fun() { status(fun() {
echo("dead"); exit(1); echo("code") echo("Hello"); exit(1); echo("World")
}) })
}) })
} }
@@ -504,7 +509,7 @@ sig example1 : () { |%}-> (Int, File)
fun example1() { fun example1() {
basicIO(fun() { basicIO(fun() {
status(fun() { status(fun() {
echo("dead"); exit(1); echo("code") echo("Hello"); exit(1); echo("World")
}) })
}) })
} }
@@ -518,7 +523,7 @@ sig example1' : () -> Int
fun example1'() { fun example1'() {
status(fun() { status(fun() {
basicIO(fun() { basicIO(fun() {
echo("dead"); exit(1); echo("code") echo("Hello"); exit(1); echo("World")
}) })
}) })
} }
@@ -617,7 +622,13 @@ fun su(user) { do Su(user) }
sig sessionmgr : (User, () {Ask:String, Su:(User) -> ()}-> a) -> a sig sessionmgr : (User, () {Ask:String, Su:(User) -> ()}-> a) -> a
fun sessionmgr(user, m) { fun sessionmgr(user, m) {
todo("implement sessionmgr") env(user, fun() {
handle(m()) {
case ans -> ans
case <Su(user') => resume> ->
env(user', fun() { resume(()) })
}
})
} }
#? #?
#} #}
@@ -710,7 +721,11 @@ fun fork() { do Fork }
sig nondet : (() {Fork:Bool}-> a) -> [a] sig nondet : (() {Fork:Bool}-> a) -> [a]
fun nondet(m) { fun nondet(m) {
todo("Implement nondet") handle(m()) {
case ans -> [ans]
case <Fork => resume> ->
resume(true) ++ resume(false)
}
} }
#? #?
#} #}
@@ -837,7 +852,11 @@ typename Pstate(a::Type, e::Eff)
sig reifyProcess : (() {Interrupt:() |e}-> a) -e-> Pstate(a, e) sig reifyProcess : (() {Interrupt:() |e}-> a) -e-> Pstate(a, e)
fun reifyProcess(m) { fun reifyProcess(m) {
todo("implement reifyProcess") handle(m()) {
case ans -> Done(ans)
case <Interrupt => resume> ->
Paused(fun() { resume(()) })
}
} }
#? #?
#} #}

View File

@@ -61,7 +61,7 @@ fun has(k, kvs) {
# Laboratory for Foundations of Computer Science # Laboratory for Foundations of Computer Science
# The University of Edinburgh, Scotland, UK # The University of Edinburgh, Scotland, UK
# #
# Huawei Research Centre Zurich, Switzerland # Huawei Research Centre Zürich, Switzerland
# October 13, 2022 # October 13, 2022
# #
# https://dhil.net/research/ # https://dhil.net/research/
@@ -260,7 +260,7 @@ sig stdout : FileDescr
var stdout = 1; var stdout = 1;
sig echo : (String) {Write:(FileDescr, String) -> ()}-> () sig echo : (String) {Write:(FileDescr, String) -> ()}-> ()
fun echo(cs) { todo("Implement echo") } fun echo(cs) { do Write(stdout, cs) }
#? #?
#} #}
@@ -281,7 +281,12 @@ fun echo(cs) { do Write(stdout, cs) }
# #
sig basicIO : ( () {Write:(FileDescr, String) -> ()}-> a ) -> (a, File) sig basicIO : ( () {Write:(FileDescr, String) -> ()}-> a ) -> (a, File)
fun basicIO(m) { fun basicIO(m) {
todo("Implement basicIO") handle(m()) {
case ans -> (ans, "")
case <Write(_, cs) => (resume : (()) -> (a, File) )> ->
var (ans, file) = resume(());
(ans, file ++ cs)
}
} }
#? #?
#} #}
@@ -338,7 +343,7 @@ fun example0() {
# Exceptions: Premature exits # Exceptions: Premature exits
# #
sig exit : (Int) {Exit:(Int) -> Zero}-> a sig exit : (Int) {Exit:(Int) -> Zero}-> a
fun exit(n) { todo("Implement exit") } fun exit(n) { switch (do Exit(n)) { } }
#? #?
#} #}
@@ -353,7 +358,10 @@ fun exit(n) { switch (do Exit(n)) { } }
# #
sig status : (() {Exit:(Int) -> Zero}-> a) -> Int sig status : (() {Exit:(Int) -> Zero}-> a) -> Int
fun status(m) { fun status(m) {
todo("Implement status") handle(m()) {
case ans -> 0
case <Exit(n)> -> n
}
} }
#? #?
#} #}

View File

@@ -139,7 +139,7 @@ fun has(k, kvs) {
# - Extremely compositional # - Extremely compositional
# #
# Some languages that support EHOP: # Some languages that support EHOP:
# C/C++, Eff, Haskell, Koka, Links, Pyro, OCaml, Unison # C/C++, Eff, Haskell, Koka, Links, Pyro, OCaml, Unison, Wasm
# #
#? #?
@@ -280,7 +280,7 @@ sig stdout : FileDescr
var stdout = 1; var stdout = 1;
sig echo : (String) {Write:(FileDescr, String) -> ()}-> () sig echo : (String) {Write:(FileDescr, String) -> ()}-> ()
fun echo(cs) { todo("implement echo") } fun echo(cs) { do Write(stdout, cs) }
#? #?
#} #}
@@ -301,7 +301,12 @@ fun echo(cs) { do Write(stdout, cs) }
# #
sig basicIO : ( () {Write:(FileDescr, String) -> ()}-> a ) -> (a, File) sig basicIO : ( () {Write:(FileDescr, String) -> ()}-> a ) -> (a, File)
fun basicIO(m) { fun basicIO(m) {
todo("implement basicIO") handle(m()) {
case ans -> (ans, "")
case <Write(_, cs) => ( resume : (()) -> (a, File) ) > ->
var (ans, file) = resume(());
(ans, cs ^^ file)
}
} }
#? #?
#} #}
@@ -373,7 +378,10 @@ fun exit(n) { switch (do Exit(n)) { } }
# #
sig status : (() {Exit:(Int) -> Zero}-> a) -> Int sig status : (() {Exit:(Int) -> Zero}-> a) -> Int
fun status(m) { fun status(m) {
todo("implement status") handle(m()) {
case ans -> 0
case <Exit(n)> -> n
}
} }
#? #?
#} #}

View File

@@ -260,7 +260,7 @@ sig stdout : FileDescr
var stdout = 1; var stdout = 1;
sig echo : (String) {Write:(FileDescr, String) -> ()}-> () sig echo : (String) {Write:(FileDescr, String) -> ()}-> ()
fun echo(cs) { todo("implement echo") } fun echo(cs) { do Write(stdout, cs) }
#? #?
#} #}
@@ -281,7 +281,12 @@ fun echo(cs) { do Write(stdout, cs) }
# #
sig basicIO : ( () {Write:(FileDescr, String) -> ()}-> a ) -> (a, File) sig basicIO : ( () {Write:(FileDescr, String) -> ()}-> a ) -> (a, File)
fun basicIO(m) { fun basicIO(m) {
todo("implement basicIO") handle( m() ) {
case ans -> (ans, "")
case <Write(fd, cs) => (resume : (()) -> (a, File))> ->
var (ans, file) = resume(());
(ans, cs ++ file)
}
} }
#? #?
#} #}
@@ -338,7 +343,7 @@ fun example0() {
# Exceptions: Premature exits # Exceptions: Premature exits
# #
sig exit : (Int) {Exit:(Int) -> Zero}-> a sig exit : (Int) {Exit:(Int) -> Zero}-> a
fun exit(n) { todo("implement exit") } fun exit(n) { switch (do Exit(n)) { } }
#? #?
#} #}