AW: [Haskell-cafe] GSoC

Wolfgang Jeltsch g9ks157k at
Fri Feb 20 05:09:42 EST 2009

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 

Best wishes,

More information about the Haskell-Cafe mailing list