Re: Another typing question

I wrote:

Wolfgang Jeltsch wrote:

...

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?

Actually, on second thought, I think this could be simplified to: if we have dependant types, then either there is a type which cannot be used in a dependant type, or for every polymorphic function there is a type it cannot be applied at. Jon Cast