AW: [Haskell-cafe] Haskell.org GSoC

[Wolfgang Jeltsch]

Am Freitag, 20. Februar 2009 09:42 schrieben Sie:
> 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.

I might not really understand you. Do you mean the compiler should be able to 
infer the specification from the implementation? In a dependently-typed 
programming language this would just mean type inference since specifications 
are types. However, type inference isn’t possible for dependent type systems.

Personally, I think, it makes more sense to start with a specification (type)  
and then provide implementations. Systems like Agda and Epigram can actually 
use the reach information from the types to assist you in writing your 
implementation.

Best wishes,
Wolfgang