如何在从Idris调用Python时不使用逗号构造元组？

直接使用无逗号的Python lambda表达式 lambda *args: args，它会接收任意数量的参数并自动打包为对应长度的元组，完全适配Idris的%foreign字符串要求（无逗号）。

示例代码（Idris中定义） #

-- 生成二元组
%foreign "python:lambda *args: args"
makePair : PythonClass -> PythonClass -> PythonClass

-- 生成三元组（按需扩展参数数量即可）
%foreign "python:lambda *args: args"
makeTriple : PythonClass -> PythonClass -> PythonClass -> PythonClass

使用方式 #

调用时传入固定数量的参数，Idris的类型系统会保证参数数量匹配，最终返回对应的Python元组：

• makePair 1 2 对应Python元组 (1, 2)
• makeTriple 3 4 5 对应Python元组 (3, 4, 5)

原理说明 #

这个lambda利用Python的可变参数语法*args，所有传入的参数会被自动打包成元组args，整个表达式中没有任何逗号，完美规避Idris Python后端对逗号的特殊处理逻辑，且无需额外编写Python模块，代码量极少。

内容的提问来源于stack exchange，提问作者joel