DEV Community: Txus

Becoming a logician with TypeScript

Txus — Tue, 17 Sep 2019 08:34:26 +0000

Logic and computation are two sides of the same coin —this is called the Curry-Howard correspondence.

Eh?

Let's explore what this means in a short tour, by the end of which I aim to convince you that, as a developer writing TypeScript, you are writing propositions and proofs for a living!

Throughout recent history, computer scientists and logicians seem to keep discovering the same concepts independently —each new concept discovered in one field seems to neatly map to one in the other.

This duality has been a great driver of innovation in practical type systems — for example, the discovery of new formal logics such as linear logic led to Rust's famous borrow checker.

Let's use TypeScript to explore how everyday types, our bread and butter, acquire a new meaning when looked at from... the other side.

Proving the obvious

Let's look at possibly the simplest type we use in our everyday job: number.

const n: number = 4

This code typechecks —it has a type and a value that matches that type. But how does this have anything to do with formal logic?

We can look at the type number as a logical proposition, which in plain language we could express as there exists a number. Pretty obvious right? But TypeScript won't believe us until we prove it. And that proof is the value 4.

Let's re-read the above code as:

The type number is the proposition or claim that there exists a number
The value 4 is a valid proof of that proposition or claim
TypeScript is convinced with our proof, so our program type-checks!

This, and that too

If simple types are claims that values of that type simply exist... what are tuples?

const nameAndAge: [string, number] = ['Curry', 119]

Turns out tuples let us have our cake and eat it too, that is, do conjunction! Again, let's put our logician hats:

The tuple type [string, number] is the proposition that there exists a string AND there exists a number.
The value ['Curry', 119] is a valid proof of that proposition
That is convincing enough for TypeScript, and so our program type-checks!

What about or?

Similarily, union types let us or propositions together:

const nameOrAge: string | number = 'Curry'

