The process of writing large parallel programs is complicated by the need to specify both the parallel behaviour of the program and the algorithm that is to be used to compute its result.
Interpreting types as abstract values [The Abstract of the lecture notes] We expound a view of type checking as evaluation with `abstract values'. Whereas dynamic semantics, evaluation, deals with (dynamic) values like 0, 1, etc., static semantics, type checking, deals with approximations like int. A type system is sound if it correctly approximates the dynamic behavior and predicts its outcome: if the static semantics predicts that a term has the type int, the dynamic evaluation of the term, if it terminates, will yield an integer. As object language, we use simply-typed and let-polymorphic lambda calculi with integers and integer operations as constants. We use Haskell as a metalanguage in which to write evaluators, type checkers, type reconstructors and inferencers for the object language.
Curry is a universal programming language aiming to amalgamate the most important declarative programming paradigms, namely functional programming and logic programming.
"Generalized Algebraic Data Structures" have become a a hot new topic. They have recently been added to the GHC compiler. They support the construction, maintenance, and propagation of semantic properties of programs using powerful old ideas about types (the Curry-Howard Isomorphism) in surprisingly easy to understand new ways. The language Omega was designed and implemented to demonstrate their utility. Here a a few talks I gave that explains how they work. Also class lectures
The Curry-Howard correspondence is a mapping between logic and type systems. On the one hand you have logic systems with propositions and proofs. On the other hand you have type systems with types and programs (or functions). As it turns out these two very different things have very similar rules. This article will explore the Curry-Howard correspondence by constructing a proof system using the Haskell type system (how appropriate since Haskell is named after Haskell Curry, the "Curry" in "Curry-Howard"). We'll set up the rules of logic using Haskell types and programs. Then we'll use these rules as an abstract interface to perform some logic profs.
In denotational semantics and functional programming, the terms monad morphism, monad layering, monad constructor, and monad transformer have by now accumulated 20 years of twisted history. The exchange between Eric Kidd and sigfpe about the probability monad prompted me to investigate this history
Daniel Fridlender Mia Indrika March 2001 Inspired by Danvy, we describe a technique for defining, within the Hindley-Milner type system, some functions which seem to require a language with dependent types. We illustrate this by giving a general definition of zipWith for which the Haskell library provides a family of functions, each member of the family having a different type and arity. Our technique consists in introducing ad hoc codings for natural numbers which resemble numerals in lambda-calculus
My existing research is mainly focused on lightweight generic programming techniques and the essence of (OO-style) design patterns. * Modular Visitor Components: A Practical Solution to the Expression Families Problem Bruno C. d. S. Oliveira ECOOP 2009. * Scala for Generic Programmers Bruno C. d. S. Oliveira, Jeremy Gibbons In Ralf Hinze, editor, Proceedings of the ACM SIGPLAN Workshop on Generic Programming (WGP'08) July 2008. * Objects to Unify Type Classes and GADTs Bruno C. d. S. Oliveira, Martin Sulzmann ICFP 2008
Simpler, Easier! In a recent paper, Simply Easy! (An Implementation of a Dependently Typed Lambda Calculus), the authors argue that type checking a dependently typed language is easy. I agree whole-heartedly, it doesn't have to be difficult at all. But I don't think the paper presents the easiest way to do it. So here is my take on how to write a simple dependent type checker. (There's nothing new here, and the authors of the paper are undoubtedly familiar with all of it.) First, the untyped lambda calculus. I'll start by implementing the untyped lambda calculus. It's a very simple language with just three constructs: variables, applications, and lambda expressions, i.e.,
A continuation-based, backtracking, logic programming monad. An adaptation of the two-continuation implementation found in the paper Backtracking, Interleaving, and Terminating Monad Transformers available here: http://okmij.org/ Control.Monad.Logic.Class
Dependent type systems, in which types can depend on values, admit detailed specifications of function behavior and data invariants. Programming languages based on System F do not have dependent types, and are therefore more limited in what structure or function invariants can be encoded in the type system. In this paper, we show how guarded algebraic datatypes can simulate dependent types. We formalize additions to a guarded-datatypes-enhanced System F that allow types to depend on values and discuss the programming style that results, which is similar to theorem proving. Our technique can be applied to multiple existing programming languages, including Haskell and C#. We also introduce an idiom for eliminating any execution cost from programming with simulated dependent types. We have developed a tool to automatically produce the boilerplate necessary for the simulation, and we have used it to enforce data structure invariants and to allow elision of run-time bounds checks.
I didn't see anyone post them yet, so here are the slides from Tim Sweeney's POPL talk entitled "The Next Mainstream Programming Languages: A Game Developer's Perspective". I know Tim and I aren't the only game developers who follow LtU, and I figure even non-game developers might find them quite interesting!
The Haskell project was begun in order to unify "more than a dozen non-strict, purely functional programming languages". (mirror) We are rapidly approaching that many viable choices for programming with dependent types. 1. Epigram 2. ATS (successor to Dependent ML) 3. Agda (successor to Cayenne) 4. Ωmega 5. NuPrl 6. Twelf 7. Isabelle 8. Coq etc caveats * Some of the items on this list are theorem provers first and dependently-typed programming languages second. Adam Chlipala argues that this is not such a problem for Coq. * Some of these choices may not be real options for programing with dependent types. Twelf is designed for programming about programming languages, and, if I remember correctly, doesn't have parametric polymorphism because of something having to do with higher-order abstract syntax. Is it time yet to do anything about the cornucopia of options? see comments
Chameleon (the language) is a Haskell style language to experiment with advanced type extensions such as type classes and generalized algebraic data types. The user can program her own type extensions via Constraint Handling Rules (CHRs). Chameleon (the system) is also a compiler framework. Chameleon has been applied in a number of project such as type error reporting, programming language program verification etc. In the XHaskell implementation we heavily rely on the compiler infrastructure provided by Chameleon. Language Features * LanguageOverview * HowtoinstallandrunChameleon The Compiler * CompilerOverview * ChameleonGecko * StandaloneSolver Applications *TypeErrorDiagnosis *ProgramVerification MartinSulzman