Type: bare 'Quotation' in signatures is silently treated as type variable, not quotation type #266

Closed
opened 2026-01-16 05:16:50 +00:00 by navicore · 2 comments
navicore commented 2026-01-16 05:16:50 +00:00 (Migrated from github.com)

Summary

Writing Quotation in a type signature is silently parsed as a type variable (Type::Var("Quotation")), not as an actual quotation type. This leads to confusing behavior where Quotation unifies with any type.

Example

: apply-twice ( Int Quotation -- Int )
    2 times
;

Here Quotation looks like it means "a quotation type" but is actually treated as a generic type variable (like T or Foo). It will unify with Int, String, or anything else.

Root Cause

In crates/compiler/src/parser.rs, parse_type() treats any uppercase identifier as a type variable:

if first_char.is_uppercase() {
    Ok(Type::Var(token.text.to_string()))

There's no special handling for Quotation as a reserved type name.

The Design Problem

The type system has Type::Quotation(Box<Effect>) which always requires an explicit effect. There's no way to express "any quotation" without specifying its stack effect. This creates a gap where users naturally write Quotation expecting it to mean "some quotation" but it means something completely different.

Proposed Solutions

Option A: Make Quotation a reserved type meaning [ ..rest -- ..rest ]

This would mean "any quotation that preserves the stack" - essentially polymorphic over effect. Simple but may be too restrictive.

Option B: Reject Quotation as a type variable with a helpful error

Error: 'Quotation' is not a valid type. Did you mean a quotation type like [Int -- Int]?

This forces users to be explicit about the expected effect.

Option C: Add proper existential quantification for quotation effects

Allow something like [ ..? -- ..? ] meaning "some unknown effect" that gets inferred. More complex but more powerful.

Recommendation

Option B (reject with error) is the safest short-term fix. It prevents silent misuse and guides users to the correct syntax. Option C could be considered for future enhancement.

## Summary Writing `Quotation` in a type signature is silently parsed as a type variable (`Type::Var("Quotation")`), not as an actual quotation type. This leads to confusing behavior where `Quotation` unifies with any type. ## Example ```seq : apply-twice ( Int Quotation -- Int ) 2 times ; ``` Here `Quotation` looks like it means "a quotation type" but is actually treated as a generic type variable (like `T` or `Foo`). It will unify with `Int`, `String`, or anything else. ## Root Cause In `crates/compiler/src/parser.rs`, `parse_type()` treats any uppercase identifier as a type variable: ```rust if first_char.is_uppercase() { Ok(Type::Var(token.text.to_string())) ``` There's no special handling for `Quotation` as a reserved type name. ## The Design Problem The type system has `Type::Quotation(Box<Effect>)` which always requires an explicit effect. There's no way to express "any quotation" without specifying its stack effect. This creates a gap where users naturally write `Quotation` expecting it to mean "some quotation" but it means something completely different. ## Proposed Solutions ### Option A: Make `Quotation` a reserved type meaning `[ ..rest -- ..rest ]` This would mean "any quotation that preserves the stack" - essentially polymorphic over effect. Simple but may be too restrictive. ### Option B: Reject `Quotation` as a type variable with a helpful error ``` Error: 'Quotation' is not a valid type. Did you mean a quotation type like [Int -- Int]? ``` This forces users to be explicit about the expected effect. ### Option C: Add proper existential quantification for quotation effects Allow something like `[ ..? -- ..? ]` meaning "some unknown effect" that gets inferred. More complex but more powerful. ## Recommendation Option B (reject with error) is the safest short-term fix. It prevents silent misuse and guides users to the correct syntax. Option C could be considered for future enhancement.
navicore commented 2026-01-16 05:18:59 +00:00 (Migrated from github.com)

After discussion: Option C (existential quantification) is unnecessary. Without generics, an "any effect" quotation type would be useless - you couldn't propagate the unknown effect through type signatures, so you couldn't safely call the quotation.

The fix is simply Option B: reject Quotation as a type variable name with a helpful error message pointing to the explicit [... -- ...] syntax.

If you're accepting a quotation, you need to know its effect to use it.

After discussion: Option C (existential quantification) is unnecessary. Without generics, an "any effect" quotation type would be useless - you couldn't propagate the unknown effect through type signatures, so you couldn't safely call the quotation. The fix is simply Option B: reject `Quotation` as a type variable name with a helpful error message pointing to the explicit `[... -- ...]` syntax. If you're accepting a quotation, you need to know its effect to use it.
navicore commented 2026-01-16 05:37:28 +00:00 (Migrated from github.com)
https://github.com/navicore/patch-seq/pull/267
Sign in to join this conversation.
No milestone
No project
No assignees
1 participant
Notifications
Due date
The due date is invalid or out of range. Please use the format "yyyy-mm-dd".

No due date set.

Dependencies

No dependencies set.

Reference
navicore/patch-seq#266
No description provided.