London Scala Users' Group - London Scala Talks: Vilem Liepelt
Tuesday 30 April 2019, 19:30 - 20:30
1 Cousin Ln, London, Reino Unido
We're looking for a speaker and a venue for this event - reach out to us if you'd like to speak! For April's talks we are delighted to be joined by Vilem Liepelt who will be presenting on type systems: * Resource-oriented programming with graded modal types * Linear types, derived from Girard's Linear Logic, provide a means to expose safeinterfaces to stateful protocols and language features, e.g. channels and filehandles. Data is delineated into two camps: unconstrained values which can beconsumed or discarded arbitrarily and 'resources' which must be used exactlyonce. Bounded Linear Logic (BLL) [1], allows tracking a more nuanced notion ofnonlinearity via the natural numbers semiring which is baked into its proofrules. Our system of Graded Modal Types generalises BLL by parameterising overthe resource algebra, thus allowing a wide array of analyses to be captured inthe type system. In this talk we will explore how graded modal types and linearity convenientlyextend our typical toolkit of parametric polymorphism and indexed types,allowing us to reason about pure and effectful programs in a novel,resource-oriented, manner. Session typed channels and mutable arrays are justtwo examples of programming idioms that can be provided in such a languagewithout having to give up safety and compositionality. We will see this inaction via Granule [2], our implementation of a functional language with a typesystem which supports all these features. 1. Girard, Scedrov, Scott (1992)2. https://github.com/granule-project/granule Pizza and drinks will be sponsored by District4 https://district4.io/
Publicado por: Betabeers