Draft
Conversation
Add docs/bs/pi_types.md covering the design for dependent function types (Pi) and lambdas at the meta level: motivation, syntax (fn(x: A) -> B for types, |x: A| body for lambdas), typing rules, core IR refactoring (App/Head → PrimApp + Global + FunApp), evaluator closures, and staging interaction. Update docs/SYNTAX.md with function type syntax, lambda syntax, and revised EBNF grammar. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
15 test programs exercising dependent function types and lambdas: - Positive: pi_basic, pi_lambda_arg, pi_polymorphic_id, pi_const, pi_compose, pi_polycompose, pi_nested, pi_dependent_ret, pi_repeat, pi_staging_hof - Error: pi_apply_non_fn, pi_lambda_type_mismatch, pi_lambda_in_object, pi_arity_mismatch, pi_lambda_missing_annotation Snapshot outputs will be generated once the implementation lands. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
- Fix lambda param type parsing: use parse_atom_owned() instead of parse_expr() so the closing | is not consumed as BitOr - Support postfix call syntax expr(args) in the expression parser - Unify FunName::Name(Name) into FunName::Term(&Term) so named calls are a special case of expression calls - Fix wildcard_enum_match_arm clippy lints in checker and pretty printer - Fix match_same_arms for Pi/Lift/U all inhabiting TYPE - Fix MetaVal variant name mismatches in eval (VLit/VCode/VTy/VClosure → Lit/Code/Ty/Closure) - Update and add snapshots for pi_compose, pi_const, pi_lambda_arg, pi_repeat, pi_staging_hof, and others Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
Introduce a local `eval_bump` arena for temporary allocations during staging (synthetic Lam wrappers for global closures). `Term` is covariant, so `'core` data coerces to the shorter `'eval` lifetime. - `MetaVal<'out, 'eval>` / `Binding` / `Env`: two lifetimes; `Closure.body` is `&'eval Term<'eval>`, covering both input terms and eval-arena allocs - All internal eval functions gain `eval_arena: &'eval Bump` - `unstage_program<'out, 'core>`: two lifetimes restored; `core_program` may be dropped once the function returns - `cli/main.rs`: restore separate `core_arena` / `out_arena` Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
Replace the two separate application nodes with a single `App { func,
args }` where `func` is any `Term` — `Term::Prim(p)` for primitives,
`Term::Global(name)` for top-level calls, etc. Empty args now
distinguishes `f()` from a bare `f` reference. No implicit currying in
the core IR; the typechecker checks arity explicitly.
Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
The lint is too aggressive when wildcards are used for non-exhaustive dispatch (e.g. inner match on App callee kind). Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
iljakuklic
commented
Mar 25, 2026
Anonymous parameters like fn(u64) are not valid — the parser requires at least a wildcard: fn(_: u64). Update all examples accordingly. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
iljakuklic
commented
Mar 26, 2026
Owner
Author
There was a problem hiding this comment.
Can we also have a version of this test where apply_twice is polymorphic in the value type?
| @@ -0,0 +1,4 @@ | |||
| // ERROR: too many arguments to a function-typed variable | |||
| fn apply(f: fn(_: u64) -> u64, x: u64) -> u64 { | |||
| f(x, x) | |||
Owner
Author
There was a problem hiding this comment.
Let's also add an opposite test case: passing one arg to a two-arg function.
Comment on lines
+1091
to
+1094
| ensure!( | ||
| !params.is_empty(), | ||
| "lambda must have at least one parameter" | ||
| ); |
Owner
Author
There was a problem hiding this comment.
It should be allowed for a lambda to have empty param list.
- pretty: print argument names in function types (fn(_: u64) -> u64) - pretty: suppress @lvl suffix on wildcard binders - subst: remove redundant doc comment lines - test: fix pi_polycompose input (use capped match instead of implicit cast) - test: add pi_arity_mismatch_too_few (one arg to two-arg function) - test: add pi_nested_polymorphic (apply_twice polymorphic in value type) - docs: update SYNTAX.md — wildcard name required, no binder-free form - docs: update bs/pi_types.md — no binder-free form, variables required, multi-param Pi not desugared (arity preserved) Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
No description provided.