diff --git a/TYPES.md b/TYPES.md
new file mode 100644
index 0000000..4f2b146
--- /dev/null
+++ b/TYPES.md
@@ -0,0 +1,73 @@
+# notes about type theories and type systems
+
+## the problem symptoms
+
+This programming language (PL) needs a proper type system to avoid the pitfalls of
+C++ template system, which does not scale properly to the needs of
+bigger projects because it ends up being too messy; particularly because errors
+only occur on usage points and there is no way to exhaustively check that
+expected invariants actually hold in an elegant way, leading to unreadable
+error messages and unexpected downstream problems.
+
+## about the urgency
+
+This PL basically inherits that problem mostly because it is extremely dynamic
+(and most dynamic PLs also share this pitfall).
+This problem can't really be solved at a much later stage, where there already
+exists a full interpreter or perhaps even an optimizing compiler, larger amounts
+of non-example code are already written, etc. because adopting a proper type system
++ type theory would cause massive friction and probably feel "not worth the effort"
+but the lack would make programming in the language a massive pain once project
+size grows, but by then, it would be too late to fix. (see also the problems of
+pythons `mypy` linter, etc.)
+
+## resources
+
+So, there are basically a bunch of really interesting papers regarding stuff
+probably affecting this language, in particular:
+
+* [MLsub](https://dl.acm.org/doi/10.1145/3093333.3009882) about polymorphism, subtyping and type inference
+* [simple-sub](https://github.com/LPTK/simple-sub), basically an implementation of MLsub which avoids the
+  somewhat difficult-to-implement structures the original paper used. probably faster and easier to implement
+  than the original paper. The usage of mutable reference-counted objects make it non-trivial to implement
+  in Rust, tho.
+* [Intro to Module systems](https://www.stephendiehl.com/posts/exotic01.html) by Stephen Diehl;
+  this language should have modules, so this is relevant.
+
+For an overview of type systems and theory, the following books were suggested to me:
+* [Types and programming languages](https://www.cis.upenn.edu/~bcpierce/tapl/) by B.C. Pierce;
+  it is pretty nice to read, but the usage of ML makes transforming of algorithms to Rust a bit of a challenge.
+* [The Little Typer](https://thelittletyper.com/) by Daniel P. Friedman and David Thrane Christiansen, etc.;
+  didn't read this one yet, but will try it. about dependent typing and associated type systems and their
+  implementation, etc.
+
+Other resources:
+* https://soasis.org/posts/a-mirror-for-rust-a-plan-for-generic-compile-time-introspection-in-rust/; an article
+  about Generic compile time introspection in Rust. pretty interesting, and maybe related to optional compile time
+  introspection features (basically pattern based code generation) for
+  [Haskell](https://en.wikipedia.org/w/index.php?title=Generic_programming&oldid=1154881316#Genericity_in_Haskell) in concept.
+* I derived [gardswag's type system](https://github.com/fogti/gardswag/tree/main/crates/gardswag-typesys) mostly from:
+  http://dev.stephendiehl.com/fun/006_hindley_milner.html
+  (huge shout-out to Stephen Diehl for the Haskell implementation, which was imo much easier to understand than the usually used Ocaml implementations)
+  Author of primary reference: Stephen Diehl
+  License: [CC BY-NC-SA](https://creativecommons.org/licenses/by-nc-sa/4.0/)
+  Sadly, the website is extremely slow to access, it's a bit painful...
+
+## the problem
+
+This PL needs support for
+* Modules + module system, including modules generic over data types, and perhaps even values.
+* control-flow jumps
+* linear types
+* `defer`/destructors, to deal with the combination of control-flow jumps and some linear types.
+* this also introduces the difficulty that in the presence of linear types, control-flow jumps
+  which don't guarantee exactly-once re-entry (it might be delayed, but it must happen,
+  the continuation *gains* the linearity of its bound/contained variables)
+* generics over arg multiplicity or some similar work around, or proper subtyping for such functions;
+  this is necessary to work around some problems noticed in Idris2, which doesn't have that,
+  and which induces the problem that a function which uses a generic argument linearly can't
+  be freely used in functions which don't care about the linearity of that argument, this
+  is particularly obvious in the `id` identity function, which is linear in its argument,
+  but can't be used in places where a function is expected which doesn't have a linear argument.
+  In particular, something that isn't linear shouldn't suddenly gain that property by just calling a function, usually.
+  Rust somehow appears to solve this, but I don't exactly know how.