
Hi folks On 18 Feb 2009, at 10:35, Ryan Ingram wrote:
On Wed, Feb 18, 2009 at 2:12 AM, Lennart Augustsson
wrote: Also, if you are using ghc you can turn on the extension that allows undecidable instances and make the type system Turing complete.
<snark>And you get the additional pain of a potentially nonterminating compiler without any of the nice type-level syntax that you really want when writing code at that level</snark>
Seriously, I love undecidable instances, but there's gotta be a way to make type-level programming less painful. GHC team: please give us type-level integers that don't suck! If I ever have to see S (S (S (S Z))) again it's too soon.
Just to say that a formal advert will appear any day now, but I should strike while the iron is hot --- Microsoft Research have been generous enough to sponsor a PhD scholarship at the University of Strathclyde (supervised by me) on a project which, for reasons of public decorum is called "Haskell Types with Numeric Constraints" but which translates to type-level integers that don't suck and then some... Start date will be October 2009 or so. An internship at MSR is typically part of the package, and in this case is likely to involve experimenting with extensions to GHC. So, if you're ready, willing, and able to work on making Ryan's wishes come true, drop me a line to let me know you're interested in working on (dependent types for) Haskell in Glasgow. All the best Conor