Could abstract algorithm use information from type system to improve evaluation?

[Kesanov]

Lets take fusion as an example:

1. this fuses

   @List.fmap #f /Y #fmap #xs #c #n
     //xs
       #x #xs //c /f x /fmap xs
       n

2. this does not

   @List.map #f /Y #map #xs
     //xs
       #x #xs #c #n //c /f x /map xs
       #c #n n

Obviously it is not possible to transform map to fmap, unless we know that xs is well behaved. (Bad behaved xs would be for example #con #nil #x x.)

---

Now comes the tough question? How do we know xs is well behaved?

• In pure lambda calculus it's impossible. You have to do it by hand.
• Adding annotations or constructors is interesting middle ground. For example Haskell has ADT and pattern matching which allows this particular transformation.
• Type system (the more powerful the better) is the general solution. Since nobody has done it (AFAIK), it won't be trivial.

Can it be done?

[Kesanov]

To make the task simpler you might think of annotating each argument with set of all possible input values:

@N        #c #n n
@C #x #xs #c #n //c x xs

@List.map 
  #(f : Any) 
  /Y #(map: List.map)
     #(xs: N | C Any List)
      //xs
        ...

The naive solution would be then to evaluate map with all possible arguments (we have them listed in the annotations):

@List.map #f /Y #map #xs
    #c #n n

@List.map #f /Y #map #xs
    #c #n //c /Any Any /List.map List

now it is obvious map always returns lambda starting with #c #n ... therefore map == fmap.

---

This approach has sadly exponential complexity, does not involve interaction nets and is quite ad hoc.

But nevertheless it is an evidence for using type system to further improve the evaluation is possible.

[VictorTaelin]

Do you have any paper describing a type system like that one you described? I don't think i've seen a type system which works by simply listing all possible values of its inputs, looks interesting.

[VictorTaelin]

But anyway, before answering that question, I think we must understand exactly when and why fusion happens, it is not as simple as that. Some terms require slightly different strategies. All in all it is still very new and unpredictable to me.

[Kesanov]

Do you have any paper describing a type system like that one you described? I don't think i've seen a type system which works by simply listing all possible values of its inputs, looks interesting.

No, it is just an experiment. But it could be emulated by doing runtime checks for equality on each function application which is not very efficient, but some languages do it (e.g. python).

[Kesanov]

Then we should at least make a file, where we put all before => after transformations, which allowed fusion, so we can make some sense of it.

[Kesanov]

For example I still do not understand, why does fmap require identity to not loop forever. Do you have any explanation for it?

[VictorTaelin]

I agree with a before => after file. And I have no idea too, a graphical evaluator would be handy to understand why.

[Kesanov]

As an example in theorems for free polymorphism is used to derive theorems about terms.