[other-lang] This Thursday: Galois Tech Talk - Dependently typed functional programming in Idris (part 1 of 3)

[Leif Warner]

Apologies for the non-Scala post. Some people in the group have in the past expressed interest in the Idris langage. It does offer a JVM target, though the primary runtime compiles to native code. It's a dependently-typed language that looks rather like Haskell. Dependent types mean that types can depend on values, and you can easily perform arbitrary computations at compile time for use in typechecking. This allows you to e.g. have assertions about list membership or what might normally be a unit test be part of the compile-time checks. Also, mathematical-style proofs can be done in such a system. This is along the lines of the kinds of static constraints you might enforce with the Scala library "shapeless", but as a more convenient full-featured built-in part of the language.

It's this Thursday at 3:30 at Galois downtown.

.

From http://galois.com/blog/2015/01/tech-talk-dependently-typed-functional-programming-idris-1-3/ :

abstract:

Idris is a pure functional language with full dependent types. In this series of tech talks, Idris contributor David Christiansen will provide an introduction to programming in Idris as well as using its development tools. Topics to be covered include the basics of dependent types, embedding DSLs in Idris, Idris’s notion of type providers, a general outline of the implementation strategy, the C FFI, and the effects library. Each talk has an associated set of exercises as well as suggested projects for further learning. Participants are expected to be familiar with functional programming in either Haskell or an ML.

bio:

David Raymond Christiansen is a Ph.D. student at the IT University of Copenhagen. For the last few months, he has been an intern at Galois, working on verifiable elections and better user interfaces for DSLs. His interests include functional programming languages, domain-specific languages, and environments that make them useful. David has contributed features such as type providers and error reflection to the Idris language as well as significant parts of the Emacs-based IDE. Additionally, he is a co-host of The Type Theory Podcast.

[Leif Warner]

Part 2 of 3 of this is tomorrow at 3:30: 

http://galois.com/blog/2015/01/tech-talk-dependently-typed-functional-programming-idris-2-3/

This time covering Idris's facilities for embedded DSLs:

https://github.com/david-christiansen/IdrisAtGalois2015/blob/master/Lecture2.idr