mirror of
https://github.com/dhil/phd-dissertation
synced 2026-03-13 02:58:26 +00:00
Compare commits
2 Commits
c60dc80fde
...
2cecb13d34
| Author | SHA1 | Date | |
|---|---|---|---|
| 2cecb13d34 | |||
| ed634fcaa3 |
@@ -56,12 +56,12 @@ fun has(k, kvs) {
|
||||
#!
|
||||
#
|
||||
# Effect Handler Oriented Programming
|
||||
# A Gentle Introduction
|
||||
# Lets build an operating system
|
||||
# Daniel Hillerström
|
||||
# Laboratory for Foundations of Computer Science
|
||||
# The University of Edinburgh, Scotland, UK
|
||||
#
|
||||
# EPL, The University of Edinburgh
|
||||
# Elements of Programming Languages
|
||||
# November 17, 2022
|
||||
#
|
||||
# https://dhil.net/research/
|
||||
@@ -118,7 +118,7 @@ fun has(k, kvs) {
|
||||
# Plotkin and Pretnar (2009) invented effect handlers.
|
||||
|
||||
# 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) }
|
||||
|
||||
|
||||
@@ -152,7 +152,7 @@ fun sem(m) {
|
||||
#?
|
||||
#}
|
||||
|
||||
#?
|
||||
#!
|
||||
#
|
||||
# Characteristics of effect handlers
|
||||
#
|
||||
@@ -161,7 +161,7 @@ fun sem(m) {
|
||||
# * 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
|
||||
# Resumeable exceptions
|
||||
# Programmable and composable operating systems
|
||||
#
|
||||
# Software engineering interpretation
|
||||
# Builders for monads (monads as a design pattern)
|
||||
# Composable monad builders (monads as a design pattern)
|
||||
#
|
||||
# Functional programming interpretation
|
||||
# Folds over computation trees
|
||||
@@ -375,7 +375,7 @@ sig stdout : FileDescr
|
||||
var stdout = 1;
|
||||
|
||||
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)
|
||||
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
|
||||
#
|
||||
@@ -445,7 +450,7 @@ fun example0() {
|
||||
# ,fun(x){ handle(E[x]) { case <Op(p) => r> -> N case ... }}/r]
|
||||
# (if Op \notin E)
|
||||
#
|
||||
#
|
||||
#?
|
||||
|
||||
#{
|
||||
#!
|
||||
@@ -453,7 +458,7 @@ fun example0() {
|
||||
# Exceptions: Premature exits
|
||||
#
|
||||
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() {
|
||||
basicIO(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() {
|
||||
basicIO(fun() {
|
||||
status(fun() {
|
||||
echo("dead"); exit(1); echo("code")
|
||||
echo("Hello"); exit(1); echo("World")
|
||||
})
|
||||
})
|
||||
}
|
||||
@@ -518,7 +523,7 @@ sig example1' : () -> Int
|
||||
fun example1'() {
|
||||
status(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
|
||||
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]
|
||||
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)
|
||||
fun reifyProcess(m) {
|
||||
todo("implement reifyProcess")
|
||||
handle(m()) {
|
||||
case ans -> Done(ans)
|
||||
case <Interrupt => resume> ->
|
||||
Paused(fun() { resume(()) })
|
||||
}
|
||||
}
|
||||
#?
|
||||
#}
|
||||
|
||||
@@ -61,7 +61,7 @@ fun has(k, kvs) {
|
||||
# Laboratory for Foundations of Computer Science
|
||||
# The University of Edinburgh, Scotland, UK
|
||||
#
|
||||
# Huawei Research Centre Zurich, Switzerland
|
||||
# Huawei Research Centre Zürich, Switzerland
|
||||
# October 13, 2022
|
||||
#
|
||||
# https://dhil.net/research/
|
||||
@@ -260,7 +260,7 @@ sig stdout : FileDescr
|
||||
var stdout = 1;
|
||||
|
||||
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)
|
||||
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
|
||||
#
|
||||
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
|
||||
fun status(m) {
|
||||
todo("Implement status")
|
||||
handle(m()) {
|
||||
case ans -> 0
|
||||
case <Exit(n)> -> n
|
||||
}
|
||||
}
|
||||
#?
|
||||
#}
|
||||
|
||||
@@ -139,7 +139,7 @@ fun has(k, kvs) {
|
||||
# - Extremely compositional
|
||||
#
|
||||
# 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;
|
||||
|
||||
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)
|
||||
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
|
||||
fun status(m) {
|
||||
todo("implement status")
|
||||
handle(m()) {
|
||||
case ans -> 0
|
||||
case <Exit(n)> -> n
|
||||
}
|
||||
}
|
||||
#?
|
||||
#}
|
||||
|
||||
@@ -260,7 +260,7 @@ sig stdout : FileDescr
|
||||
var stdout = 1;
|
||||
|
||||
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)
|
||||
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
|
||||
#
|
||||
sig exit : (Int) {Exit:(Int) -> Zero}-> a
|
||||
fun exit(n) { todo("implement exit") }
|
||||
fun exit(n) { switch (do Exit(n)) { } }
|
||||
#?
|
||||
#}
|
||||
|
||||
|
||||
Reference in New Issue
Block a user