# Another typing question

**Jon Cast
**
jcast@haskell.org

*Tue, 05 Aug 2003 17:39:27 -0500*

I wrote:
>* Wolfgang Jeltsch <wolfgang@jeltsch.net> 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