add some notes about type systems and type theory

This commit is contained in:
Alain Zscheile 2023-05-28 00:31:24 +02:00
parent 5672942c6b
commit 44d71ac8f9

73
TYPES.md Normal file
View File

@ -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.