## 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.

## Comment viewing options

### 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?

### 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.

### 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.

### 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.

### 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).