The union type string | number is the proposition that there exists a string OR a number (a non-exclusive or like we're used to in programming)
The value 'Curry' is a valid proof of that proposition
TypeScript says sure, type-checked!

If this, then that

Probably the most interesting kind of TypeScript types from the point of view of logic are... function types!

function add(a: number, b: number): number {
  return a + b
}

Functions represent logical implication (if x, then y). Let's see how:

The function type (a: number, b: number): number is the proposition that if there exists a number a and a number b, there also exists a third number (the return value).
The implementation return a + b is a valid proof that you can effectively make a number given these two numbers.

Less is more

As you've probably noticed, just as there are many numbers of type number, there are many implementations of the function (a: number, b: number): number!

One possible implementation could always return 42, and it would still type-check, because you were able to produce a number given a and b, even if you didn't use them.

That is why, the more expressive a type system is, the more you can constrain types (propositions), so that there are fewer valid implementations (proofs) — and so that the type-checker will reject more invalid ones!

Generalizing with... generics

All generalizations are dangerous, even this one.

Alexandre Dumas-fils

How do generic types come into play? What do they mean in logic? They are a way to generalize claims, so that we don't have to concern ourselves with unnecessary detail.

function length<A>(array: Array<A>): number {
  return array.length
}

In formal logic, they are akin to universal quantification of propositions (claiming that a proposition holds for all things, for every case). Let's look at it from the point of view of TypeScript:

The function type (array: Array<A>): number is the proposition that for any type A, if there exists an array of As, there also exists a number (the return value, its length).
The implementation array.length is a valid proof that you can effectively make a number given an array of absolutely any type.

Staring at the abyss: never say `never`

In any cool formal logic, there should be a way to swear. TypeScript has the never type for that! Let's look at how it's used in practice.

function goOnForever(a: number): never {
  while (true) {
    console.log('I never end!')
  }
}

The type never is also known as the bottom type, and it has no values. That means we can never return anything from this function (and I mean NOTHING, not even undefined or null). In plain English, I like to translate it as the proposition we are screwed.

The function type (a: number): never is the proposition that if there exists a number a, we're screwed.
The implementation never returns any value, and so no further reasoning can be done. We're screwed. TypeScript happily type-checks, because we did fulfill our promise: that we'll never return anything at all.

Promising the moon

Lastly, let's look at an impossible type (proposition), and try to implement (prove) it:

function arbitrary<A>(): A { ... }

What? We are claiming that for any type A, we can come up with a value of that type. Over-confident much? How are you going to implement that function so that you can create a value of type number, Record<string, Password>, and UserPreferencesFactory and whatever else I throw at this function as type A?

This function is surely impossible to implement... in a sound type system. But lo and behold, this type-checks:

function arbitrary<A>(): A {
  return (null as unknown) as A
}

Aha! Turns out TypeScript is not sound —and neither are most modern practical type systems. That's not necessarily a bad thing, but it offers us a major way to screw up our programs. Be careful!

Ambrose Bonnaire-Sergeant wrote an insightful piece about why unsoundness in modern type systems might not be a bad thing.

Conclusion

If you enjoyed this post and want to learn more about these ideas, I recommend you read Philip Wadler's paper Propositions as Types. It's very well-written, witty and understandable even by non-mathy types like me.

I also gave a few talks about the topic, and the potential of expressive type systems to make our programs safer (and thus, our world, increasingly dependant on those programs). Watch it here.

Now I shall let you go get back to your propositions and proofs, I mean, your TypeScript project.

Cover photo by Benjamin Lizardo on Unsplash

Infrastructure as code with Pulumi

Txus — Mon, 19 Aug 2019 13:53:13 +0000

When it comes to managing our infrastructure, as developers we often face a double standard. Our code is version-controlled, subject to code reviews, checked periodically by test harnesses. We don't risk it.

However, the infrastructure running our code, often the most critical part of our production systems, is treated differently. Log onto your AWS account, a few clicks, provision a machine. With the advent of Docker, at least environments have become more reproducible, but still too many of us spend their days clicking around with their cloud superuser account to terraform the world.

Declarative DSLs

Speaking of which, there is... well, Terraform! And other solutions too. The notion of Infrastructure As Code is just starting to become the new default in the DevOps mindset. Declaratively defining your infrastructure, running some basic health checks and having everything version-controlled is a huge step forward.

Declarative DSLs are an improvement, but we can do better. In our experience at Codegram, often you can spend 80% of your time figuring out the right incantation of your cloud provider's module, with very little help from tooling. That means the debugging cycle is painfully slow, and often very frustrating. Even more so in a serverless context, where most of the code is infrastructure glue --queues, storage buckets, and lambdas all need to talk to each other in just the right ways, with the right ACL permissions.

Pulumi was built to leverage the power of general-purpose programming languages to solve these very shortcomings.

Enter Pulumi

Disclaimer: Codegram is not affiliated with pulumi.com in any way. None of the benefits detailed in this post require a subscription to pulumi.com --you can just use the open-source library.

Pulumi is an open-source library that lets you use a general-purpose programming language to build your infrastructure on your cloud provider of choice. At Codegram we usually choose TypeScript as our language for this task.

As an example, here's all the code it takes to create an S3 bucket and spin up an AWS Lambda that triggers on every document uploaded to it:

import * as aws from "@pulumi/aws";

const docsBucket = new aws.s3.Bucket("docs");

docsBucket.onObjectCreated("docsHandler", (e) => {
   for (const rec of e.Records || []) {
      console.log(`Hello from Lambda -- got an S3 Object: ${rec.s3.object.key}`);
    }
});

export docsBucketName = docsBucket.bucketName;

All this glue code is type-checked by the Typescript compiler --from the records inside the S3 event, to the properties of the created S3 Bucket should be want to inspect them. And it goes way beyond serverless --whether you're deploying to Kubernetes, or plain Docker containers, you're good to go.

In my opinion, the advantages of this approach go well beyond mere convenience. Read on.

Extensibility via Terraform providers

Even though Pulumi doesn't depend on Terraform, The Pulumi CLI often leverages Terraform providers, and there is nice tooling to generate a Pulumi library from an existing Terraform provider. In our case, this was tremendously useful as we needed to manage DNSs with DNSimple through Pulumi. Even though it was my first time using the code generation tool, it was only an hour or two until I had the DNSimple integration working.

Repeatable environments

When you keep all your infrastructure alongside your code, spinning up a staging environment, or a test environment in a different cloud region, is trivial. We find that Pulumi helps us bring the gap between starting testing out a piece of code and having a deployed, repeatable environment provisioned from our Continuous Deployment pipeline.

For an agency like us, this becomes even more critical --often, projects start out in our cloud accounts, only to then be moved over to the client's --without the certainty that environments are completely repeatable and nothing is left to point and click interfaces, it would be a daunting task to ensure a smooth handover (and believe me, it used to be).

Avoiding cloud vendor lock-in

The pulumi.cloud right now implements a lot of the basic concepts of a cloud service, in a cloud-agnostic way.

This lets you abstract a lot of the cloud-specific tools to facilitate deploying a multi-cloud project. However, wherever the current APIs can't reach, it's just code -- you can leverage abstraction to avoid locking your infrastructure to a particular cloud vendor.

Serverless and magic functions

Pulumi has the concept of a magic function. It's a closure that will be packaged into a Lambda or cloud function, and it can reference elements of the infrastructure. These elements are resolved at provisioning time, so they are not dynamic, even though they are as flexible as if they were.

import * as aws from '@pulumi/aws'

const inputBucket = new aws.s3.Bucket('input')
const outputBucket = new aws.s3.Bucket('output')

input.onObjectCreated('process', e => {
  for (const rec of e.Records || []) {
    const processed = processFile(rec.s3.object.key)
    uploadFile(outputBucket.bucketName.get(), processed)
  }
})

In this example, every time a file is uploaded to inputBucket, we call a Lambda that processes the file and uploads it to another bucket. The closure we use to define the lambda closes upon outputBucket.bucketName and calls get() on it. This code, at provisioning time, will be compiled to a Lambda that will contain the literal name of the output bucket, statically.

We get all the benefit of seemingly dynamic references between elements of our infrastructure, without the hassle of configuration management --misconfigured environment variables and so on. These references are checked at compile time, before provisioning time, and obviously way before runtime.

Magic functions help building the kind of glue code that is so tedious to write in serverless, seamlessly and with the power of a full programming language and tooling at your disposal.

Encoding best practices

When it comes to managing infrastructure as a team, standardizing best practices becomes essential. Which settings do we use for storage buckets? Do we always use queues to decouple production and consumption? What durability settings are good defaults?

By abstracting common infrastructure patterns in our own company library, these questions are brought into the team, and answered in the form of Pull Requests, code reviews, and technical discussions around real, tangible code. This way we move away from the one person who knows how things are done around here, to version controlled best practices owned by the whole team.

Granular security by default

In traditional infrastructure management, people usually default to creating a superuser first, and worry about tightening permissions later, when all the parts are defined and stable. Does it sound familiar?

To avoid that, having infrastructure patterns in code means you can abstract granular permissions around resources. Whenever you create a queue, the code that does that can make sure that only a specific storage bucket can publish events to it, or that only a specific machine or lambda can read from it.

Once it's in the library, its users (team members) never have to worry about loose permissions again. Write once, worry never again.

Bonus points: type safety

At Codegram, TypeScript is our language of choice to manage infrastructure. The myriad of options that each cloud provider exposes in their wide range of offerings, and the fact that these change often, makes compiler help invaluable.

The reason is, most of the parameter validation in cloud providers is done at actual provisioning time of the particular resource, which means, for N resources, it can easily degenerate into a really long feedback loop.

By having most of the parameter validation at compile time, you don't even need to run the code to make sure it matches. Plus, you get a lot of help from your tooling in terms of auto-completion.

On top of that, TypeScript's type system is powerful enough to allow parametric polymorphism, which helps greatly in abstracting away common patterns, and helps a lot in the way of multi-cloud abstractions.

Conclusion

Managing infrastructure used to be a tedious task that few people enjoyed doing. Since we started using Pulumi, it's fused with the process of developing a project from start to end, and it's given us extra confidence in the portability and repeatability of our production environments.

And now, go forth and terraform the world! Pun intended.

Cover photo by Ricardo Gómez Ángel on Unsplash

DEV Community: Txus

Becoming a logician with TypeScript

Eh?

Proving the obvious

This, and that too

What about or?

If this, then that

Less is more

Generalizing with... generics

Staring at the abyss: never say never

Promising the moon

Conclusion

Infrastructure as code with Pulumi

Declarative DSLs

Enter Pulumi

Extensibility via Terraform providers

Repeatable environments

Avoiding cloud vendor lock-in

Serverless and magic functions

Encoding best practices

Granular security by default

Bonus points: type safety

Conclusion

Staring at the abyss: never say `never`