Iter 15f: std_pair — 2-type-var product, no recursion
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>
This commit is contained in:
@@ -0,0 +1 @@
|
||||
{"defs":[{"ctors":[{"fields":[{"k":"var","name":"a"},{"k":"var","name":"b"}],"name":"MkPair"}],"doc":"Polymorphic product: a single ctor MkPair holding one value of each parameter.","kind":"type","name":"Pair","vars":["a","b"]},{"body":{"arms":[{"body":{"name":"x","t":"var"},"pat":{"ctor":"MkPair","fields":[{"name":"x","p":"var"},{"p":"wild"}],"p":"ctor"}}],"scrutinee":{"name":"p","t":"var"},"t":"match"},"doc":"First projection. Returns the `a` payload.","kind":"fn","name":"fst","params":["p"],"type":{"body":{"effects":[],"k":"fn","params":[{"args":[{"k":"var","name":"a"},{"k":"var","name":"b"}],"k":"con","name":"Pair"}],"ret":{"k":"var","name":"a"}},"k":"forall","vars":["a","b"]}},{"body":{"arms":[{"body":{"name":"y","t":"var"},"pat":{"ctor":"MkPair","fields":[{"p":"wild"},{"name":"y","p":"var"}],"p":"ctor"}}],"scrutinee":{"name":"p","t":"var"},"t":"match"},"doc":"Second projection. Returns the `b` payload.","kind":"fn","name":"snd","params":["p"],"type":{"body":{"effects":[],"k":"fn","params":[{"args":[{"k":"var","name":"a"},{"k":"var","name":"b"}],"k":"con","name":"Pair"}],"ret":{"k":"var","name":"b"}},"k":"forall","vars":["a","b"]}},{"body":{"arms":[{"body":{"args":[{"name":"y","t":"var"},{"name":"x","t":"var"}],"ctor":"MkPair","t":"ctor","type":"Pair"},"pat":{"ctor":"MkPair","fields":[{"name":"x","p":"var"},{"name":"y","p":"var"}],"p":"ctor"}}],"scrutinee":{"name":"p","t":"var"},"t":"match"},"doc":"Exchange the components: Pair<a, b> -> Pair<b, a>.","kind":"fn","name":"swap","params":["p"],"type":{"body":{"effects":[],"k":"fn","params":[{"args":[{"k":"var","name":"a"},{"k":"var","name":"b"}],"k":"con","name":"Pair"}],"ret":{"args":[{"k":"var","name":"b"},{"k":"var","name":"a"}],"k":"con","name":"Pair"}},"k":"forall","vars":["a","b"]}},{"body":{"arms":[{"body":{"args":[{"args":[{"name":"x","t":"var"}],"fn":{"name":"f","t":"var"},"t":"app"},{"name":"y","t":"var"}],"ctor":"MkPair","t":"ctor","type":"Pair"},"pat":{"ctor":"MkPair","fields":[{"name":"x","p":"var"},{"name":"y","p":"var"}],"p":"ctor"}}],"scrutinee":{"name":"p","t":"var"},"t":"match"},"doc":"Apply f to the first component, leave the second intact.","kind":"fn","name":"map_first","params":["f","p"],"type":{"body":{"effects":[],"k":"fn","params":[{"effects":[],"k":"fn","params":[{"k":"var","name":"a"}],"ret":{"k":"var","name":"c"}},{"args":[{"k":"var","name":"a"},{"k":"var","name":"b"}],"k":"con","name":"Pair"}],"ret":{"args":[{"k":"var","name":"c"},{"k":"var","name":"b"}],"k":"con","name":"Pair"}},"k":"forall","vars":["a","b","c"]}},{"body":{"arms":[{"body":{"args":[{"name":"x","t":"var"},{"args":[{"name":"y","t":"var"}],"fn":{"name":"f","t":"var"},"t":"app"}],"ctor":"MkPair","t":"ctor","type":"Pair"},"pat":{"ctor":"MkPair","fields":[{"name":"x","p":"var"},{"name":"y","p":"var"}],"p":"ctor"}}],"scrutinee":{"name":"p","t":"var"},"t":"match"},"doc":"Apply f to the second component, leave the first intact.","kind":"fn","name":"map_second","params":["f","p"],"type":{"body":{"effects":[],"k":"fn","params":[{"effects":[],"k":"fn","params":[{"k":"var","name":"b"}],"ret":{"k":"var","name":"c"}},{"args":[{"k":"var","name":"a"},{"k":"var","name":"b"}],"k":"con","name":"Pair"}],"ret":{"args":[{"k":"var","name":"a"},{"k":"var","name":"c"}],"k":"con","name":"Pair"}},"k":"forall","vars":["a","b","c"]}}],"imports":[],"name":"std_pair","schema":"ailang/v0"}
|
||||
@@ -0,0 +1,77 @@
|
||||
; 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)))))))
|
||||
@@ -0,0 +1 @@
|
||||
{"defs":[{"body":{"args":[{"name":"x","t":"var"},{"lit":{"kind":"int","value":1},"t":"lit"}],"fn":{"name":"+","t":"var"},"t":"app"},"doc":"Add 1. Used as the (a -> c) arg.","kind":"fn","name":"inc","params":["x"],"type":{"effects":[],"k":"fn","params":[{"k":"con","name":"Int"}],"ret":{"k":"con","name":"Int"}}},{"body":{"args":[{"name":"x","t":"var"},{"lit":{"kind":"int","value":2},"t":"lit"}],"fn":{"name":"*","t":"var"},"t":"app"},"doc":"Multiply by 2. Used as the (b -> c) arg.","kind":"fn","name":"double","params":["x"],"type":{"effects":[],"k":"fn","params":[{"k":"con","name":"Int"}],"ret":{"k":"con","name":"Int"}}},{"body":{"lhs":{"args":[{"args":[{"args":[{"lit":{"kind":"int","value":7},"t":"lit"},{"lit":{"kind":"int","value":9},"t":"lit"}],"ctor":"MkPair","t":"ctor","type":"std_pair.Pair"}],"fn":{"name":"std_pair.fst","t":"var"},"t":"app"}],"op":"io/print_int","t":"do"},"rhs":{"lhs":{"args":[{"args":[{"args":[{"lit":{"kind":"int","value":7},"t":"lit"},{"lit":{"kind":"int","value":9},"t":"lit"}],"ctor":"MkPair","t":"ctor","type":"std_pair.Pair"}],"fn":{"name":"std_pair.snd","t":"var"},"t":"app"}],"op":"io/print_int","t":"do"},"rhs":{"lhs":{"args":[{"args":[{"args":[{"args":[{"lit":{"kind":"int","value":7},"t":"lit"},{"lit":{"kind":"int","value":9},"t":"lit"}],"ctor":"MkPair","t":"ctor","type":"std_pair.Pair"}],"fn":{"name":"std_pair.swap","t":"var"},"t":"app"}],"fn":{"name":"std_pair.fst","t":"var"},"t":"app"}],"op":"io/print_int","t":"do"},"rhs":{"lhs":{"args":[{"args":[{"args":[{"args":[{"lit":{"kind":"int","value":7},"t":"lit"},{"lit":{"kind":"int","value":9},"t":"lit"}],"ctor":"MkPair","t":"ctor","type":"std_pair.Pair"}],"fn":{"name":"std_pair.swap","t":"var"},"t":"app"}],"fn":{"name":"std_pair.snd","t":"var"},"t":"app"}],"op":"io/print_int","t":"do"},"rhs":{"lhs":{"args":[{"args":[{"args":[{"name":"inc","t":"var"},{"args":[{"lit":{"kind":"int","value":7},"t":"lit"},{"lit":{"kind":"int","value":9},"t":"lit"}],"ctor":"MkPair","t":"ctor","type":"std_pair.Pair"}],"fn":{"name":"std_pair.map_first","t":"var"},"t":"app"}],"fn":{"name":"std_pair.fst","t":"var"},"t":"app"}],"op":"io/print_int","t":"do"},"rhs":{"args":[{"args":[{"args":[{"name":"double","t":"var"},{"args":[{"lit":{"kind":"int","value":7},"t":"lit"},{"lit":{"kind":"int","value":9},"t":"lit"}],"ctor":"MkPair","t":"ctor","type":"std_pair.Pair"}],"fn":{"name":"std_pair.map_second","t":"var"},"t":"app"}],"fn":{"name":"std_pair.snd","t":"var"},"t":"app"}],"op":"io/print_int","t":"do"},"t":"seq"},"t":"seq"},"t":"seq"},"t":"seq"},"t":"seq"},"doc":"Drive every combinator. Expected (per line): 7, 9, 9, 7, 8, 18.","kind":"fn","name":"main","params":[],"type":{"effects":["IO"],"k":"fn","params":[],"ret":{"k":"con","name":"Unit"}}}],"imports":[{"module":"std_pair"}],"name":"std_pair_demo","schema":"ailang/v0"}
|
||||
@@ -0,0 +1,32 @@
|
||||
; Iter 15f — fourth consumer demo. Drives every std_pair combinator
|
||||
; once. fst/snd are stable at 7/9; swap reverses; map_first/map_second
|
||||
; demonstrate the Pair<a, b> -> Pair<c, b> / Pair<a, c> reshape with
|
||||
; b/a held rigid.
|
||||
|
||||
(module std_pair_demo
|
||||
|
||||
(import std_pair)
|
||||
|
||||
(fn inc
|
||||
(doc "Add 1. Used as the (a -> c) arg.")
|
||||
(type (fn-type (params (con Int)) (ret (con Int))))
|
||||
(params x)
|
||||
(body (app + x 1)))
|
||||
|
||||
(fn double
|
||||
(doc "Multiply by 2. Used as the (b -> c) arg.")
|
||||
(type (fn-type (params (con Int)) (ret (con Int))))
|
||||
(params x)
|
||||
(body (app * x 2)))
|
||||
|
||||
(fn main
|
||||
(doc "Drive every combinator. Expected (per line): 7, 9, 9, 7, 8, 18.")
|
||||
(type (fn-type (params) (ret (con Unit)) (effects IO)))
|
||||
(params)
|
||||
(body
|
||||
(seq (do io/print_int (app std_pair.fst (term-ctor std_pair.Pair MkPair 7 9)))
|
||||
(seq (do io/print_int (app std_pair.snd (term-ctor std_pair.Pair MkPair 7 9)))
|
||||
(seq (do io/print_int (app std_pair.fst (app std_pair.swap (term-ctor std_pair.Pair MkPair 7 9))))
|
||||
(seq (do io/print_int (app std_pair.snd (app std_pair.swap (term-ctor std_pair.Pair MkPair 7 9))))
|
||||
(seq (do io/print_int (app std_pair.fst (app std_pair.map_first inc (term-ctor std_pair.Pair MkPair 7 9))))
|
||||
(do io/print_int (app std_pair.snd (app std_pair.map_second double (term-ctor std_pair.Pair MkPair 7 9))))))))))))
|
||||
Reference in New Issue
Block a user