# type theory

## `void` is not a unit type in TypeScript

In type theory a unit type is any type that represents exactly one possible value. The unit types in TypeScript include null, undefined, and literal types. TypeScript also has the type void which is used as the return type for functions that don’t have an explicit return value. In JavaScript a function that does not explicitly return implicitly returns undefined; so at first glance it would seem that void is an alias for the undefined type. But it is not! …

## When to use `never` and `unknown` in TypeScript

This is an excerpt of a post that I wrote for LogRocket. The never and unknown primitive types were introduced in TypeScript v2.0 and v3.0 respectively. These two types represent fundamental and complementary aspects of type theory. TypeScript is carefully designed according to principles of type theory, but it is also a practical language, and its features all have practical uses – including never and unknown. To understand those uses we will have to begin with the question, what exactly are types? …

## Type-Driven Development with TypeScript

This is an excerpt of a post that I wrote for Olio Apps. I am always interested in making my coding process faster and more robust. I want to be confident that my code will work as expected. And I want to spend as little time as possible debugging, testing, and hunting down pieces of code that I forgot to update when I make changes to a project. That is why I am a fan of correct-by-construction methods. Those are methods of constructing programs where the program will not build / compile unless it behaves the way that it is supposed to. …

## Category Theory proofs in Idris

Dependent types provide an unprecedented level of type safety. A quick example is a type-safe printf implementation. They are also useful for theorem proving. According to the Curry-Howard correspondence, mathematical propositions can be represented in a program as types. An implementation that satisfies a given type serves as a proof of the corresponding proposition. In other words, inhabited types represent true propositions.