Home » forums » LtU Forum

GADTs + Extensible Kinds = Dependent Programming

Tim Sheard claims that usual functional programming methods (plus two new features found in his new programming language Ωmega) take care of some of the needs dependent types are often thrown at.

By Jim Apple at 2005-05-06 05:32 | LtU Forum | previous forum topic | next forum topic | other blogs | 14524 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

I believe he claims they take

I believe he claims they take care of all needs dependent types are thrown at; although he does not offer proof.

By Jeff Cutsinger at Sun, 2005-05-08 17:31 | login or register to post comments

Haskell Workshop talk

He's scheduled for the Haskell Workshop, to present Putting Curry Howard to Work. The latest paper presents this material in a rather accessible and appealing form, from the point of view of a Haskell guy who's not schooled in dependent types.

The redundancy in the name Ωmega is ugly. :-)

By Scott Turner at Fri, 2005-07-22 14:51 | login or register to post comments

Not really redundant

How do you think they spell it in the greek? (Ωμεγα + accents)
It's just a mix of english and greek.

By Jeff Cutsinger at Fri, 2005-07-22 16:43 | login or register to post comments

Offtopic comments are fun

My guess is that the Grecians would have "spelled" it as Ω. For example, we spell W in English with a single character, and not as a word, i.e. Dubya. To draw another analogy, we already have programming languages named after letters in the english alphabet - C and D. We do not generally refer to these languages as "See" and "Dee".

-- Java.Next

By rreyelts at Mon, 2005-07-25 19:23 | login or register to post comments

Hey why don't we ask one of o

Hey why don't we ask one of out resident "Grecians"? Andris?

By Marcin Tustin at Tue, 2005-07-26 11:10 | login or register to post comments

Sure

You must have meant "Achilleas", right? :)

But don't worry, people thought I am Lithuanian, German, Dutch, Jew, Russian, etc. (even Pole ;) ) depending on their own background (so not a single Dutch thought I am Dutch :) ).

By Andris Birkmanis at Tue, 2005-07-26 11:49 | login or register to post comments

Well.

According to Revelation 1:8, we're both right.
The text says "I am the Αλφα and the Ω".

By Jeff Cutsinger at Tue, 2005-07-26 19:07 | login or register to post comments

Pros and Cons

Can I get some of the Type Theory guys to comment on whether this kind of thing is preferable to dependent typing? I mean, assuming they are equal in power, which is "better"? Or is there no way to make such a distinction?

By Jeff Cutsinger at Tue, 2005-07-26 11:57 | login or register to post comments

Full vs restricted dependent types

The main advantage of this sort of restricted dependent types seems to be the ease of adding them into other languages, particularly languages with side-effects. In traditional full dependent type systems, all terms are pure and terminating, so type equality is decidable. Its not clear how to statically check full dependent types in the presence of side-effects.

The approach taken in Omega is essentially the approach that was taken in DML, and further developed in ATS. In fact there is a paper similar to this one in the upcoming ICFP. It is a bit less accessible and more technical, but also further developed. For example they use constraint solving and metrics to guarentee coverage and termination for proof terms and they prove that proofs are fully erasable, this is left as future work in the Omega paper.

I would hesitate to say that this method takes care of all uses of dependent types, in fact I highly doubt it. But it is extremely useful and flexible in being able to specify and verify a wide range of important propeties not captured by simpler type systems.

By Kevin Donnelly at Tue, 2005-07-26 14:20 | login or register to post comments