[mercury-users] Dependent Types

[Fergus Henderson]

On 22-Feb-2000, Stefan Karrmann <sk at mathematik.uni-ulm.de> wrote:
> There is an interesting extension of Haskell by Lennart Augustsson.
> It is Cayenne (see http://www.cs.chalmers.se/~augustss/cayenne/index.html)
> which uses dependent types. This increases the power of functions,

It certainly increases the power of the static type system.
But note that if you already have optional dynamic typing, as Mercury
does, then it doesn't increase the language's expressiveness, it just
increases the fraction which can be statically checked.

> Can Mercury be extended in a similar way? How would it look like?

Yes, Mercury could probably be extended in a similar way.  It would like
quite analagous to Cayenne.  But I'm not sure that complicating the type
system in that way is worth it. 

One technical problem is that in Mercury, unlike Cayenne, it probably
wouldn't be easy for the compiler to avoid constructing and passing
around types at run-time.

If you're interested in the topic, I suggest you check the
archives of the Haskell mailing list.  There was a long discussion
on dependent types on that list in Febuary 1999, during which I think
I made my views pretty clear.

Type systems are a good way of expressing and reasoning about certain
fairly simple kinds of properties.  But once you start trying to express
more complicated properties, then IMHO things start to get rather
difficult.  In Cayenne, if you want to express some complex logical
property which the arguments to a function should satisfy, then you need
to express it as a type, by using the Curry-Howard isomorphism to map
logical properties to types and proofs to terms.  To me, it seems
clear that it would be more natural for programmers to express
such properties directly in predicate logic rather than via a
relatively complicated encoding as types.

So rather than adding support for dependent types, what we have been
looking at is adding support for admissability constraints (which roughly
correspond to preconditions in Eiffel) and other kinds of assertions
(e.g. success set constraints, which roughly correspond to postconditions),
with the long term plan of trying to use a combination of
(a) runtime checking, to check (some of) them at runtime,
and/or (b) automated and/or programmer-assisted otheorem-proving
techniques, to prove them.

Our ideas for adding support for admissability constraints and other kinds
of assertions have been discussed quite a bit on the mercury-developers
mailing list, so if you're interested you may want to check the archive
for that list, which is available via our web site.

-- 
Fergus Henderson <fjh at cs.mu.oz.au>  |  "I have always known that the pursuit
WWW: <http://www.cs.mu.oz.au/~fjh>  |  of excellence is a lethal habit"
PGP: finger fjh at 128.250.37.3        |     -- the last words of T. S. Garp.
--------------------------------------------------------------------------
mercury-users mailing list
post:  mercury-users at cs.mu.oz.au
administrative address: owner-mercury-users at cs.mu.oz.au
unsubscribe: Address: mercury-users-request at cs.mu.oz.au Message: unsubscribe
subscribe:   Address: mercury-users-request at cs.mu.oz.au Message: subscribe
--------------------------------------------------------------------------