mopdf.com

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: http://blog.stermon.com/ and Twitter: @genTauro423 / 42

F# Open Source projects Previous workplace (CTO of CRM @ Delegate A/S):–MS CRM Tools: –Delegate.Sandbox: ub.io/Delegate.Sandbox/Current 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