Conor's Rule?

Edwin Brady writes in "How to write programs in two easy steps", that

I think it's also an area where dependently typed languages like Epigram will shine, because it will one day be possible to write verified interpreters for domain specific languages …

I immediately thought "I can write dependently typed programs right now with GADTs, and I can do so in GHC Haskell, Scala, or the upcoming C#". This is, of course, only mostly true, since none of these does termination checking, and the syntax is awkward.

The same blog post later references Greenspun's Tenth Rule:

Any sufficiently complicated C or Fortran program contains an ad hoc, informally-specified, bug-ridden, slow implementation of half of Common Lisp

and I thought that my programs follow a similar pattern with dependent types: I'm always simulating them informally. Based on Section 6.1: "The Trouble with Faking It" in Conor McBride's Faking It (Simulating Dependent Types in Haskell) (mirror), I wonder if there's any truth to something we might call

Conor's Rule

Any sufficiently complicated Haskell or ML program contains an ad hoc, informally-specified, bug-ridden, half-completed simulation of dependent types.

C++ and GADTs

I just noticed this post about GADTs in C++. It's more about C++'s warts than GADTs, but it's interesting nonetheless.

I also noticed recently, while preparing for my upcoming talk at the theory lunch (mirror, suspected future permalink, presently 404), that because the constructors in the OOP version of GADTs each get their own class, the class name can function as the constructor tag. This leads to what is called the Curiously Recurring Template Pattern in C++. Example:

Haskell	C++
data Nat t where Z :: Nat ZTag S :: Nat n -> Nat (STag n) data ZTag data STag n	template<class T> class nat {}; class zero : nat<zero> {}; template<class N> class succ : nat<succ<N> > { public: succ<N>(nat<N> x) : pred(x) {} nat<N> pred; };

Of course, the tags in the Haskell version could have the same names as the constructors, since the constructor and type namespaces in Haskell are disjoint, but they would still have distinct meanings, unlike in the C++ code.

If I Had Time

Projects I would work on if I had time:

• On Simulating Dependent Types with Guarded Algebraic Datatypes:
  • Automatic lambda lifting for the Haskell syntax.
  • Automatic printing of Scala and C# syntax
  • A lambdabot plugin for lifting types, using GHC-as-a-library.
• Sized lists:
  • Make a cabal-ized, hackage-d sized lists library.
  • Automatically translate the buggy NoFib benchmarks to using sized lists to see if the bugs get caught by the type checker.
• Write Data.Scannable and instance Foldable ((->) a)