Lennart Augustsson <[EMAIL PROTECTED]> writes:
> Let me just point out that my main interest in dependent types is
> NOT to do specifications and proofs (like sort above), but to
> make the type system more expressible. This way we can make more
> programs typeable, and also give more accurate types to programs.
> The latter is well illustrated in a paper by Hongwei Xi and Frank
> Pfenning in POPL99.
BTW, I am interested in dependent types for specifications and proofs.
Thanks for mentioning the Xi and Pfenning paper; highly recommended.
They describe a language with dependent types (DML(C)) which is very
different from Cayenne; it is both much stronger and much weaker.
1) The type language of DML(C) is much weaker than Cayenne's. DML(C)
is an extension of ML; all its types are subtypes of regular ML types.
(You can convert DML(C) programs to standard ML by erasing the
dependent type bits.) Cayenne, of course, can express much more
complicated (and interesting) types.
2) The type checking of DML(C) is much stronger than Cayenne's. Their
implementation can automatically verify many program properties which
would, I believe, be quite tedious to verify in Cayenne. (For
instance, DML(C) can automatically verify that a sorting function
returns a list of the same length as its input. I believe that a
similar verification in Cayenne would start with a formalization of
the natural numbers, proofs of many basic properties of the naturals,
and some annoying manipulations of these proofs in order to verify the
sorting function.) (I may be wrong about the difficulty of the
Cayenne verification; I'm ashamed to confess that I still have not
written any Cayenne programs.)
I want the best of all these worlds. I want a programming language
whose type system is as strong as Cayenne's. For parts of the program
without explicit type declarations, I want types to be inferred (using
Hindley-Milner). For parts of the program with explicit type
declarations, I want types to be checked with powerful, yet efficient
inference engines (as in DML(C)). For parts of the program where the
system cannot automatically verify type correctness, I want to be able
to give my own proofs.
In fact, I'm in the middle of the design and implementation of such a
language. I've been working on it since about 1992 (off and on, in my
spare time); at the current rate of progress, I expect to have
something releasable in another 30 years or so. (Don't hold your
breath, in other words.) I hope somebody else will beat me to it.
Carl Witty
[EMAIL PROTECTED]
