Home » forums » LtU Forum

FP, auto-generated code..

I read that one of the big things about F.P is the ability to reason about programs/prove them; is there also much more scope for code-generation.. automatically filling in the gaps after manually transforming one part of a system

lets say you have a known datastructure X and some known function F
and you want to transform the datastructure via G, and you want another H function to produce the same result..
F(X) = H(G(X))

my question is, in the functional programming world is there the ability to auto-generate 'H' given 'F' & 'G' (i guess even the ability to verify manually written functions fit the bill would be usefull)

has this sort of thing been used in practice to solve any real word problems, at what level of complexity..

Any pointers for things to read up on along these lines.

By ceti331 at 2009-08-19 13:39 | LtU Forum | previous forum topic | next forum topic | other blogs | 4069 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Halting problem

Note that you can't verify (arbitrary) manually written functions; for example, if G is the identity function, then you are asking for a program to verify that a user-supplied function H is the same as a given function F. (I'm assuming that we are in FP-land here, so that we don't have to worry about side effects and it's clear what it means for two functions to be the same.) If this could be done, then you could solve the halting problem by testing whether

aux_H a = do
    x <- H a
    1

was the same as const return 1.

(I don't know what sorts of things happen if you restrict to a language in which all functions are guaranteed to be total—maybe that would be a reasonable restriction in your setting?)

By L Spice at Wed, 2009-08-19 14:11 | login or register to post comments

Lenses

Sounds a little like Lenses.

By Matt M at Wed, 2009-08-19 14:31 | login or register to post comments

yes this is exactly the sort

yes this is exactly the sort of thing I'm inquiring about. autogenerating playback from Encoders, with the encoding typically re-arranging data for locality & compression.

Thanks for the reference I'll read through that..

I note in the comments a title "how to derive a lzw decompressor from a compressor" :)

I was also going to ask about reversibility - e.g. can one auto generate/verify the INVERSE of some functions.., or maybe there are restrictions on how to express functions that are garanteed to be invertible.

By ceti331 at Wed, 2009-08-19 14:48 | login or register to post comments

i can post a second related

i can post a second related question,
"what language would be best to experiment with this sort of thing"
with the restriction that one would need to be able to translate it into C/C++

By ceti331 at Wed, 2009-08-19 15:11 | login or register to post comments