I wrote: > Wolfgang Jeltsch <[EMAIL PROTECTED]> 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 _______________________________________________ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
