Another typing question

[Jon Cast]

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

<snip>

> > 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.

<snip>

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

> What negative consequences does their implementation have?

It depends on whether you just want to write functions to take in values
of such types, or whether you want to write functions to return values
of such types.  Doing the former uses dependant products, which would
require a significant extension to GHC's guts, but not (AIUI) inherently
unpleasant.  Doing the latter (AIUI) essentially requires dependant
sums.  Basically, a family of types A_i parameterized by a value i :: I
is written, for long-honored traditional reasons too complex to get into
here, Sigma i::I.A_i.  Now, if you have such dependant sums, there's a
bad interaction with polymorphism: either you must have a type alpha
which cannot appear in a family of types A_i in a dependant sum, or, for
any function f :: alpha -> alpha, there exists a type beta such that f
cannot be aplied at either beta or Sigma i::Int.beta.  Clear?

The alternative, btw., is to have both dependant sums and an undecidable
type-checking problem.

> I think, sometimes they could be quite handy.

Sure.  <Sarcastic comment censored>.

Jon Cast