Polymorphic higher-order functions limited by type system #297

New issue

Closed

opened 2026-01-23 02:03:49 +00:00 by navicore · 1 comment

navicore commented

2026-01-23 02:03:49 +00:00

(Migrated from github.com)

Polymorphic higher-order functions limited by type system

Summary

Seq's type system cannot unify concrete types (like Int, quotations) with Variant when calling higher-order functions. This prevents idiomatic
functional patterns like fold/reduce from being fully generic.

Example

include std:zipper

# Generic fold - compiles fine
: zfold ( Variant Variant Variant -- Variant )
  rot dup znil? if
    drop drop
  else
    dup zhead 4 roll swap 4 roll dup 4 roll swap call swap zfold
  then
;

# Using fold with concrete types - fails to compile
: sum ( ZList -- Int )
  0 [ i.+ ] zfold
;

Error:

  zfold: stack type mismatch. Expected (..rest Variant Variant Variant),
  got (..rest Variant Int [(..a Int Int) -- (..a Int)]):
  Type mismatch: cannot unify [(..a Int Int) -- (..a Int)] with Int

The Gap

Seq has all the building blocks for functional programming:

Quotations and call
Cons lists via std:zipper (znil, zcons, zhead, ztail)
Recursion with verified TCO (1M mutual recursive calls work)

But the type system can't express "this function is polymorphic in the accumulator and element types."

Potential Approaches

Automatic Variant coercion - Allow concrete types to implicitly coerce to Variant at call sites
Type variables in signatures - Something like ( a [a b -- a] List -- a )

Bounded polymorphism - Declare a word as accepting "any type" for certain positions

Untyped/dynamic mode - Relax type checking for HOF contexts (note: this may conflict with Seq's compile-time safety goals)

Current Workaround

Implement concrete recursive functions instead of using generic HOF:

# Works - direct recursion with concrete types : sum-acc ( ZList Int -- Int ) over znil? if nip else over zhead i.+ swap ztail swap sum-acc then ; : sum ( ZList -- Int ) 0 sum-acc ;
This is idiomatic and works well, but requires reimplementing the recursion pattern for each use case rather than abstracting it once.

Context

This came up while creating a functional programming paradigm example (examples/paradigms/functional/lists.seq). The example can be completed with direct
recursion, but generic map/filter/fold would make it more expressive.

# Polymorphic higher-order functions limited by type system ## Summary Seq's type system cannot unify concrete types (like `Int`, quotations) with `Variant` when calling higher-order functions. This prevents idiomatic functional patterns like `fold`/`reduce` from being fully generic. ## Example ```seq include std:zipper # Generic fold - compiles fine : zfold ( Variant Variant Variant -- Variant ) rot dup znil? if drop drop else dup zhead 4 roll swap 4 roll dup 4 roll swap call swap zfold then ; # Using fold with concrete types - fails to compile : sum ( ZList -- Int ) 0 [ i.+ ] zfold ; ``` Error: ``` zfold: stack type mismatch. Expected (..rest Variant Variant Variant), got (..rest Variant Int [(..a Int Int) -- (..a Int)]): Type mismatch: cannot unify [(..a Int Int) -- (..a Int)] with Int ``` The Gap Seq has all the building blocks for functional programming: - Quotations and call - Cons lists via std:zipper (znil, zcons, zhead, ztail) - Recursion with verified TCO (1M mutual recursive calls work) But the type system can't express "this function is polymorphic in the accumulator and element types." Potential Approaches 1. Automatic Variant coercion - Allow concrete types to implicitly coerce to Variant at call sites 2. Type variables in signatures - Something like ( a [a b -- a] List<b> -- a ) 3. Bounded polymorphism - Declare a word as accepting "any type" for certain positions 4. Untyped/dynamic mode - Relax type checking for HOF contexts (note: this may conflict with Seq's compile-time safety goals) Current Workaround Implement concrete recursive functions instead of using generic HOF: ```seq # Works - direct recursion with concrete types : sum-acc ( ZList Int -- Int ) over znil? if nip else over zhead i.+ swap ztail swap sum-acc then ; : sum ( ZList -- Int ) 0 sum-acc ; ``` This is idiomatic and works well, but requires reimplementing the recursion pattern for each use case rather than abstracting it once. Context This came up while creating a functional programming paradigm example (examples/paradigms/functional/lists.seq). The example can be completed with direct recursion, but generic map/filter/fold would make it more expressive.

navicore commented

2026-01-24 01:42:45 +00:00

(Migrated from github.com)

Case for "won't do":

The workaround is idiomatic. Direct recursion with concrete types is how Forth-family languages traditionally work. The sum-acc pattern isn't really a
workaround - it's the natural way to express this in a concatenative language.
Significant undertaking. Real polymorphism (type variables, HM-style inference, or implicit Variant coercion) would be a major type system overhaul.
The LLVM codegen would need to handle monomorphization or boxing, and the complexity could destabilize what currently works well.
Design coherence. Seq sits at an interesting point: typed enough to catch errors at compile time, but not Haskell. Adding full polymorphism might blur
that identity.

Case for "won't do": 1. The workaround is idiomatic. Direct recursion with concrete types is how Forth-family languages traditionally work. The sum-acc pattern isn't really a workaround - it's the natural way to express this in a concatenative language. 2. Significant undertaking. Real polymorphism (type variables, HM-style inference, or implicit Variant coercion) would be a major type system overhaul. The LLVM codegen would need to handle monomorphization or boxing, and the complexity could destabilize what currently works well. 3. Design coherence. Seq sits at an interesting point: typed enough to catch errors at compile time, but not Haskell. Adding full polymorphism might blur that identity.