Edwin Brady at Lambda World 2016

Edwin Brady at Lambda World 2016

 

Type-driven Development of Communicating Systems in Idris

Idris is a functional programming language with dependent types, which supports ‘total’ functional programming. A function is total if, for all well-typed inputs, it gives either a complete result of a finite prefix of an infinite result, in finite time. Total functions give us strong guarantees about their behavior: for example functions can’t crash due to badly formed inputs, servers will always produce responses to requests. In this talk, I’ll show how Idris supports total programming, with a series of examples. As an extended example, I’ll show how to define a type for describing communicating concurrent systems which, by writing total functions, guarantees that concurrent programs will interact as intended.

Subscribe to our official YouTube channel to be updated when new videos are added.

blog comments powered by Disqus

Ensure the success of your project

47 Degrees can work with you to help manage the risks of technology evolution, develop a team of top-tier engaged developers, improve productivity, lower maintenance cost, increase hardware utilization, and improve product quality; all while using the best technologies.