PuritasA journey of a thousand miles towards side-effect free code

Overview About me and F# Open Source projects What is purity and how does it perform Background Proposed solution Why is purity relevant for you Summary ( demo, if time) Q&ANote: I would love questions, but please save them to the end of the talk, lotto say and time is mana, I mean limited2 / 42

About me (very shortly) Ramón Soto Mathiesen MSc. Computer Science DIKU/Pisa and minors in Mathematics HCØ CompSci @ SPISE MISU ApS–“If I have seen further it is by standing on the shoulders of giants”-- Isaac Newton (Yeah Science, Mostly mathematics)–Elm (JS due to ports) with a bit of Haskell and a bit of F# (fast prototyping) Elm / Haskell / TypeScript / F# / OCaml / Lisp / C / C# / JavaScript Founder of Meetup for F#unctional Copenhageners (MF#K) Blog: and Twitter: @genTauro423 / 42

F# Open Source projects Previous workplace (CTO of CRM @ Delegate A/S):–MS CRM Tools: –Delegate.Sandbox: workplace (SPISE MISU ApS):–Syntactic Versioning (SynVer @ F# Community Projects) –Mostly driven by Oskar Gewalli (@ozzymcduff)Puritas, isolated side-effects at compile-time in F#4 / 42

What is purity There was an interesting blog post with regard of this topic thatsurfaced after my talks was made public by #fsharpX:– It was a bit unfortunate the definition of purity that was taken fromWP at the top of that post:– F# and Purity from Eirik Tsarpalis' blog“ Purely functional programing may also be defined by forbiddingchanging state and mutable data.”If we can’t change state, why even run it?let main state state (* If we can’t change state? I guess we are done *)5 / 42

What is purity I’m guessing that we should be talking about pure functions WPinstead:–The function always evaluates to the same result value given the samearguments–Evaluation does not cause any observable side effect or output, such asmutation of mutable objects or output to I/O devicesOK, so we change state and we are still pure:let rec main state function 0u state n main (state 1) (n - 1u) So in purely functional programing, state changes, but in a sound way6 / 42

What is purity Be careful to not become to pedantic, still from pure functions WP:– The result value need not depend on all (or any) of the argument values.However, it must depend on nothing other than the argument valuesSo this is not pure?let foo () 42let bar x foo () x (* besides x, the result depends on foo *) What about curried arguments?let baz x y x ylet qux fun x fun y x y (* nested lambda depends on parent *)7 / 42

What is purity The previous pure functions (foo, bar, baz, qux) canbe mapped directly to λ-calculus, which ismathematically pure.Therefore, the result of combining pure functions,would still be considered pure–Save this “bit of information” for later8 / 42

What is purity Lets recap:–Functions always evaluates to the same output value given thesame input–Evaluation does not cause any side effect, such as mutation ofmutable objects or output to I/O devices–Functions can be mapped directly to λ-calculus, which ismathematically pure.–The result of combining pure functions, would still be consideredpure9 / 42

and how does it perform Taken from SO (Academia):–Pippenger [1996], “Pure Versus Impure Lisp", comparing pureLisp (strict evaluation, not lazy) to one that can mutate data,establishes that is the best you can do is Ω(n log n) in the purewhen problems are O(n) in the impure version–Bird, Jones and De Moor [1997], “More haste, less speed: Lazyversus eager evaluation”, demonstrate that the problemconstructed by Pippenger can be solved in a lazy functionallanguage in O(n)10 / 42

and how does it perform Taken from SO: (In Practice)–Okasaki [1996] and Okasaki [1998], “Purely FunctionalData Structures”, many algorithms can be implementedin a pure functional language with the same efficiency asin a language with mutable data structures. My blog: F# - Puresort of lists (Okasaki)11 / 42

