Another typing question

[Jon Cast]

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