Now don't pitch me Hindley-Milner because _that_ one I grok well enough to know it has some forbidding limitations making it a poor fit for mutation-/imperative-permitting languages. Instead of tagged sum types like ML-alikes sport, I'm hankering after more-structural/not-nominal and type-annotation-free covering at least TypeScript's capabilities. Now I _did_ find the 2012 Flow Typing paper and an inferencer for it by ayazhafiz.com but it's a total symbol soup and there's just no coder-lingo treatments of such out there, only greek algebraic gibberish. I also don't see them handling imperative mutations that expand/change a variable's type at that "temporal location" for so long until it is next mutated elsewhere (perhaps even in an anon closure passed off to elsewhere to run elsewhen). Also that "calculus" seemingly ignoring recursion (mutual or direct). And even so adapting the (quite hefty) OCaml version it seems like a real cryptic soup that I see no sense in even adopting unless I grok it deeply. But I didn't want to sign up for years of PhD study of, dunno, "type theory" or abstract algebra or whatever they call it just to get a type-inferencer done & working.
Feels like I'm missing the right kinda material to see the light and capture me that grokkage. Like the tuts out there when you want to learn ASM, C, 3D graphics? I can stomach that, in fact love to. But all this type theory stuff drives me mad and has me only mystified. But I need to cover the full spectrum from Never to Any, the logical Union/Intersection/Negation types, on top of the usual basic prim types. And — inferred, not via annotation.
Oh yeah, hacking it together ad-hoc and patching it up until it works really don't fly in this arena. Tried more than once. Will keep at it too if have to. But it really is a weird tar-pit. 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).
Abstract interpretation? Dunno. I feel there has to some elegant-core akin to a bare-bones minimal Lisp that already covers its own self-interpretation, that can deliver this computation without a gigantic hairball of special-casing rules that have been brute-forced into being and seem inscrutable in and of themselves?
I'm sure I'm missing a puzzle piece and one of you out here has it. Spill it!
But I still think since dynamic languages can do it at runtime (figure out the type of a var)
In dynamic languages, variables don't have types, only values do.
Tomato, tomahto. You clearly got what I was getting at =)
Didn't this thread used to have more replies?
I also don't see them handling imperative mutations that expand/change a variable's type at that "temporal location" for so long until it is next mutated elsewhere
Locally if all cases of mutation agree in typestate then the type transitions can be inferred, e.g. the same type transforms occur in either branch of an if
Playing type tetris is fun thougheverbeit
>>6
M-x tetris
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.
and also for like $INSERT_LANG_NAME they some times do formal verification or compiler formal verification, so that's how they can be sure that language is type safe. so it's up to you to ensure if your lang or $interpreted_dynamic_lang_of_your_interest is formally verified. There is CompCert & similiar. I've heard some parts of ML/Rust been formally verified, that's their selling feature and +1 reason behind their marketing.
If you care about type safety your probably want your lang compiler/interpreter to be formally verified, but you can't do that without dipping your toes in to fundamentals of math of type theory. In theory you can do formal verification in ML/Coq etc.
and if you want your lang to be secure, there are ISO standarts secure verifications.