Skip to content
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
40 changes: 40 additions & 0 deletions .github/workflows/typedpython.yml
Original file line number Diff line number Diff line change
@@ -0,0 +1,40 @@
name: TypedPython CI

# The TypedPython gate and compiler are Python (python-multiplatform-ksp/src/{main,test}/python).
# Gradle does not run them; this workflow does.
on:
push:
branches: [ "develop", "main" ]
paths: [ "python-multiplatform-ksp/**", ".github/workflows/typedpython.yml" ]
pull_request:
branches: [ "develop", "main" ]
paths: [ "python-multiplatform-ksp/**", ".github/workflows/typedpython.yml" ]

jobs:
test:
name: TypedPython tests (${{ matrix.os }})
runs-on: ${{ matrix.os }}
strategy:
fail-fast: false
matrix:
os: [ubuntu-latest, macos-latest]
defaults:
run:
working-directory: python-multiplatform-ksp
steps:
- uses: actions/checkout@v4

- uses: astral-sh/setup-uv@v5

- name: Create the environment
# pyrefly is pinned exactly: the gate reads its versioned type-report format.
run: |
uv venv .venv --python 3.13
uv pip install --python .venv/bin/python "pyrefly==1.3.2" pytest "cython>=3.1" setuptools

- name: Behaviour tests
run: .venv/bin/python -m pytest -q -m "not measurement"

- name: Measurements (recorded, sanity bounds only)
# A shared runner is not an idle machine (AGENTS.md §8): read ratios, not absolute times.
run: .venv/bin/python -m pytest -q -s -m measurement
19 changes: 18 additions & 1 deletion docs/INTENT.md
Original file line number Diff line number Diff line change
Expand Up @@ -26,6 +26,23 @@ CPython interpreter inside a Kotlin Multiplatform application so that:
written (`Greeter('Kotlin').greet(2)` in `sample/`).
3. **The same code runs on every target** a Kotlin Multiplatform app ships to: desktop JVM, Android,
iOS, Android native, and the web (wasm, experimental).
4. **The project's own Python is statically typed by default** (TypedPython). The maintainer's goal:

> "파이썬을 컴파일 언어 및 타입 안정화, 정적 타입 검사, 컴파일 타임 타입검사를 지원할 수 있도록"
> — *Support Python as a compiled language with type stability, static type checking and
> compile-time type checking*, so that Python stays usable as AI-friendly languages such as Rust
> and TypeScript gain ground.

> "TypedPython을 별도 레포가 아니라 PythonMultiplatform의 기본 동작이 될거야"
> — *TypedPython is not a separate repository; it will be PythonMultiplatform's default behaviour.*

The maintainer chose the scope "검사만 기본, 컴파일은 opt-in" (2026-10-02): every user Python source
is **checked** by default; **compiling** it to native code is opt-in. The compiled code still runs on
the embedded CPython, as an extension module (`docs/design/typedpython.md`).

> The maintainer also asked to *explore* GPU kernels written in Python without a separate language
> ("GPU 관련 최적화까지도 별도 언어 없이 지원할 방안을 모색해보자"). That is an exploration, not yet
> a commitment; it is recorded in the design note only.

