Hello, but to specify that “this function turns a list into its sorted equivalent” would probably require to specify e.g. "sort" in terms of the type system and to write code that actually does the sorting. The first task is much like specifying what a sorted list is in first-order-logic (much like a Prolog program) and the second task is a regular functional program.
If this is correct, dependent types would become more useful if the first task could be done by the compiler - which is probably impossible in general. Am I right? Best wishes, Torsten -----Ursprüngliche Nachricht----- Von: [email protected] [mailto:[email protected]] Im Auftrag von Wolfgang Jeltsch Gesendet: Donnerstag, 19. Februar 2009 14:22 An: [email protected] Betreff: Re: [Haskell-cafe] Haskell.org GSoC Am Donnerstag, 19. Februar 2009 11:35 schrieb Alberto G. Corona: > 2009/2/19 Wolfgang Jeltsch <[email protected]> > > > Am Donnerstag, 19. Februar 2009 02:22 schrieb sylvain: > > > Haskell is a nice, mature and efficient programming language. > > > By its very nature it could also become a nice executable formal > > > specification language, provided there is tool support. > > > > Wouldn't it be better to achieve the goals you describe with a > > dependently typed programming language? > > But I wonder how a dependent typed language can express certain properties, > for example, the distributive property between the operation + and * in a > ring or simply the fact that show(read x)==x. As far as I understand, a > dependent type system can restrict the set of values for wich a function > apply, but it can not express complex relationships between operations. Each type system corresponds to some constructive logic and can enforce properties which are expressible in that logic. Dependent type systems correspond to higher order predicate logics or so and therefore can express almost everything you want. An Agda or Epigram type can cover a complete behavioral specification like “This function turns a list into its sorted equivalent.” Best wishes, Wolfgang _______________________________________________ Haskell-Cafe mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe
_______________________________________________ Haskell-Cafe mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe
