Iter 15g — std_either_list: first 3-way cross-module stdlib fn
First stdlib fn that imports three other stdlib modules (std_list,
std_either, std_pair) and returns a compound polymorphic ADT tree
(Pair<List<e>, List<a>>). Stresses monomorphisation across nested
parameterised ADTs.
What shipped:
- examples/std_either_list.{ailx,ail.json}: 3 combinators —
- lefts : forall e a. (List<Either<e, a>>) -> List<e>
- rights : forall e a. (List<Either<e, a>>) -> List<a>
- partition_eithers : forall e a. (List<Either<e, a>>)
-> Pair<List<e>, List<a>>
lefts/rights use depth-2 nested Ctor patterns (Cons (Left l) t)
— exercises 16a's desugar pass at a depth not reached by any
prior fixture.
- examples/std_either_list_demo.{ailx,ail.json}: drives all three
combinators on a five-element List<Either<Int, Int>>; expected
output one per line: 2, 3, 2, 3.
- crates/ail/tests/e2e.rs::std_either_list_demo: e2e count 34 → 35.
- docs/JOURNAL.md: Iter 15g entry.
Compiler bug surfaced (queued as 15g-aux, not fixed):
unify_for_subst in ailang-codegen/src/lib.rs accepts $u wildcards
only on the arg side. Mixing inline (Either Left n) and (Either
Right n) in a list literal lands $u on the param side via the
outer List<a>'s binding and errors. Reduced repro: `length [Left
1, Right 10]`. Demo works around with monomorphic mkleft/mkright
helpers; workaround documented inline. Fix is a one-line symmetric
extension of the early-return.
Tests: 94/94. Stdlib: 5 modules, 27 combinators.
This commit is contained in:
@@ -0,0 +1 @@
|
||||
{"defs":[{"body":{"arms":[{"body":{"args":[{"name":"l","t":"var"},{"args":[{"name":"t","t":"var"}],"fn":{"name":"lefts","t":"var"},"t":"app"}],"ctor":"Cons","t":"ctor","type":"std_list.List"},"pat":{"ctor":"Cons","fields":[{"ctor":"Left","fields":[{"name":"l","p":"var"}],"p":"ctor"},{"name":"t","p":"var"}],"p":"ctor"}},{"body":{"args":[{"name":"t","t":"var"}],"fn":{"name":"lefts","t":"var"},"t":"app"},"pat":{"ctor":"Cons","fields":[{"ctor":"Right","fields":[{"p":"wild"}],"p":"ctor"},{"name":"t","p":"var"}],"p":"ctor"}},{"body":{"args":[],"ctor":"Nil","t":"ctor","type":"std_list.List"},"pat":{"p":"wild"}}],"scrutinee":{"name":"xs","t":"var"},"t":"match"},"doc":"Project the Left payloads of a list of Eithers into a List<e>. Order-preserving. Uses the 16a nested-Ctor pattern to inline the inner Either dispatch within each Cons arm; the trailing wildcard arm seals the desugar's fall-through chain into a List<e> rather than the synthetic Unit fallback.","kind":"fn","name":"lefts","params":["xs"],"type":{"body":{"effects":[],"k":"fn","params":[{"args":[{"args":[{"k":"var","name":"e"},{"k":"var","name":"a"}],"k":"con","name":"std_either.Either"}],"k":"con","name":"std_list.List"}],"ret":{"args":[{"k":"var","name":"e"}],"k":"con","name":"std_list.List"}},"k":"forall","vars":["e","a"]}},{"body":{"arms":[{"body":{"args":[{"name":"t","t":"var"}],"fn":{"name":"rights","t":"var"},"t":"app"},"pat":{"ctor":"Cons","fields":[{"ctor":"Left","fields":[{"p":"wild"}],"p":"ctor"},{"name":"t","p":"var"}],"p":"ctor"}},{"body":{"args":[{"name":"r","t":"var"},{"args":[{"name":"t","t":"var"}],"fn":{"name":"rights","t":"var"},"t":"app"}],"ctor":"Cons","t":"ctor","type":"std_list.List"},"pat":{"ctor":"Cons","fields":[{"ctor":"Right","fields":[{"name":"r","p":"var"}],"p":"ctor"},{"name":"t","p":"var"}],"p":"ctor"}},{"body":{"args":[],"ctor":"Nil","t":"ctor","type":"std_list.List"},"pat":{"p":"wild"}}],"scrutinee":{"name":"xs","t":"var"},"t":"match"},"doc":"Project the Right payloads of a list of Eithers into a List<a>. Symmetric to lefts; same nested-Ctor + wildcard-tail pattern shape.","kind":"fn","name":"rights","params":["xs"],"type":{"body":{"effects":[],"k":"fn","params":[{"args":[{"args":[{"k":"var","name":"e"},{"k":"var","name":"a"}],"k":"con","name":"std_either.Either"}],"k":"con","name":"std_list.List"}],"ret":{"args":[{"k":"var","name":"a"}],"k":"con","name":"std_list.List"}},"k":"forall","vars":["e","a"]}},{"body":{"arms":[{"body":{"args":[{"args":[],"ctor":"Nil","t":"ctor","type":"std_list.List"},{"args":[],"ctor":"Nil","t":"ctor","type":"std_list.List"}],"ctor":"MkPair","t":"ctor","type":"std_pair.Pair"},"pat":{"ctor":"Nil","fields":[],"p":"ctor"}},{"body":{"body":{"arms":[{"body":{"args":[{"args":[{"name":"l","t":"var"},{"args":[{"name":"rest","t":"var"}],"fn":{"name":"std_pair.fst","t":"var"},"t":"app"}],"ctor":"Cons","t":"ctor","type":"std_list.List"},{"args":[{"name":"rest","t":"var"}],"fn":{"name":"std_pair.snd","t":"var"},"t":"app"}],"ctor":"MkPair","t":"ctor","type":"std_pair.Pair"},"pat":{"ctor":"Left","fields":[{"name":"l","p":"var"}],"p":"ctor"}},{"body":{"args":[{"args":[{"name":"rest","t":"var"}],"fn":{"name":"std_pair.fst","t":"var"},"t":"app"},{"args":[{"name":"r","t":"var"},{"args":[{"name":"rest","t":"var"}],"fn":{"name":"std_pair.snd","t":"var"},"t":"app"}],"ctor":"Cons","t":"ctor","type":"std_list.List"}],"ctor":"MkPair","t":"ctor","type":"std_pair.Pair"},"pat":{"ctor":"Right","fields":[{"name":"r","p":"var"}],"p":"ctor"}}],"scrutinee":{"name":"h","t":"var"},"t":"match"},"name":"rest","t":"let","value":{"args":[{"name":"t","t":"var"}],"fn":{"name":"partition_eithers","t":"var"},"t":"app"}},"pat":{"ctor":"Cons","fields":[{"name":"h","p":"var"},{"name":"t","p":"var"}],"p":"ctor"}}],"scrutinee":{"name":"xs","t":"var"},"t":"match"},"doc":"Partition a list of Eithers into a Pair<List<e>, List<a>>: lefts on the left, rights on the right. Single pass via direct recursion; head dispatch is a flat match on the recursive result's projections.","kind":"fn","name":"partition_eithers","params":["xs"],"type":{"body":{"effects":[],"k":"fn","params":[{"args":[{"args":[{"k":"var","name":"e"},{"k":"var","name":"a"}],"k":"con","name":"std_either.Either"}],"k":"con","name":"std_list.List"}],"ret":{"args":[{"args":[{"k":"var","name":"e"}],"k":"con","name":"std_list.List"},{"args":[{"k":"var","name":"a"}],"k":"con","name":"std_list.List"}],"k":"con","name":"std_pair.Pair"}},"k":"forall","vars":["e","a"]}}],"imports":[{"module":"std_list"},{"module":"std_either"},{"module":"std_pair"}],"name":"std_either_list","schema":"ailang/v0"}
|
||||
@@ -0,0 +1,71 @@
|
||||
; Iter 15g — fifth stdlib module: first 3-way cross-module fn set.
|
||||
; Imports std_list, std_either, std_pair simultaneously. All three
|
||||
; combinators dispatch over List<Either<e, a>>; partition_eithers
|
||||
; additionally returns Pair<List<e>, List<a>>. Stresses
|
||||
; monomorphisation across List × Either × Pair, cross-module ctor
|
||||
; resolution at qualified term-ctor sites, and the 16a desugar
|
||||
; layer at depth-2 nested Ctor patterns (in `lefts` / `rights`).
|
||||
|
||||
(module std_either_list
|
||||
|
||||
(import std_list)
|
||||
(import std_either)
|
||||
(import std_pair)
|
||||
|
||||
(fn lefts
|
||||
(doc "Project the Left payloads of a list of Eithers into a List<e>. Order-preserving. Uses the 16a nested-Ctor pattern to inline the inner Either dispatch within each Cons arm; the trailing wildcard arm seals the desugar's fall-through chain into a List<e> rather than the synthetic Unit fallback.")
|
||||
(type
|
||||
(forall (vars e a)
|
||||
(fn-type
|
||||
(params (con std_list.List (con std_either.Either e a)))
|
||||
(ret (con std_list.List e)))))
|
||||
(params xs)
|
||||
(body
|
||||
(match xs
|
||||
(case (pat-ctor Cons (pat-ctor Left l) t)
|
||||
(term-ctor std_list.List Cons l (app lefts t)))
|
||||
(case (pat-ctor Cons (pat-ctor Right _) t)
|
||||
(app lefts t))
|
||||
(case _ (term-ctor std_list.List Nil)))))
|
||||
|
||||
(fn rights
|
||||
(doc "Project the Right payloads of a list of Eithers into a List<a>. Symmetric to lefts; same nested-Ctor + wildcard-tail pattern shape.")
|
||||
(type
|
||||
(forall (vars e a)
|
||||
(fn-type
|
||||
(params (con std_list.List (con std_either.Either e a)))
|
||||
(ret (con std_list.List a)))))
|
||||
(params xs)
|
||||
(body
|
||||
(match xs
|
||||
(case (pat-ctor Cons (pat-ctor Left _) t)
|
||||
(app rights t))
|
||||
(case (pat-ctor Cons (pat-ctor Right r) t)
|
||||
(term-ctor std_list.List Cons r (app rights t)))
|
||||
(case _ (term-ctor std_list.List Nil)))))
|
||||
|
||||
(fn partition_eithers
|
||||
(doc "Partition a list of Eithers into a Pair<List<e>, List<a>>: lefts on the left, rights on the right. Single pass via direct recursion; head dispatch is a flat match on the recursive result's projections.")
|
||||
(type
|
||||
(forall (vars e a)
|
||||
(fn-type
|
||||
(params (con std_list.List (con std_either.Either e a)))
|
||||
(ret (con std_pair.Pair (con std_list.List e) (con std_list.List a))))))
|
||||
(params xs)
|
||||
(body
|
||||
(match xs
|
||||
(case (pat-ctor Nil)
|
||||
(term-ctor std_pair.Pair MkPair
|
||||
(term-ctor std_list.List Nil)
|
||||
(term-ctor std_list.List Nil)))
|
||||
(case (pat-ctor Cons h t)
|
||||
(let rest (app partition_eithers t)
|
||||
(match h
|
||||
(case (pat-ctor Left l)
|
||||
(term-ctor std_pair.Pair MkPair
|
||||
(term-ctor std_list.List Cons l (app std_pair.fst rest))
|
||||
(app std_pair.snd rest)))
|
||||
(case (pat-ctor Right r)
|
||||
(term-ctor std_pair.Pair MkPair
|
||||
(app std_pair.fst rest)
|
||||
(term-ctor std_list.List Cons r (app std_pair.snd rest)))))))))))
|
||||
File diff suppressed because one or more lines are too long
@@ -0,0 +1,46 @@
|
||||
; Iter 15g — fifth consumer demo. First demo to import four stdlib
|
||||
; modules (std_list, std_either, std_pair, std_either_list); first to
|
||||
; thread a List<Either<Int, Int>> through three combinators that
|
||||
; together exercise every monomorphisation site introduced by 15g.
|
||||
;
|
||||
; The list is constructed via the monomorphic helpers `mkleft` and
|
||||
; `mkright` rather than bare `(term-ctor std_either.Either Left ...)` /
|
||||
; `(term-ctor std_either.Either Right ...)`. This sidesteps a codegen
|
||||
; bug that 15g surfaced: when an inline list literal mixes
|
||||
; `Either Left n` (pins e, leaves a as `$u`) and `Either Right n` (pins
|
||||
; a, leaves e as `$u`), the synth-time unification of the outer
|
||||
; `List<a>`'s parameter against the `$u`-bearing element types fails
|
||||
; on the param side because `unify_for_subst` only accepts arg-side
|
||||
; `$u` wildcards. The helpers fully pin both type vars at the call
|
||||
; site, so each list element arrives with concrete `Either<Int, Int>`
|
||||
; and the bug is dodged. Logged as known-debt under 15g; the fix is
|
||||
; a one-line symmetric extension of the `$u` early-return.
|
||||
|
||||
(module std_either_list_demo
|
||||
|
||||
(import std_list)
|
||||
(import std_either)
|
||||
(import std_pair)
|
||||
(import std_either_list)
|
||||
|
||||
(fn mkleft
|
||||
(doc "Monomorphic Left-injector at Either<Int, Int>. Pins both type vars at the call site so the codegen synth doesn't leave a `$u` wildcard on the second var.")
|
||||
(type (fn-type (params (con Int)) (ret (con std_either.Either (con Int) (con Int)))))
|
||||
(params x)
|
||||
(body (term-ctor std_either.Either Left x)))
|
||||
|
||||
(fn mkright
|
||||
(doc "Monomorphic Right-injector at Either<Int, Int>. Symmetric to mkleft.")
|
||||
(type (fn-type (params (con Int)) (ret (con std_either.Either (con Int) (con Int)))))
|
||||
(params x)
|
||||
(body (term-ctor std_either.Either Right x)))
|
||||
|
||||
(fn main
|
||||
(doc "Drive lefts, rights, and partition_eithers on the same five-element List<Either<Int, Int>> (Left 1, Right 10, Left 2, Right 20, Right 30). Expected output (one per line): 2, 3, 2, 3.")
|
||||
(type (fn-type (params) (ret (con Unit)) (effects IO)))
|
||||
(params)
|
||||
(body
|
||||
(seq (do io/print_int (app std_list.length (app std_either_list.lefts (term-ctor std_list.List Cons (app mkleft 1) (term-ctor std_list.List Cons (app mkright 10) (term-ctor std_list.List Cons (app mkleft 2) (term-ctor std_list.List Cons (app mkright 20) (term-ctor std_list.List Cons (app mkright 30) (term-ctor std_list.List Nil)))))))))
|
||||
(seq (do io/print_int (app std_list.length (app std_either_list.rights (term-ctor std_list.List Cons (app mkleft 1) (term-ctor std_list.List Cons (app mkright 10) (term-ctor std_list.List Cons (app mkleft 2) (term-ctor std_list.List Cons (app mkright 20) (term-ctor std_list.List Cons (app mkright 30) (term-ctor std_list.List Nil)))))))))
|
||||
(seq (do io/print_int (app std_list.length (app std_pair.fst (app std_either_list.partition_eithers (term-ctor std_list.List Cons (app mkleft 1) (term-ctor std_list.List Cons (app mkright 10) (term-ctor std_list.List Cons (app mkleft 2) (term-ctor std_list.List Cons (app mkright 20) (term-ctor std_list.List Cons (app mkright 30) (term-ctor std_list.List Nil))))))))))
|
||||
(do io/print_int (app std_list.length (app std_pair.snd (app std_either_list.partition_eithers (term-ctor std_list.List Cons (app mkleft 1) (term-ctor std_list.List Cons (app mkright 10) (term-ctor std_list.List Cons (app mkleft 2) (term-ctor std_list.List Cons (app mkright 20) (term-ctor std_list.List Cons (app mkright 30) (term-ctor std_list.List Nil))))))))))))))))
|
||||
Reference in New Issue
Block a user