[Haskell-cafe] Haskell.org GSoC
g9ks157k at acme.softbase.org
Thu Feb 19 08:22:27 EST 2009
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
More information about the Haskell-Cafe