Reduce about product fucntion

[kmyk]

Description / 説明

Rewrite rules to convert sum / modsum to closed formulae are already implemented.
For example, an expr sum(sorted(map(lambda x: x + 1, xs))) of Python becomes sum(xs) + len(xs).
Implementation:

https://github.com/kmyk/Jikka/blob/52299f06f7f8d96643198b2cff95fd873da9b371/src/Jikka/Core/Convert/CloseSum.hs#L42-L68

Rewrite rules for product / modproduct are not fully implemented. We want to complete them.
In concrete, please do followings:

• Rewrite existing rules which are written in a old format (hand-written pattern matches), using a new format (quasi-quotes, like [r| "sum/range" forall n. sum (range n) = n * (n - 1) /! 2 |])
• Add lacking rewrite rules

Current implementation:

https://github.com/kmyk/Jikka/blob/52299f06f7f8d96643198b2cff95fd873da9b371/src/Jikka/Core/Convert/CloseSum.hs#L70-L86

Motivation / 動機

because not implemented yet

[soraiemame]

たとえば sum(sorted(map(lambda x: x + 1, xs))) という Python の式が sum(xs) + len(xs) になったりする。

とのことですが、実際に実行してみたところ、エラーが出ます。
実行したコード

def solve(xs: List[int]) -> int:
    return sum(sorted(map(lambda x: x + 1, xs)))

発生したエラー

Internal Error (implementation's bug?): Jikka.Core.Convert.TypeInfer: failed to solve type equations: failed to unify $43 and int list: different type ctors int and 
int list

これはコードが間違っているのでしょうか？それともシステムの問題なのでしょうか？

[kmyk]

システムの問題です。Jikka の既存の実装がバグっているのだと思います。

Jikka.Core.Convert.TypeInfer は core 言語上で型推論 (type inference) をする module です。
Python 上での型推論をした後に、core 言語に変換し、そこでもう一度型推論をするのですが、このときにエラーが出ているということになります。
なので実行したコードは合っています。

呼び出し元:

https://github.com/kmyk/Jikka/blob/aafa681e666dfb306702f8902acf6473a5b58d22/src/Jikka/Main/Subcommand/Convert.hs#L58-L60

https://github.com/kmyk/Jikka/blob/aafa681e666dfb306702f8902acf6473a5b58d22/src/Jikka/Core/Convert.hs#L81-L84

エラーが failed to unify $43 and int list: different type ctors int and int list なので「型変数 $43 (値は型 int) のところで int list が使われていてなにかがおかしいぞ」と言っています。
Python から core 言語に変換するところとかにバグがあるんじゃないかなという気がします。

@soraiemame よければこれの調査を任せたいです。どうですか？

[soraiemame]

やってみます！

[kmyk]

@soraiemame とりあえず issue #222 を切っておきました。
ところで型推論 (src/Jikka/Core/Convert/TypeInfer.hs) の側が間違ってる可能性もある (忘れてた、すまん……) のでこちらも疑ってみてほしいです