[Haskell-cafe] Microsoft PhD Scholarship at Strathclyde

[Conor McBride]

Hi Wolfgang

On 14 Mar 2009, at 12:00, Wolfgang Jeltsch wrote:

> Am Samstag, 14. März 2009 08:19 schrieb Peter Verswyvelen:
>> Well, in C++ one can already use the numerical values with  
>> templates for
>> achieving a lot of compile time computations.
>>
>> So I would be very happy to have this feature in Haskell. It might  
>> also be
>> good research towards full dependent types no?
>
> I doubt that it will be a good thing to include full dependent types  
> into a
> language with partial functions like Haskell.

I think we could manage quite a bit, though. It seems
reasonable to allow types to contain expressions
drawn from a total fragment of the value language.
Even a tiny fragment (such the expressions built only
from fully applied constructors and variables) would
be a useful start (vector head, tail, zip, but not
vector append).

The present capacity for open type functions suggests
that it shouldn't be too violent to add some total
value-functions (probably with a flag allowing
self-certification of totality).

We should also ask what the problem is with partiality?
I'd far rather have a simplistic Set-based intuition
about what values in types might mean, rather than
worrying about vectors of length bottom. The other
side of that coin is that it makes perfect sense to
have partial *computations* in types as long as they're
somehow distinguished from total values, and as long as
the system remembers not to *run* them until run-time.

My point: it isn't all or nothing -- there's a slider
here, and we can shift it a bit at a time.

>
>
> Conor, is Epigram currently under development?

We've even stopped working on the engine and started
working on the chassis. I'm in an intensive teaching
block until the end of April, but from May it becomes
Priority. The "Reusability and Dependent Types"
project studentship will hopefully bring an extra
pair of hands, come October.

Epigram exists to be stolen from, so I'll be trying
to encourage a literate programming style and plenty
of blogging. We've spent a lot of time figuring out
how to make the system much more open and modular,
so it will hopefully prove easier for people to
contribute to as well as to burgle. The worst thing
about Epigram 1 was just how monolithic and
impenetrable the code base became. It was a valuable
learning experience but no basis for further
progress. This time, we optimize for clarity.

I don't see any conflict -- indeed I see considerable
synergy -- in working simultaneously on the
experimental frontier of dependent type systems and
on the pragmatic delivery of their basic benefits via
a much more established language like Haskell.
Indeed, I think we'll learn more readily about the
engineering realities of developing applications with
dependent types by doing plenty of the latter.

I don't think functional programmers should wait for
the next generation of languages to mature before
picking up this particular habit...

All the best

Conor