and how does it perform Taken from SO: (In Practice)–SPJ and Marlow [1999], “Stretching the storagemanager: weak pointers and stable names in Haskell”,due to referential transparency, even when using memoand unsafe IO, will not change pure behaviormemo :: (a b) (a b) and unsafePerformIO :: IO a afib :: Int Intfib memo ufibufib :: Int Intufib 0 1ufib 1 1ufib n fib (n – 1) fib (n – 2)12 / 42

and how does it perform Taken from SO: (In Practice)–Remark: To ensure that impurity can be hidden underreferential transparency, the following must be added ontop of all your files so that side-effects must be handledthrough Monads to avoid “Launching the missiles”:{-# LANGUAGE Safe #-}13 / 42

Background A few years ago I created Delegate.Sandbox in order to provide side-effectfree code in F#I mainly did it to troll Haskell people. MF#K is a cross-functional MeetupGroup and haskellers can be a bit annoying with their purity sometimes On a serious note, the reason is that most developers don’t really knowwhich I/O side-effects are executed in their applicationsThe library is built on top of the AppDomain Class which allows toRun Partially Trusted Code in a Sandbox (.NET)Talk at MF#K (2015-09-29): I/O side-effects safe computations in F#14 / 42

Background Delegate.Sandbox Pros:–Guaranteed side-effect free code–Idiomatic syntax:15 / 42

Background Delegate.Sandbox Cons:–Tainted expressions (Unsafe) cause run-time errors–Not thread-safe (race conditions)–Post-Build F# script (need code to be compiled first)–Reason, the F# Compiler Services (FCS) only supporteduntyped syntax trees back then16 / 42

Background17 / 42

Proposed solution Thanks to Microsoft and the F# Community, FCS now alsosupports typed expression trees (*)So lets recall: “Therefore, the result of combining purefunctions, would still be considered pure”Now that we can type-check our code with FCS, we shouldbe able to reason about if code is pure (or not)(*) - Almost, at least Sum Types aren’t supported (yet?)type FooBar Foo of int Bar of float (* not working *)18 / 42

Proposed solution There is actually a POC in the F# Compiler to check if anexpression has effects (flag: --test:HasEffect)And recently I found out, from a tweet, that there was anotherproject trying to separate pure from impure code:– PolyglotSymposium.SandlineBoth experiments are based on typed expression trees as well asmy project, SpiseMisu.Puritas, but what makes my projectdifferent from theirs is that I mark pure branches with a type whilethey rely on marking idiomatic code as pure or not (true/false)19 / 42

Proposed solution The reason I’m adding a type is because F# is an eager (strict) impurefunctional language and that way I can distinguish branches atcompile time (F# is what it is and we can’t/shouldn’t change that)Therefore, my approach is to add ad-hoc pure branches to ourimpure codelet foo : int Pure purify 42 Just think of it as with the lazy keyword, where we are able to addad-hoc lazy branches to our strict codelet bar : int Lazy lazy 4220 / 42

Proposed solution So now, we just need to find all our code branches that return purecode. This is actually very easy to do as F# (.NET) has a canonicaltype signatures:let foo : int list [ 42 ]let bar : List System.Int32 [ 42 ] Therefore we can just look for all signatures that comply with:((.) . SpiseMisu.Puritas.Pure) (ends with)SpiseMisu.Puritas.Pure . (starts with) Even though we can type-check, this will not be enough .21 / 42

Proposed solution as we will have to taint code expressions thatdon’t comply with the following recursiveparent/child code branch logic:Code branchesParent ImpureParent PureParent TaintedChild ImpureImpureTaintedTaintedChild PureImpurePureTaintedChild TaintedTaintedTaintedTainted22 / 42

Proposed solution Therefore our taint-checker marks the following branches as valid:–Impure Impure (regular F# code is perfectly valid)–Impure Pure (pure code consumed by impure is also OK)–Pure Pure (used when defining pure libs and/or APIs)All the other cases will be marked as invalid (tainted)Invalid code will bubble up to the top, tainting the holeexpression as invalid. Just think of taint like poison in Tony HoareCommunicating Sequential Processes (CSP)23 / 42

Proposed solution Like I mentioned before, my project differs from theothers in that I’m able to mark the following code asvalid, while they would mark it as invalid (true/false): BasicPatterns.NewArray ( ,exprs) - (* FSharpType * FSharpExpr list *)let msg "BasicPatterns.NewArray"let tag' (* Reason: Arrays are mutable, therefore impure *)tag taint msg range Tag.Impure taint msg range (taintExprs debug (tag) exprs)debug mexpr msg tag' tagtag'24 / 42

Proposed solution We only consider pure code signatures that comply with:((.) . SpiseMisu.Puritas.Pure) (ends with)SpiseMisu.Puritas.Pure . (starts with) That means that F# Core is impure as wellpurify (1 2) (* is actually impure, so “Computer Says No” *) So how do you code without basic arithmetic operators?Well F# to the rescue. We just expand our pure type with some operatoroverloading and we are good to go:purify 1 purify 225 / 42

Proposed solution So what are we looking at?#r @"SpiseMisu.Puritas.dll"open SpiseMisu.Puritaslet sum : int Pure - int Pure - int Pure fun x y - x ylet result sum (purify 42) (purify 42)let inc : (int Pure - purify (fun x - x let dec : (int Pure - purify (fun x - x let add : (int Pure - purify (fun x y - xletletletletfoobarbazqux let letrec fold fNilCons(x,xs)map f xs int Pure) Pure purify 1)int Pure) Pure purify 1)int Pure - int Pure) Pure y)dec * purify 42inc * dec * purify 42purify 42 * (inc * dec)purify 42 / add / purify 42acc function- acc- fold f (cons (f x) xs) xsfold f nil xslet foobar cons (purify 42) nil map (fun x - x x)26 / 42

Proposed solution It’s pretty idiomatic right? From/to (purify/value) and list support (cons/nil and Cons Nil ) In order to wrap/unwrap pure functions/values, I added a few extraoperators (apply * , left/right composition * and * , pipe * , )I also added a few functions (memo, concurrent, delay) withreferential transparency to achieve better performanceSince F# Core is impure, we will need boolean arithmetic operators aswe can’t overload them: (EQ), / (NEQ) - (G), - (L), (GE), (LE)27 / 42

Proposed solution Fibonacci ( memo version):#r @"SpiseMisu.Puritas.dll"open SpiseMisu.Puritaslet zero purify 0let one purify 1let two purify 2let rec fib : int Pure - int Pure fun n - ifzero n then oneelif one n then oneelse(n-one fib) (n-two fib)(* Real: 00:00:08.959, CPU: 00:00:09.132, GC gen0: 2312, gen1: 0 *)Array.init 36 (purify fib value)let rec ufib : int Pure - int Pure fun n - ifzero n then oneelif one n then oneelse(n-one fibMemo) (n-two fibMemo)and fibMemo : int Pure - int Pure memo ufib(* Real: 00:00:00.000, CPU: 00:00:00.000, GC gen0: 0, gen1: 0 *)Array.init 36 (purify fibMemo value)28 / 42

Proposed solution Lets recap (SpiseMisu.Puritas):––A library: SpiseMisu.Puritas.dll ( 100 lines of code) Provides ad-hoc pure branches to our impure code (think of it like with lazy)A taint-checker: SpiseMisu.Puritas.TaintChecker.fsx ( 1000 lines of code) Only depending on F# Core and FCS (HAL 9000, I mean @ncave, Fable much?) Tainting expressions at compile-time and errors are prettified with Markdown syntax–Idiomatic, except for boolean arithmetic operators–Acceptable performance due to referential transparency (memo, .)29 / 42

Why is purity relevant for you Purity it’s not just academic mumbo jumboPrivacy-by-design, get used to it as General Data Protection Regulation (GDPR)arrives next year:– Doom-day: 2018-05-28Easiest way to comply with this approach is by isolating your side-effect. Languagessupporting this at the moment are: Haskell, COQ, Idris, PureScript, Elm amongothers and hopefully soon F#, due to SpiseMisu.PuritasI know, the people from the UK are just thinking: “Why should we care?”, well:–The future of UK data protection law post-Brexit “The GDPR will come into effect before the UK leaves the European Union” “The UK will still have GDPR-like rules after it leaves the European Union”30 / 42

Why is purity relevant for you31 / 42

Why is purity relevant for you We recently had two cases where sensitive was leaked through websites (both casescould easily be avoided by using something like Hardy Jones elm-proxy):–SKAT (Danish Ministry of Taxation) –Novo Nordisk (Denmark's Top 2 greatest company, turnover/revenue: 107.927 mDKK) Some people when login in could choose other peoples profiles, presented in a list, like admin mode95.000 job applicants data (name, phone, e-mail, ) was published to their main website (human error)What if it was next year, both blamed their software provider? (Sanctions)–Fines in the size of 10/20 mEUR or 2%/4% annual worldwide turnover (whichever is greater)Note: turnover (UK)/revenue (US) reference to the amount of money a companygenerates without paying attention to expenses or any other liabilities32 / 42

Why is purity relevant for you33 / 42

Why is purity relevant for you Are you willing to deliver software from Doom-day next year?– How are you going to convince your customers that you are doing everythingto ensure that no unwanted side-effects and hereby data-leaks will occur?Lets remove the blame-game and the say a lot but do nothing fromthe equation and focus on solving the real problem, with science ofcBy tainting unwanted side-effects at compile-time, no system willbe deployed to production with vulnerabilitiesYou will just need to request pure code through signatures files fromyour contractors or software providers (next slide)34 / 42

Why is purity relevant for younamespace EvilCorpmodule BusinessLogic (* Connect to 3rd party and leak data, perfectly fine *)val foo : int - int(* Create folder and log sensitive data, fine as well *)val bar : float - floatvsnamespace CantBeEvilCorpAnymoremodule BusinessLogic (* Connect to 3rd party and leak data, Computer Says No *)val foo : int Pure - int Pure(* Create folder and log sensitive data, Computer Says No *)val bar : float Pure - float Pure“Don't be evil” enforced by code !!!35 / 42

Why is purity relevant for you Just think of it in Simon P. Jones (SPJ) terminology:–Isolate side-effects to avoid “Launching the missiles”–Isolate side-effects to avoid “Leaking data”By enforcing purity, the “Volkswagen emissions scandal”(dieselgate), would never have been possible as theGovernments could just require that car manufacturessoftware, complied with their signatures files36 / 42

So Don Vito Syme37 / 42

Can I haz pure keyword so that38 / 42

Can I haz pure keyword so that The following code .let foo : int Pure purify 42 becomes#nowarn “46”let foo : int Pure pure 4239 / 42

F# can join the Mad Tea Party40 / 42

Summary ( demo, if time) SpiseMisu.Puritas provides ad-hoc side-effect free code at compile-time Privacy-by-design, General Data Protection Regulation (GDPR): Doom-day: 2018-05-28 Dank memes aside, I will make a formal request for the reserved keyword pure atF# Language and Core Library Suggestions–I will post link on Twitter, please vote if you agree that it should be part of F# Core If @ncave pulls it off, F# could be the first to provide purity at both BE and FE !!! “Stay Pure, Isolating Side-Effects” (SPISE MISU ApS, it was all part of the Masterplan)– Michael Werk Ravnsmed dixitFinally, I would like to thank Joakim Ahnfelt-Rønne (@Continuational) for his reviews, his initial“counter” examples and specially showing that the library was pretty much useless without thepossibility to lift impure values into pure functions (ex: load an int from a file, increment and save)Any time left to “Show some code” and demo?41 / 42

Q&AOnly “old” Spaniards will get this42 / 42

5 / 42 What is purity There was an interesting blog post with regard of this topic that surfaced after my talks was made public by #fsharpX: – F# and Purity from Eirik Tsarpalis' blog It was a bit unfortunate the definition of purity that was taken from WP at the top of that post: – “ Purel