It doesn't have to be PhD. it could have been M.Sc. or B.Eng. with semester credit course in functional programming, compilers, PL theory.
But you seem doesn't have those.
Well, lucky you, I'm here to help you, at the best Anon Guest board alternative to Hackernews, that treats me with fat 403 in my mouth, each time I try to open it to contribute. (srsly, dublicate your question to Stack Overflow, Hackernews, pick one and wait some time to repost to another platform). But don't just Ctrl-C -V your text, you should rewrite it to make it bearable to read & let some Bachelor review it, before you post it. Like there is some thing off-putting expressions that make you look like not a Senior Grug but as an a typical roblox enjoyer.
getting (even paid) grad/undergrad course in PL, compilers, ML, typesystems, set|category|type theory in your case if you want to accomplish the task you said, doesn't seem like a bad option. Or hiring an M.Sc. tutor/teacher.
The problem you described is kind of naive in description and you looking plain naive solution. A simple naive solution that may not exist and you may not find, realizing only after by purseuing the hard way.
The things you've described you need to accomplish : is writing compiler, type checker, static analyzer, and those things aren't 10th grade math, it's a Type Theory level of math. And you'll face some fundamentals before you proceed. This ain't a 5min guide to spawn a roblox server, bud.
Ok, let's proceed to answer step by step
don't pitch me Hindley-Milner
yes, there are other alternatives type inference systems
but it's a total symbol soup and there's just no coder-lingo treatments of such out there, only greek algebraic gibberish.
yes, exactly, it's called mathemathical notations for type theory, and is de facto language of type systems & math behind, idk how you expected to find something else.
Maybe you should start by learning notation for learning untyped & then simply typed lambda calculus, and then there are good video tutorials for Set | Category | Hott | CoC | CTT theories on youtube. You free to use GPT, but it doesn't understand everything and prone to invalid answers.
You trying to accomplish M.Sc. job but like without having preq B.Sc+M.Sc. background exp. Make sure you getting paid for 'project of yours' otherwise it'll end up like yet another TempleOS level lang, byproduct of manic psychosis. If you getting paid, you allowed to invest your non-free & some one else time/resources, because no time is free in this world. Otherwise if that's just hobby toy project it's at risk of being abandoned/incompleted. Support resources matter. General C compiler, as example, isn't a byproduct of One lonely single person/dev.
But I didn't want to
outsource to few individuals to make few different versions of inference, pick then according to your taste. You haven't even provided an git of your project with a description, do you think projects trying to recruit contributors/mainteiners/community for no reason? Start by writing a documentation of your project , that's clearly an git ticket issue. I don't recomment using github today , due their policies.
ML >Hindley-Milner >temporal >mutation
they are not Rust, they never heard of Rust and weren't developed with notion of it around it. There is Quantitive Type Theory however :3 I'm working on a smol cute PL research of mine, so if you want to stay in touch & around & about here, welcome UwU. optionally leave email. I think your post it cute, after 10th time re-reading it >;3
you may familiarize yourself with SIGBOVIK and similiar related relevant user groups to ask there. Just ask better, smarter questions, not that naive gibberish you described. Other than HN/S.O you may also ask/post at few relevant Reddit/Mastodon/Matrix/X/pleroma/akkoma/fedi communities.
you must undestand is what you writing is a type system, type checker, static analyzer for a compiler.
all this type theory stuff drives me mad and has me only mystified
you are not alone, me too. and others as well.
fly in this arena
ioquake had been written in C. (so is Linux). time for you to remind yourself of Memory Arenas, RAII, safe pointers, and write lang with lifetimes, borrow checker, without GC, with optional manual safe meme. I'm tired of GC langs, we don't need another slowlang.
But I still think since dynamic languages can do it at runtime (figure out the type of a var), it must be just as possible statically from just the wholly-unannoted code-base at hand itself, plus the known arg/ret types of prim ops (your arithmetic & logical impls).
dynamic interpreted langs like python/ruby/js/etc compiled to bytecode which later interpreted by their relevant iterpreter in runtime. so you just look at C code of CPython as example. You can ask any specific lang/compiler/interpreter dev did they based lang on specific type inference theory.
Your problem is you trying to develop `something new`, and existing solutions don't fit you. You don't like ML. You don't want to look at Rust typechecker source code and ask their dev how they implemented inference. Something new IS PhD, people like getting degree for this literally, by writing new lang, compiler. Dynamic lang doesn't use so called inference, you look at specific code of relevant dynamic lang for runtime checks. Inference/typechecking calculation is just fancy name for Formalized Execution/Computation/Interpretation of types. e.g. type checker calculates types in type checking environment stage aka type checking runtime. fast. for seconds. they just don't call it 'runtime' they call it type checking. what you may missing, is that completeted formalized based on math theory checks for termination|infinity. interpreter doesn't. that's probably the difference.
I think I gave pretty exhaustive & extensive answer to your post. Hope that was helpful and useful, and you hit and smash that like button, support me on ko-fi, get my NFT, and answer with demostration of appreciation & any more new relevant questions. I'm glad I could help with such simple thing, because I wouldn't handle anything much more complex, sowy.