SumAll on Java to Haskell and Richard Eisenberg on Dependent Types

7pm: Making the Switch: How We Transitioned from Java to Haskell

In this talk, SumAll's CTO, Todd Sundsted, and Senior Software Engineer, Michael Ho, will discuss the move from Java to Haskell along two parallel paths. First, the business/political story — how SumAll convinced the decision makers, fought the nay-sayers, and generally managed the people impacted by the transition. Second, the technical story — how they actually replaced their Java code with Haskell code. Along the way, they will address their hopes and expectations from transitioning from Java to Haskell, and will conclude with the results they've gained and seen to date.

8pm: Stitch: The Sound Type-Indexed Type Checker

Richard Eisenberg will present his work on Stitch, a typed
lambda-calculus interpreter, written in Haskell using type-indexed
abstract syntax. The datatype that represents expressions in the
interpreter is indexed by its Stitch type, meaning that only
well-typed expressions can be represented. However, Stitch is not just
a toy example: the interpreter is an application with a REPL, and thus
contains a parser and type-checker. It also can optimize expressions
via a common-subexpression-elimination pass and presents a flexible,
expressive user interface that can be used to teach the
lambda-calculus. The implementation of Stitch taps into a wide range
of Haskell features for working with fancy types, including
generalized algebraic datatypes (GADTs), existentials, higher-rank
types, singletons, and the new type-indexed TypeRep feature. This talk
will include a brief introduction to these features and use Stitch as
a case study to show that Haskell is ready to support fancy types used
in anger, even though it still lacks support for full dependent types.

Richard is an Assistant Professor of Computer Science at Bryn Mawr
College, an undergraduate-focused women's college in suburban
Philadelphia. He is a 2016 graduate from the PhD program at the
University of Pennsylvania, where he worked with Stephanie Weirich.
His dissertation was on a design for the surface syntax, internal
language, and type inference algorithm to support dependent types in
GHC; he is a core contributor to GHC and is currently funded by an NSF
grant to implement dependent types in GHC.