[Haskell-cafe] question on types

[Conor McBride]

Hi folks

On 18 Feb 2009, at 10:35, Ryan Ingram wrote:

> On Wed, Feb 18, 2009 at 2:12 AM, Lennart Augustsson
> <lennart at augustsson.net> 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