prelude: input builtin

DESIGN.md

@@ -601,8 +601,13 @@ mechanism needed **no parser change**: `Module.member` is parsed as the ordinary
 `Field { base: Var("List"), name: "map" }`; `types::qualified_name` recognizes an **uppercase** base
 (value identifiers are lowercase, so `Upper.x` is only ever module access — a record-field base is a
 lowercase value), and the checker + lowering resolve the dotted member against the module instead of as
-record-field access. A genuinely global handful stay unqualified (`print`/`abs`/`min`/`max` in
-`PRELUDE`), matching F# (`List.map` qualified, `abs` global). An unknown member gets a **"did you
+record-field access. A genuinely global handful stay unqualified (`print`/`input`/`abs`/`min`/`max` in
+`PRELUDE`), matching F# (`List.map` qualified, `abs` global). `input : string ->{io} string` is
+Python's `input(prompt)` name-for-name (`input ""` for promptless) — the io effect coming *in*,
+pairing with `print`'s going out; `input "n? " |> String.toInt : Option int` is the idiomatic total
+parse. Environment caveats: the REPL's worker protocol runs over stdin, so `input` inside the REPL
+consumes protocol bytes (the documented stdin hazard), and the Pyodide playground cannot block on
+stdin — scripts via `pyfun run` (and Jupyter, whose kernel routes stdin) are its home turf. An unknown member gets a **"did you
 mean"** hint — `` `startswith` is not a member of `String` (did you mean `String.startsWith`?) `` —
 computed by `closest_member` (a case-insensitive match first, then edit distance ≤ ~⅓ the name, then a
 prefix relation for abbreviation slips like `length`→`len`). It scans the env's qualified keys, so it

src/types/mod.rs

@@ -348,6 +348,7 @@ const MAX_ORD_DEPTH: usize = 100;
 /// call-site renaming is needed — the simplest honest interop surface.
 pub const PRELUDE: &[(&str, usize)] = &[
     ("print", 1),
+    ("input", 1),
     ("abs", 1),
     ("min", 2),
     ("max", 2),
@@ -2371,7 +2372,7 @@ const RESERVED_VARS: u32 = 5;
 /// and returns `unit`; `abs`/`min`/`max` are polymorphic over the numeric base
 /// (`num`) *and* the unit, i.e. `num 'a => 'a<'u> -> …`.
 fn seed_prelude(env: &mut Env) {
-    // print : 'a ->{io} unit  — the prelude's one effectful builtin.
+    // print : 'a ->{io} unit  — effects going out.
     env.insert(
         "print".to_string(),
         Scheme {
@@ -2384,6 +2385,23 @@ fn seed_prelude(env: &mut Env) {
             ty: Ty::Fun(Box::new(Ty::Var(0)), Box::new(Ty::Unit), Effect::io()),
         },
     );
+    // input : string ->{io} string  — effects coming in: prompt → one line of
+    // stdin, exactly Python's `input(prompt)` (`input ""` for promptless).
+    // Monomorphic and name-for-name like the rest of the prelude. NB the REPL's
+    // worker protocol runs over stdin, so `input` there consumes protocol bytes
+    // (the documented stdin hazard); scripts via `pyfun run` are the home turf.
+    env.insert(
+        "input".to_string(),
+        Scheme {
+            vars: vec![],
+            uvars: vec![],
+            num_vars: vec![],
+            ord_vars: vec![],
+            eff_vars: vec![],
+            mutable: false,
+            ty: Ty::Fun(Box::new(Ty::Str), Box::new(Ty::Str), Effect::io()),
+        },
+    );
     let num_u = || Ty::Num(PRELUDE_NUMVAR, Unit::var(PRELUDE_UVAR));
     let scheme = |ty| Scheme {
         vars: vec![],

tests/compile.rs

@@ -1175,6 +1175,51 @@ fn choose_and_collect_lower_to_helpers() {
     assert!(py.contains("out.extend(f(x))"), "{py}");
 }
 
+#[test]
+fn input_lowers_name_for_name() {
+    let py = pyfun::compile("let name = input \"who? \"\nprint name").unwrap();
+    assert!(py.contains("name = input(\"who? \")"), "{py}");
+}
+
+#[test]
+fn e2e_input_reads_a_line_from_stdin() {
+    let Some(python) = python_cmd() else {
+        eprintln!("skipping end-to-end check: no python interpreter found");
+        return;
+    };
+    let program =
+        pyfun::compile("let name = input \"who? \"\nprint (String.concat \"hi \" name)").unwrap();
+    // `python -` (the run_python helper) reads ALL of stdin as the program, so
+    // write the program to a file and pipe the input line as real stdin.
+    let dir = std::env::temp_dir().join("pyfun_input_e2e");
+    std::fs::create_dir_all(&dir).expect("create temp dir");
+    let path = dir.join("main.py");
+    std::fs::write(&path, &program).expect("write program");
+    let mut child = Command::new(&python)
+        .arg(&path)
+        .stdin(Stdio::piped())
+        .stdout(Stdio::piped())
+        .stderr(Stdio::piped())
+        .spawn()
+        .expect("spawn python");
+    child
+        .stdin
+        .take()
+        .expect("python stdin")
+        .write_all(b"ana\n")
+        .expect("write input line");
+    let output = child.wait_with_output().expect("wait for python");
+    assert!(
+        output.status.success(),
+        "python exited with {}\nstderr:\n{}",
+        output.status,
+        String::from_utf8_lossy(&output.stderr)
+    );
+    let stdout = String::from_utf8_lossy(&output.stdout);
+    // The prompt is echoed to stdout (no tty), then the greeting.
+    assert!(stdout.contains("hi ana"), "{stdout}");
+}
+
 #[test]
 fn e2e_list_choose_and_collect() {
     run_and_check(

tests/roundtrip.rs

@@ -76,6 +76,7 @@ const PROGRAMS: &[&str] = &[
     "let hit = List.find (fun x -> x > 0) xs",
     "let kept = List.choose f xs",
     "let flat = List.collect f xs",
+    "let name = input \"who? \"",
     // `5<m>` (adjacent, in the units section below) is a unit annotation, whereas
     // `5 < m` (spaced) is a comparison — the printer keeps them distinct.
     "let r = 5 < m",

tests/typecheck.rs

@@ -2251,6 +2251,21 @@ fn map_of_an_impure_function_is_impure() {
     );
 }
 
+#[test]
+fn input_is_a_prelude_builtin_with_the_io_effect() {
+    // input : string ->{io} string — Python's input(prompt), name-for-name.
+    assert!(pyfun::check("let ask u = input \"? \"").is_ok());
+    // Composes with the total parse into Option int.
+    assert!(pyfun::check("let n = String.toInt (input \"n? \")").is_ok());
+    // The io effect flows out: a `pure` binding using input is rejected.
+    assert_error_contains(
+        "let pure ask u = input \"? \"",
+        "declared `pure` but performs `io`",
+    );
+    // The prompt is a string.
+    assert_error_contains("let x = input 3", "string");
+}
+
 #[test]
 fn rejects_redefining_builtin_list() {
     assert_error_contains("type List a = Empty | More a", "already defined");