Creating tools for Developers

DATE 2025-03-07 -- TIME 07:11:49

Description

I'm making a programming language and there's nothing you can do to stop me

I’ve been working on this thing on and off on nights and weekends (and maybe even some vacations) for about a year (the README was created February of 2024, today is March 2025). It’s time to start talking about it. Or, talk about it publicly, because I’ve already been telling anyone who would listen about its best parts. Of which there are many.

Extra

The best part about Extra is:

Every single thing about it. Take the best of Elm, the best of TypeScript, the best of Swift and Rust and Python, then remove the really amazing compiler performance because that’s not what I spent any time on yet, and you will have something still not as good as Extra. Let’s take a look.

Today, we’re just looking at Types.

Extra has Types.

TypeScript has types too so what!?

Not like this.

Rust?

Nope, still not there.

Haskell!?

Well yea of course Haskell has types as good as… wait does it? Hey I found out the standard lib doesn’t have types as good as Extra! (jumping ahead: Extra has “refinement types”) (my sarcasm and hyperbole are just getting started, btw)

Types are rooted in set theory, so I’d like to build up a model of how I considered types in Extra using those terms.

Let’s start with two important types:

  • Never the empty set
  • Any the set of all possible types

Never is useful for expressing the type of a type in the else branch of a switch that is already exhaustive:

let
  isExtraAmazing: true | null = whatDoesUserThink(user: you, about: 'Extra')
in
  switch (isExtraAmazing) {
    case:
      true => "aww thank you"
    case:
      null => "you haven't heard of Extra!?"
    else:
      -- 'isExtraAmazing' would have type 'Never' in this branch, because we have
      -- already checked for the only other possible values: true | null
      'impossible branch'
  }

So Never has no members, and Any has all possible types (which, incidentally, makes it just about as useful and useless as Never, if you think about it).

┌───────┐
│       │
│  Any  │ ←- any type you can imagine is in here, and in
│       │ -- untyped languages, this is *the only* type.
└───────┘

  Never   ←- nothing to see here

We divide Any into smaller sets. For example (not an exhaustive list):

  • Int
  • Float
  • String
  • Boolean
┌────────────────────┐
│  Any               │
│ ┌───┐  ┌─────┐     │
│ │Int│  │Float│     │
│ └───┘  └─────┘     │
│ ┌──────┐ ┌───────┐ │
│ │String│ │Boolean│ │
│ └──────┘ └───────┘ │
└────────────────────┘

Where things get interesting is if we zoom into one of these types…

┌───────────┐
│   Any     │
│ ┌───────┐ │
│ │Boolean│ │
│ │┌─────┐│ │
│ ││true ││ │
│ │└─────┘│ │
│ │┌─────┐│ │
│ ││false││ │
│ │└─────┘│ │
│ └───────┘ │
└───────────┘

That’s it for Boolean. There’s a “type” true and a “type” false. “type” in danger quotes because it’s really a value, but values have types, and the type of the value ‘true’ is the type ‘true’… yeah… so let’s just call it something simple like “literal”.

But if the literal Boolean value true is a valid type what about numbers? Is 1 a valid type? Sure ‘nuff!

Wait. I said Extra was better than TypeScript at representing types, so what gives…

Let’s jump to the chase. Int is the “set of all integers”. So how about the set of positive integers?

┌──────────────────┐
│   Any            │
│ ┌──────────────┐ │
│ │  Int         │ │  -- I was having fun with ASCII box drawing
│ │┌───┐┌─┐┌───┐ │ │  -- but now this is getting tedious...
│ ││<0 ││0││ >0│ │ │  -- can you see that this is "All Integers"
│ │└───┘└─┘└───┘ │ │  -- containing "all negatives/zero/all positives"?
│ └──────────────┘ │
└──────────────────┘

We can express it mathematically, how about in Extra type notation?

type PositiveInt = Int(>0)

“Alright,” you’re saying to yourself, “That is really cool, how about a Byte, ie an 8-bit positive integer?”

type Byte = Int(0...255)

“Woah now, ok, how about we group those into an Array to make an IPv4 type,” you caught yourself saying before you could stop yourself. You wanted to know more!

“But hold up, because IPv4 only has 4 integers. If we introduce an Array type, it could have any number of items in it…”

Please, sit down, drink some water, and allow me:

type IPv4 = Array(Int(0...255), length: =4)

If you then try to construct an IPv4 with negatives or large numbers or not enough or too many of them, the compiler will tell you to sod off.

