[Haskell-cafe] Haskell.org GSoC

[Wolfgang Jeltsch]

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