>>105684409
Thanks anon that was fun to read (the latter half was kinda complicated), I was wondering about lambda without type annotations (like s3.3 in the pdf) and it looks like that's addressed in s5 (with subst)

With these changes to >>105683999 lambda can be written without type annotations
(define (update bind type table)
(set-cdr! (assoc bind table) type)
type)

[('lambda bind body)
(set! table (cons (cons bind 'a) table))
(let ([type (test body table)])
(list (lookup bind table) '-> type))]
[(f x)
(match (list (test f table) (test x table))
...]
[('+ x y)
(match (list (test x table) (test y table))
[('Int 'Int) 'Int]
[('Real 'Real) 'Real]
[('a 'Int) (update x 'Int table)]
[('a 'Real) (update x 'Real table)]
[('Int 'a) (update y 'Int table)]
[('Real 'a) (update y 'Real table)]
[(a b) (format #t "type error: (+ ~a ~a)~%" a b) #f])]
with the limitation that most polymorphic terms don't check
(check (lambda x (+ x 1))) ;=> (Int -> Int)
(check ((lambda x (+ x 1)) 1)) ;=> Int

(check (lambda x x)) ;=> (a -> a)
(check ((lambda x x) 1)) ;=> type mismatch: ((a -> a) Int)
(check (lambda x (+ x x))) ;=> type error: (+ a a)

I'm tired of pretending mukimame isn't a top tier addition to noodles, rice, and salads.