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