AW: [Haskell-cafe] Haskell.org GSoC

[Kemps-Benedix Torsten]

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: haskell-cafe-bounces at haskell.org [mailto:haskell-cafe-bounces at haskell.org] Im Auftrag von Wolfgang Jeltsch
Gesendet: Donnerstag, 19. Februar 2009 14:22
An: haskell-cafe at haskell.org
Betreff: Re: [Haskell-cafe] Haskell.org GSoC

Am Donnerstag, 19. Februar 2009 11:35 schrieb Alberto G. Corona:
> 2009/2/19 Wolfgang Jeltsch <g9ks157k at acme.softbase.org>
>
> > 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
Haskell-Cafe at haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe