From ffe6ebd0b9b8a9cf5c68e094453f584c012d4082 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Daniel=20Hillerstr=C3=B6m?= Date: Wed, 25 May 2022 22:29:14 +0100 Subject: [PATCH] Update MSR 2022 slides --- code/unix-msr2022.links | 66 ++++++++++++++++++++++++++--------------- 1 file changed, 42 insertions(+), 24 deletions(-) diff --git a/code/unix-msr2022.links b/code/unix-msr2022.links index ec4ffa3..70aeaca 100644 --- a/code/unix-msr2022.links +++ b/code/unix-msr2022.links @@ -87,6 +87,44 @@ fun has(k, kvs) { # Homomorphisms between free algebraic models #? +#! +# What is an effect handler? +# +# Operational interpretation +# Resumeable exceptions +# Programmable and composable operating systems <--- THIS TALK +# +# Software engineering interpretation +# Builders for monads (monads as a design pattern) +# +# Functional programming intepretation +# Folds over computation trees +# Free interpreters +# +# Mathematical interpretation +# Homomorphisms between free algebraic models +#? + +#! +# +# The key idea +# +# *System calls* are an interface, implemented by an *operating system* +# +# *Effectful operations* are an interface, implemented by an *effect handler* +# +#? + +#! +# +# The key idea +# +# *System calls* are an interface, implemented by an *operating system* +# = = +# *Effectful operations* are an interface, implemented by an *effect handler* +# +#? + # # # What is an operating system? (very abstractly) @@ -148,26 +186,6 @@ fun has(k, kvs) { # #? -#! -# -# The key idea -# -# *System calls* are an interface, implemented by an *operating system* -# -# *Effectful operations* are an interface, implemented by an *effect handler* -# -#? - -#! -# -# The key idea -# -# *System calls* are an interface, implemented by an *operating system* -# = = -# *Effectful operations* are an interface, implemented by an *effect handler* -# -#? - #! # # This talk at glance @@ -243,7 +261,7 @@ typename FileDescr = Int; sig stdout : FileDescr var stdout = 1; -sig echo : (String) {Write:(FileDescr,String) -> ()}-> () +sig echo : (String) {Write:(FileDescr, String) -> ()}-> () fun echo(cs) { todo("implement echo") } #? #} @@ -254,7 +272,7 @@ typename FileDescr = Int; sig stdout : FileDescr var stdout = 1; -sig echo : (String) {Write:(FileDescr,String) -> () |%}-> () +sig echo : (String) {Write:(FileDescr, String) -> () |%}-> () fun echo(cs) { do Write(stdout, cs) } @@ -263,14 +281,14 @@ fun echo(cs) { do Write(stdout, cs) } # # Basic I/O: Handling writes # -sig basicIO : ( () {Write:(FileDescr,String) -> ()}-> a ) -> (a, File) +sig basicIO : ( () {Write:(FileDescr, String) -> ()}-> a ) -> (a, File) fun basicIO(m) { todo("implement basicIO") } #? #} -sig basicIO : ( () {Write:(FileDescr,String) -> () |%}-> a ) { |%}-> (a, File) +sig basicIO : ( () {Write:(FileDescr, String) -> () |%}-> a ) { |%}-> (a, File) fun basicIO(m) { handle(m()) { case Return(ans) -> (ans, "")