689c445d25
Fourth stdlib module. Pair<a, b> is the canonical product with two type vars and a single constructor MkPair. Five combinators: fst, snd, swap, map_first (Pair<a, b> -> Pair<c, b>), map_second (Pair<a, b> -> Pair<a, c>). Smallest dogfood for the parameterised-ADT path so far: no recursion in the data def or any combinator, single-arm matches throughout. Demo prints 7, 9, 9, 7, 8, 18 deterministically. No compiler bug surfaced (fourth stdlib iter in a row to land clean). The only fixable issue was a paren-balance typo in the demo's seq chain. Cumulative: 4 stdlib modules, 24 combinators. Type-system surface exercised end-to-end now spans 1/2/3-type-var data, 1/2/3-type-var fns, recursive ADTs, cross-module imports of all of the above, flat and nested patterns, TCO via monomorphised musttail, GC. Tests: 93/93 (e2e 33 → 34). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
78 lines
2.1 KiB
Plaintext
78 lines
2.1 KiB
Plaintext
; Iter 15f — fourth stdlib module: product types.
|
|
; Pair<a, b> is the canonical 2-type-var, single-ctor product. No
|
|
; recursion in the data def or any combinator. Combinators here
|
|
; build on the new (Iter 16a) nested-Ctor-pattern support: `swap`
|
|
; flattens via `(pat-ctor MkPair x y)` and the eliminator `pair`
|
|
; matches the same shape directly without an outer var-binding.
|
|
|
|
(module std_pair
|
|
|
|
(data Pair (vars a b)
|
|
(doc "Polymorphic product: a single ctor MkPair holding one value of each parameter.")
|
|
(ctor MkPair a b))
|
|
|
|
(fn fst
|
|
(doc "First projection. Returns the `a` payload.")
|
|
(type
|
|
(forall (vars a b)
|
|
(fn-type
|
|
(params (con Pair a b))
|
|
(ret a))))
|
|
(params p)
|
|
(body
|
|
(match p
|
|
(case (pat-ctor MkPair x _) x))))
|
|
|
|
(fn snd
|
|
(doc "Second projection. Returns the `b` payload.")
|
|
(type
|
|
(forall (vars a b)
|
|
(fn-type
|
|
(params (con Pair a b))
|
|
(ret b))))
|
|
(params p)
|
|
(body
|
|
(match p
|
|
(case (pat-ctor MkPair _ y) y))))
|
|
|
|
(fn swap
|
|
(doc "Exchange the components: Pair<a, b> -> Pair<b, a>.")
|
|
(type
|
|
(forall (vars a b)
|
|
(fn-type
|
|
(params (con Pair a b))
|
|
(ret (con Pair b a)))))
|
|
(params p)
|
|
(body
|
|
(match p
|
|
(case (pat-ctor MkPair x y)
|
|
(term-ctor Pair MkPair y x)))))
|
|
|
|
(fn map_first
|
|
(doc "Apply f to the first component, leave the second intact.")
|
|
(type
|
|
(forall (vars a b c)
|
|
(fn-type
|
|
(params (fn-type (params a) (ret c))
|
|
(con Pair a b))
|
|
(ret (con Pair c b)))))
|
|
(params f p)
|
|
(body
|
|
(match p
|
|
(case (pat-ctor MkPair x y)
|
|
(term-ctor Pair MkPair (app f x) y)))))
|
|
|
|
(fn map_second
|
|
(doc "Apply f to the second component, leave the first intact.")
|
|
(type
|
|
(forall (vars a b c)
|
|
(fn-type
|
|
(params (fn-type (params b) (ret c))
|
|
(con Pair a b))
|
|
(ret (con Pair a c)))))
|
|
(params f p)
|
|
(body
|
|
(match p
|
|
(case (pat-ctor MkPair x y)
|
|
(term-ctor Pair MkPair x (app f y)))))))
|