Home » forums » LtU Forum

Defunctionalization+Refunctionalization+Expression Problem

Interesting paper which suggests you can solve the expression problem by defunctionalizing, converting data to codata and refunctionalizing (and vice versa). Suggests that the function type is a special case of codata with a single destructor.

By chrisoliver at 2018-01-25 22:14 | LtU Forum | previous forum topic | next forum topic | other blogs | 3921 reads

Comment viewing options

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

Why not just pattern match against the symbol of a function?

I have no idea why a functional language couldn't just pattern match against the symbol/name of a function? The Egel language does that without a problem. I.e., the following just works^tm.

[ Math.sqrt -> "square root" ] Math.sqrt = "square root"

Also, the paper doesn't spell out how they want to tackle the expression problem so, uhm, what is their proposal?

By marco at Fri, 2018-01-26 03:06 | login or register to post comments

IDE

As I understand it, the suggestion was that you have an IDE where you push a button to show the codata view when you want to add a variant and toggle to the data view when you want to add an operation - thus maintaining modularity.

By chrisoliver at Fri, 2018-01-26 16:01 | login or register to post comments

This breaks alpha-equivalence

I have no idea why a functional language couldn't just pattern match against the symbol/name of a function?

If you can branch on the name of a function, then renaming a function can change the behaviour of a program. This defeats most optimizations. For example, whether you generated a specialized version of a function for when some of its arguments were known statically becomes detectable.

If you mean this Egel language, it uses an interpreter which basically doesn't do optimizations, so this matter less for it.

By neelk at Tue, 2018-01-30 11:36 | login or register to post comments

Yah

That's a lovely little language! Sure, I agree with your observation but, of course, some languages might be designed along the line that it is a sensible position. For example, I doubt a tool like Wolfram Alpha could be built without it.

By marco at Fri, 2018-02-02 04:24 | login or register to post comments

Function type is negative

Suggests that the function type is a special case of codata with a single destructor.

Yes, I believe this is well-understood now by type-system people. Functions are just one *negative* type among others (such as lazy pairs), as is apparent for example in call-by-push-value (CBPV) and abstract machine calculi based on mu-multida. (I think I first learned about it from a popularization presentation on Curien-Herbelin's mu-mutilda made by Michael Adams in 2012).

By gasche at Tue, 2018-01-30 13:38 | login or register to post comments