Theoratical overview over type systems

I hope it’s ok to ask something not specifically related to the IC. I’m trying to get generally a better theoretical understanding of type systems.

From what I understand type systems of various languages range from doing relatively basic checks (is something a string or an int) to being highly expressive. It seems like languages such as Idris go in that direction with dependent types. From what I understand we want the type system not to be turning complete so we know the type checks terminate and are therefore useful to run at compile time (correct?).

As there seems to be a large variety of type “features” it’s hard to understand which features make a type system how expressive. I would love to see an overview of these features ranked by expressiveness with examples of what that enables in practice. Does that exist?

To the people that work on Motoko; how do you think about designing its type system? Which tradeoffs are involved? For example, why do we have variants in Motoko but not union types, how do you think about that?

I ultimately would like to understand these things to write better code. So if you have any advice on how to optimally leverage Motoko’s type system or typescript I’d be interested in that as well.

It would be great if someone could point me to the most useful resources on these topics.
Thanks in advance for any help.

This may be a bit dated now, and doesn’t go into dependent types, but is still I think a classic paper:

http://lucacardelli.name/papers/onunderstanding.a4.pdf

Sorry, need to pack for a trip…

1 Like

Thank you very much, I will make some time to dig into it!