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 _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
