Another typing question

Wolfgang Jeltsch wolfgang@jeltsch.net
Tue, 5 Aug 2003 15:30:44 +0200


On Tuesday, 2003-08-05, 15:22, CEST, Nick Name wrote:
> [...]

> > Is there any way to parametrize a type by a value, rather than another
> > type? What I would like to do is to define "list of length 3" and "list of
> > length 4" as separate parametrization of the same type, such that I could
> > write functions that accept lists (under my new typename) of any length as
> > long as parameters have the same length. The goal is to remove the need
> > for runtime checks all over the code.
>
> This is called "dependent types" and is not a feature of haskell (nor of any
> language that I know); there was "cayenne" (try a google search) but I don't
> believe it is still mantained.

Well, there are, e.g., Ada and C++ which allow types to be parametrized by 
values. The point is that they obviously still use runtime checks, it's just 
that you don't have to code these checks explicitely.

> BTW, why is there no general interest for such a thing as dependent types?

What negative consequences does their implementation have? I think, sometimes 
they could be quite handy.

> V.

W. ;-)