Type systems are interesting

Hi,

I am Aman, and this safe space is where I am most raw with my thoughts, hop on if you'd like to interact with them :))

Introduction/Context

Type systems have been my new fascination for past few weeks, but before going deep down into this rabbit hole, let me provide a little bit of context first of how i got here at the first place.

Javascript is the first programming language I learned, and since there is no native type system associated with the language, migrating to typescript was a very interesting.

Apart from Javascript I have written in golang and my endeavour's with golang are still ongoing

understanding go

I have been fascinated by the differences in expressions that different languages communicate, and have been going deeper into the type system rabbit hole

A very simple javascript type system in golang

I'm sorry for the rabbit hole I'm about to introduce you to. ― Cat Voleur, Revenge Arc

Type system

I really like this approach where I can project my understanding of a particular subject in order to understand it with more clarity

A type system proposes a set of rules, which can be used to reason logic in a programming language.

As a developer who works with typescript you may think that the goal of a type system is to predict whether an integer is an integer or not, which is not entirely wrong

but a type system can be thought of as the underlying science/theoretical proof on the basis of which the behaviours of a particular language can be predicted.

A way for the compiler to predict the correctness of a program, in simplest terms to predict the correctness of any logical argument in computer science.

Understanding Type Inference

Copycopy code to clipboard
1const result = function mul (x){
2   return x*2
3}

Let's try to infer the type of the value returned from this function using the idea of a type system, which is one of the applications of an effective type system

The function returns

Copycopy code to clipboard
1x*2

Now considering * as a multiplication operation, the list of possible values which result can be narrows down to a few possible options like

1. int
2. float
3. string
4. Invalid

Considering how most languages are designed they will not let you execute a multiplication operation on a boolean value or even string returning some runtime error or a compilation error or returning an invalid value

This is what Javascript returns when I try to

Copycopy code to clipboard
1console.log('a' *2)

NaN

which boils down the possibility to two options result can be either an int or a float, and this is where the theoretical nuance of a type system kicks in. The Lamda calculus which helps us determine the type of x,

Now one might think, why is the inference of type such a useful thing?

A programming language has a set of rules and operations which it chooses to allow based on those types, without this logical interface inside the language it will become very difficult for a language to model the real world.

Hindley-Milner type system is one such system.

Applications of type systems

All this theoretical concepts are fine but what I find absolutely fascinating is the applications of such type systems,

I mean programming languages are possibly the coolest applications of these extending beyond theoretical proofs.

Typescript's type system is turing complete which means they can be used for all sorts of things.

At this point I was invested too much into type systems world and the normie developer inside me was screaming hard for a todo app, so why not

World's simplest todo implementation using a type system

Hypescript

The best thing about rabbit holes is, as you go deeper and deeper you find things that you would never expect to,

**enters hypescript**

Copycopy code to clipboard
1export type Tail<T extends Array<any>> = ((...t: T) => void) extends (
2  h: any,
3  ...rest: infer R
4) => void
5  ? R
6  : never;
7
8export type Push<T extends Array<any>, E> = [...T, E];
9
10export type Unshift<T extends Array<any>, E> = [E, ...T];
11
12export type Concat<T1 extends Array<any>, T2 extends Array<any>> = [
13  ...T1,
14  ...T2,
15];
16
17export type TailBy<
18  T extends Array<any>,
19  B extends number,
20  A extends Array<any> = [],
21> = B extends A['length'] ? T : TailBy<Tail<T>, B, Push<A, 0>>;

This is an implementation of array data structure using typescript's type system, taken straight out of hypescript, for a nerd like me this is absolutely cool just thinking about the possibilities we can extend type systems to.

Refs/Rabbit Holes

Intro to Lambda Calculus: Syntax, evaluation, terminology (compared to Haskell, Python, JavaScript)

What to know before debating type systems

So you want to write a type checker (2014)

Typing the Technical Interview in TypeScript

Extreme Explorations of TypeScript's Type System

Conclusion

Accelerated Learning

This is still one of my core thesis, learning has become so much better post chat gpt.

I personally believe it is easier for anyone to pursue theoretical side quests now, just to satisfy curiosity.

Executing learning experiments have become a lot easier now and I think I will continue to do more of these quests where I can dive super deep into something theoretical just to understand the world around me better.