let
  ip-address: IPv4 = [10, 0, 0, 1, 256]
                                   ^^^ Error: sod off (no, not really)

How it works

Types can have “refinements”. These are specific to the type, for instance Array/Dict/Set/String all have a length refinement, which is of type PositiveRange (minimum length is 0). Boolean doesn’t have any refinements. Int has a magnitude refinement (minimum and/or maximum values), and Float does as well but the range can be open or closed (inclusive or exclusive). String also has a matches refinement, which is an array of Regex that the string must match.

When you make a check on a value, that check can annotate the type with a refinement. That hot bowl of word soup means:

let
  a: Int = …
in
  if (a > 0) {
    then:
      -- in this branch, 'a' is of type 'Int(>0)'
    else:
      -- and in this branch, 'a' is of type 'Int(<=0)'
  }

So what about Array#length refinements?

if (users.length == 0) {
  then:
    -- users: Array(User, length: =0), an empty array type
  else:
    -- users: Array(User, length: >0)
}

In the then/else branches of the conditional, users is annotated with more type information; it is “narrowed/refined”, hence the term “type refinement”.

These annotations need not be concrete numbers, though. They might be relationships to other data structures. This is where the sauce starts to get extra calienté!

I’m going to implement a zip function, which takes two Arrays and combines their values into a new Array, with each entry being a 2-tuple. I’m going to do it in a cool, type-safe way that guarantees the lengths are all consistent.

Hold my beer.

let
  -- "#lhs: Array" indicates a positional argument, e.g. zip(_)
  -- "lhs: Array" would indicate a named argument, e.g. zip(lhs: _)
  fn zip<T, U, L is Int>(
    #lhs: Array(T, length: L)  -- commas are optional when separating by newlines
    #rhs: Array(U, length: L)  -- rhs must have _the same length_
  ): Array({T, U}, length: L)  -- returns Array of 2-Tuple, same length
  =>
    lhs.map((left, index) => -- index: Int(<L)
      {left, rhs[index]} -- 2-tuple of lhs and rhs
    )

  names = ...
  numbers = ...
in
  if (names.length === numbers.length) {
    then:
      -- names and numbers are annotated with the same length, even though we don't
      -- know the length at runtime
      zip(names, numbers)
    else:
      []  -- pick a fallback value
  }

One important detail to point out: Array#[index: Int] usually returns a nullable type, but not if the index is less than the known length. This means that you can check a number against the length of the array, and if the number is less, you can use it to verifiably retrieve an item from the array.

-- it also has to be positive, duh
if (index >= 0 and index < users.length) {
  then:
    -- index is now annotated as `Int(0..<users.length)`
    -- users[index] is of type 'User'
  else:
    -- users[index] is of type 'null'
}

This also works for things like keyof Dict.

if (key in names) {
  then:
    -- names[key] is of type 'String'
  else:
    -- names[key] is of type 'null'
}

Random things before we wrap up

The Object type (aka Tuple - these are one type in Extra) doesn’t have refinements per se, because they are inherently built up from other types (is this why they’re called “Product” types? because they’re the “Product” of combining other types! No one knows.), but there are lots of ways that you can build up new Object types based on other Object types (just like you can in TypeScript, and this is the only thing that is only just as good because frankly TypeScript nailed this feature and the best anyone can do is to copy it with no changes) (other than changing <> to ()).

const AllPartsOfALanguage = ['syntax', 'features', 'standard library']
type TheBestProgrammingLanguage =
  Omit(Javascript, AllPartsOfALanguage)
  &
  Pick(Extra, AllPartsOfALanguage)

The Dict, Array, and Set types are homogeneous - all items have the same type.

Does that mean you can’t mix and match items in these containers? Not at all!

let
  things = dict(
    thing1 = 'I am a string'
    thing2 = 2  -- and this is an int
  )
in
  typeof things --> Dict(String | Int)
  -- actually, because it was assigned *literals*, `things` would have the type
  -- Dict('I am a string' | 2)

Importantly, you could not pass Dict(String | Int) to a function expecting Dict(String) or Dict(Int), or Dict(String) | Dict(Int) (dict of all strings or dict of all ints). These are all distinct types.

You could, however, pass an IPv4 to a function expecting Array(Int). But not the other way around.

This is because Array(Int) is a type that contains the subtype IPv4.

I got off the topic of set theory (I felt like I was losing you?), but see how I brought it all back around!? That’s character development! Or no, exposition? Foreshadowing?

Anyway, that’s a glimpse into Types in Extra. Hopefully you stayed awake long enough to drink all the Koolaid.

Published: 2025-03-03