Concern on the size of normalized code, compiling complexity.

Gabriella439 / Haskell-Morte-Library

A bare-bones calculus-of-constructions

BSD 3-Clause "New" or "Revised" License

372 stars 25 forks source link

Concern on the size of normalized code, compiling complexity. #52

Open TorosFanny opened 7 years ago

TorosFanny commented 7 years ago

I'm not quite familiar with compiling theory, category theory and many other related topics. But I'm very interested in all of them. Within my limited knowledge, I'm concerned about two things.

I think the normalized code's would be unnecessarily big when, for example, it de-sugaring a program which has a constant number as a recursion time.
When the source code contains a constant which needs O(2^n) time to compute, the compiling time will be at least O(2^n).

How can you handle these two problems, if I'm not asking stupid questions? Thank you for your attention.

VictorTaelin commented 7 years ago

If I understand your question, yes. Imagine, for example, the following program:

add_100000_times :: Nat -> Nat
add_100000_times = sum . replicate 100000

Compiling that program on Morte would generate a huge normal form. My approach to this problem is to simply lift those constants out of the program, i.e.,

add_n_times :: Nat -> Nat -> Nat
add_n_times n = sum . replicate n

This way, you postpone the expansion to the runtime on your target language. I have not, so far, found an instance where this wasn't practical. What example do you have in mind?

TorosFanny commented 7 years ago

Yes, that's a good idea.

TorosFanny commented 7 years ago

Then, do you think Morte can transform a slow algorithm into a faster one? Do you think algorithm design is still needed?

Gabriella439 commented 7 years ago

@TorosFanny So I think if Morte were backed by something like Lamping's abstract algorithm for normalization it could in many cases transform a slow algorithm into a faster one in terms of time complexity. I would need some more specific examples to say anything more definitive than that, though

TorosFanny commented 7 years ago

For a very simple example transform \x -> \y -> (x + y) - x to \_ -> \y -> y. As Morte can't prove addition commutes, I think maybe Morte can't do that transform as well

Gabriella439 commented 7 years ago

@TorosFanny You're right. Morte can't really handle substraction

VictorTaelin commented 7 years ago

I'd love to understand why this is the case, in a deeper sense...