search

diprism / perpl

The PERPL Compiler
MIT License
10 stars 5 forks source link

Affine-to-linear before de/refunctionalize #71

Closed davidweichiang closed 1 year ago

davidweichiang commented 2 years ago

Closes #54

davidweichiang commented 1 year ago

I think this is working but probably will want to add a few more tests to be sure.

davidweichiang commented 1 year ago

Towards the end of making the compiler able to parse its own -c output, I allowed <> in source code and gave it type AdditiveUnit. Totally open to better ways to write AdditiveUnit.

davidweichiang commented 1 year ago

This is passing all of the new sum-product tests. But it's noticeably slower than before.

davidweichiang commented 1 year ago

"Noticeably slower" = 3.25x slower.

ccshan commented 1 year ago

A trivial comment: AdditiveUnit is usually called Zero.

ccshan commented 1 year ago

A trivial comment: AdditiveUnit is usually called Zero. Correction: Girard calls it $\top$

davidweichiang commented 1 year ago

OK, now this passes all tests and the test that originally motivated this.

davidweichiang commented 1 year ago

@ccshan if you want to approve this instead of @HerbertMcSnout I think that would be fine.

davidweichiang commented 1 year ago

But nonrecursive datatypes are already positive (robust)...why would we want to generate the extra code?

ccshan commented 1 year ago

But nonrecursive datatypes are already positive (robust)...why would we want to generate the extra code?

To clarify, I mostly just thought that it would be nice to not rely on isRecursiveTypeName. Also, some nonrecursive datatypes are nonpositive: data T = MkT (Bool -> Bool)

Just a suggestion...

davidweichiang commented 1 year ago

OK, I see, that saves a lot of code. I pushed a change in master that takes your suggestion, but suppresses generation of the discard function for positive datatypes.