The CPython version moved on from 3.13 (the build pins 3.14.x today and offers opt-in free-threaded 3.14t builds
on desktop only); the intent — embed **CPython itself**, not a re-implementation — is unchanged.
Expand Down Expand Up @@ -88,7 +105,7 @@ no per-platform Python → Kotlin binding code to maintain.
| A replacement for the `pythonx` packages | §2.3 — they are real packages in their own repository |
| Runtime-reflection or name-lookup based binding | §2.1 — impossible under Kotlin/Native and native image |
| A hand-written wrapper per Kotlin function or class | Generic adaptation plus generated tables; per-declaration wrappers were tried in 2024 and rotted (`docs/design/pythonx-adapter-design.md`) |
| A Python re-implementation, transpiler, or JVM-hosted Python | It embeds CPython itself, so C extensions keep working |
| A Python re-implementation, transpiler, or JVM-hosted Python | It embeds CPython itself, so C extensions keep working. TypedPython (§1.4) does not change this: checked code is ordinary Python, and compiled code is a CPython extension module, not a translation to another runtime |
| A build tool, dependency resolver or packager | That is pypackpack (the work) and toolchain (the Gradle vocabulary) |
| A sub-interpreter parallelism model | Rejected: extensions that do not declare multi-interpreter support fail to import; parallelism comes from free-threaded CPython |
| A vendored interpreter | The build downloads and verifies CPython per platform |
Expand Down
26 changes: 26 additions & 0 deletions docs/SPEC.md
Original file line number Diff line number Diff line change
Expand Up @@ -239,6 +239,32 @@ All in `PM/commonTest`, so they run wherever the interpreter loads.
- **N-3** Binding Kotlin/Native klib declarations at run time (B-2). `Status: planned`.
- **N-4** Linux and Windows desktop runs in CI (P-2). `Status: planned`.
- **N-5** Native-image upcall verification as an automated test (U-6). `Status: planned`.
- **N-6** TypedPython soundness gate (INTENT §1.4; `docs/design/typedpython.md` §4.2): checking a set of
user Python files reports every Pyrefly type error, the Any-leak kinds (`implicit-any-parameter`,
`unannotated-return`, `unknown-variable-type`, `no-any-return-implicit`, `no-any-return-explicit`,
`explicit-any`) and any user-code expression of type `Any` outside `cast()` (`any-flow`) as errors;
the forbidden list (`eval`/`exec`, computed-name `getattr`/`setattr`/`delattr`, patching an imported
module or a module-level class, rebinding an unannotated name to a different type, and a list/set/dict
display whose inferred element type is a union) as warnings in `checked` mode and errors in
`compiled` mode. Nothing
inside dependencies is reported. `python -m typedpython check` exits 0 / 1 / 2 for clean / errors /
tool failure. `Status: partial` — the gate is asserted by
`python-multiplatform-ksp/src/test/python/` (run with that module's `.venv`); it is **not yet run by the
build** (design §6 step 1b). Rebinding and mixed containers are found by a second Pyrefly pass over a
probed copy (design §6.1), which runs only when a file has a name assigned twice or a container
display; `for` targets and comprehension variables are not probed.
- **N-7** TypedPython compilation (INTENT §1.4; design §4.3 stage 1, #23): `typedpython.compiled` is the
identity in CPython; functions it marks, or every module-level function under a first-line
`# typedpython: compiled`, compile through Cython to a CPython extension **with CPython's results**:
`int` keeps arbitrary precision (C `long long` only behind an entry range check, and in pure functions
with overflow checking that redoes the call interpreted), an argument of a different runtime type
takes the interpreted path, `list[float]` elements are unboxed only when the function cannot make them
non-floats, and `math.sqrt` of a negative still raises `ValueError`. A module that fails the gate in
`compiled` mode is not compiled. `python -m typedpython demo <module> [args]` builds a module, runs its
`main()` interpreted and compiled, and fails unless the output is identical. `Status: partial` —
asserted by `python-multiplatform-ksp/src/test/python/test_compile.py` and `test_cli.py` (CI:
`.github/workflows/typedpython.yml`); desktop only, module-level functions with plain signatures only
(methods, defaults, `*args` compile as untyped Python), no M2 benchmark targets yet.

---

Expand Down
31 changes: 31 additions & 0 deletions docs/design/typedpython.md
Original file line number Diff line number Diff line change
Expand Up @@ -207,6 +207,37 @@ TypedPython 은 그래서 자체 텐서 런타임을 만들지 않고 **torch op
각 단계는 AGENTS.md §5·§14 의 TDD 와 측정 테스트 규정을 따른다. 특히 3 은 경계 비용 감소를, 4 는
upstream 대비 수치 오차를 기준선으로 박아 둔다.

### 6.2 단계 2 (컴파일) 의 현재 상태 (2026-10-03, #23)

- SPEC N-7. 의미 보존 규칙은 `compiler.py` 모듈 독스트링에 있다: `int` 는 진입 범위 검사 뒤에만 C
`long long` 이고, 순수 함수에서는 overflow 검사 후 인터프리터로 다시 실행(승격)한다. 비순수 함수의
`int` 지역 변수는 경계가 C 정수인 `range` 인덱스만 C 정수다. `list[float]` 원소는 함수가 그것을
float 아닌 값으로 바꿀 수 없을 때만 언박싱하고, 진입 시 모든 원소가 정확히 `float` 인지 본다.
- 첫 확인(측정 아님, load 197): 벤치 `nbody.py` 에 모듈 표식을 붙여 `demo` 로 돌리면 출력이 같고 약
4배. 스칼라 루프 단위 테스트는 약 136배(load 109). 리스트 원소가 여전히 PyFloat 이라 저장마다
박싱이 일어난다 — 고정 길이 배열을 C 배열로 내리는 것이 다음 단계다.

### 6.1 단계 1 의 현재 상태 (2026-10-03, #16)

- **위치:** `python-multiplatform-ksp/src/main/python/typedpython/`, 테스트는
`python-multiplatform-ksp/src/test/python/`. 사용자 지시("ksp랑 통합")에 따라 KSP 모듈 안에 둔다.
KSP 프로세서는 Kotlin 심볼만 보고 파이썬 파일 변경으로는 다시 돌지 않으므로, **실행**은 1b 에서
Gradle 태스크가 맡는다 — KSP 모듈은 소스와 배포(jar 리소스)의 자리다.
- **구현된 규칙:** SPEC N-6. Pyrefly 의 `Any` 유출 kind 6개를 에러로 올리고, Pyrefly 의
per-expression 타입 리포트(`--report-pysa`)로 사용자 코드 안의 `Any` 식을 찾는다(`any-flow`).
`cast()` 인자, 버려지는 식 문장의 값, 함수 시그니처 자체는 제외한다.
- **재할당·혼합 컨테이너 (#22):** Pyrefly 1.3.2 는 둘 다 보고하지 않고, 타입 리포트에 대입 대상의
타입이 없다. 대신 이름을 *읽는* 위치의 타입은 기록한다. 그래서 대입문 바로 뒤에 같은 줄로
`; x` 를 붙인 사본을 만들어(줄 번호 불변) 한 번 더 돌리고, 그 위치의 타입으로 판정한다. 두 번
이상 대입되는 이름이나 컨테이너 디스플레이가 있는 파일에서만 돈다. `for` 대상과 컴프리헨션
변수는 아직 탐침하지 않는다.
- **측정:** 1800줄 합성 모듈에서 plain `pyrefly check` 160–235 ms, 게이트 1.3–1.9 s — 두 번 잰 비율이
모두 약 8배다. 탐침 패스가 붙은 뒤로는 약 15배(232 ms → 3.6 s, load 41)다 — 합성 모듈의
`total += ...` 가 탐침 대상이라 두 번째 실행이 돈다. 단독 측정이 아니다(두 번째는 load average 18.6). 절대값보다 비율을 기준으로 본다. 차이의
대부분은 타입 리포트가 typeshed 사본까지 디스크에 쓰는 비용으로 보인다(추정, 미분해). 1b 에서
빌드마다 돌리기 전에 줄일 대상이다.
- **고정:** Pyrefly `==1.3.2`. 타입 리포트는 Pyrefly 가 버전을 매기는 포맷이지 공개 API 가 아니다.

## 7. 위험

- **Pyrefly 의 외부 API 안정성.** 라이브러리 임베드는 확인 전까지 미룬다 (§4.1).
Expand Down
5 changes: 5 additions & 0 deletions python-multiplatform-ksp/.gitignore
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
.venv/
__pycache__/
.pytest_cache/
*.egg-info/
.pytest_tmp/
31 changes: 31 additions & 0 deletions python-multiplatform-ksp/pyproject.toml
Original file line number Diff line number Diff line change
@@ -0,0 +1,31 @@
# TypedPython soundness gate (docs/design/typedpython.md §4.2).
# The Kotlin processor in this module is built by Gradle; this file only describes the Python
# package that lives next to it in src/main/python.
[project]
name = "typedpython"
version = "0.1.0"
requires-python = ">=3.13"
# Pinned exactly: the gate reads Pyrefly's per-expression type report (--report-pysa), whose
# format is versioned by Pyrefly, not by a public API.
dependencies = ["pyrefly==1.3.2"]

[project.scripts]
typedpython = "typedpython.__main__:cli"

[build-system]
requires = ["hatchling"]
build-backend = "hatchling.build"

[tool.hatch.build.targets.wheel]
packages = ["src/main/python/typedpython"]

[project.optional-dependencies]
test = ["pytest"]
# `typedpython demo` / compiler.compile_module: Cython and a C compiler for the host.
compile = ["cython>=3.1", "setuptools"]

[tool.pytest.ini_options]
testpaths = ["src/test/python"]
pythonpath = ["src/main/python"]
addopts = "--basetemp=.pytest_tmp"
markers = ["measurement: records cost; asserts only sanity bounds"]
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
"""TypedPython — static checking for the Python code of a PythonMultiplatform project.

See docs/design/typedpython.md. This package is the soundness gate (§4.2).
"""


def compiled[T](target: T) -> T:
"""Mark a function or class for native compilation. In CPython it does nothing."""
return target
101 changes: 101 additions & 0 deletions python-multiplatform-ksp/src/main/python/typedpython/__main__.py
Original file line number Diff line number Diff line change
@@ -0,0 +1,101 @@
"""`python -m typedpython check [--mode checked|compiled] [--format text|json] PATHS...`

Exit status: 0 no errors (warnings allowed), 1 errors, 2 the gate itself could not run.
"""
import argparse
import json
import sys
from pathlib import Path

from typedpython import gate
from typedpython.pyrefly import PyreflyError

EXIT_CLEAN, EXIT_ERRORS, EXIT_FAILURE = 0, 1, 2


def main(argv: list[str]) -> int:
parser = argparse.ArgumentParser(prog="typedpython")
commands = parser.add_subparsers(dest="command", required=True)
check = commands.add_parser("check", help="type-check user Python code")
check.add_argument("paths", nargs="+", type=Path)
check.add_argument("--mode", choices=["checked", "compiled"], default="checked")
check.add_argument("--format", choices=["text", "json"], default="text")
check.add_argument("--search-path", action="append", type=Path, default=[],
help="directory to resolve imports from (repeatable)")
demo = commands.add_parser(
"demo", help="compile a module, run its main() interpreted and compiled, and compare",
)
demo.add_argument("module", type=Path)
demo.add_argument("argv", nargs="*", help="sys.argv[1:] for the module's main()")
demo.add_argument("--out", type=Path, default=Path("build/typedpython"),
help="where the extension is built (default: build/typedpython)")
args = parser.parse_args(argv)

if args.command == "demo":
return _demo(args.module, args.argv, args.out)

try:
found = gate.check(args.paths, mode=args.mode, search_paths=args.search_path)
except PyreflyError as e:
print(f"typedpython: {e}", file=sys.stderr)
return EXIT_FAILURE

if args.format == "json":
print(json.dumps([d.to_json() for d in found], indent=2))
else:
for d in found:
print(f"{d.severity.upper()} {d.path}:{d.line}:{d.column}: {d.message} [{d.rule}]")

return EXIT_ERRORS if any(d.severity == "error" for d in found) else EXIT_CLEAN


def _demo(module: Path, module_argv: list[str], out: Path) -> int:
import contextlib
import io
import time

from typedpython import compiler

try:
built = compiler.compile_module(module, out / module.stem)
except (compiler.CompileError, PyreflyError) as e:
print(f"typedpython: {e}", file=sys.stderr)
return EXIT_ERRORS if isinstance(e, compiler.CompileError) else EXIT_FAILURE

def run(load: object) -> tuple[str, float]:
mod = load() # type: ignore[operator]
saved = sys.argv
sys.argv = [str(module), *module_argv]
out_text = io.StringIO()
try:
with contextlib.redirect_stdout(out_text):
start = time.perf_counter()
mod.main()
elapsed = time.perf_counter() - start
finally:
sys.argv = saved
return out_text.getvalue(), elapsed

interpreted, t_i = run(built.load_interpreted)
compiled, t_c = run(built.load)
print(f"compiled {module.name} -> {built.extension.name}")
print(f"typed functions: {', '.join(built.typed_functions) or '(none)'}")
print(f"interpreted: {t_i * 1000:.1f} ms compiled: {t_c * 1000:.1f} ms "
f"speedup {t_i / t_c:.1f}x")
if interpreted != compiled:
print("output differs:")
print(f" interpreted: {interpreted!r}")
print(f" compiled: {compiled!r}")
return EXIT_ERRORS
print("identical output:")
print(compiled, end="")
return EXIT_CLEAN


def cli() -> None:
"""Console-script entry point (`typedpython check ...`)."""
sys.exit(main(sys.argv[1:]))


if __name__ == "__main__":
cli()
Loading