Dependent types, refinement types, gradual types, rank-n polymorphism, etc, – we are moving in the right direction

Let’s dream a bit and try to imagine what can be improved about type systems. Ability to limit and check variables and function arguments at compile time multiplies development speeds by dozens of times, but modern type systems are STILL not expressive enough - you mostly can filter out only quite basic errors. Functional programmers excel at making the wrong state inexpressible in terms of the type system, but static type systems still can’t encode very complex logic and relations.

Well, they do, but it is absolutely unusable for casual coding, fast prototyping, and most industrial use cases.

In certain fields, such as game development, the amount of rules gets crazy, and most interactions of related game mechanics can’t even be covered with tests, not to mention types. But possibly this is only because type systems are too restrictive. They don’t allow embedding crazy expressions from the the value level. Yet.

Possible Improvements For Type Systems

  1. Types should be first-class objects. There should be convenient type lambdas
  2. Types should be allowed to contain value-level expressions (Refinement Types)
  3. Moreover, types could contain runtime values (Gradual Types)
  4. The same code should be usable both at compile time and execution time
  5. There should be runtime conditional expressions for type checks
  6. All definitions and type specifications should share context with the code they’re in
  7. Type intersection is a fundamental operation for composing types
  8. BONUS: Types, sets, and functions should be unified with T̷y̷p̴e̷ ̵Fi̵l̷t̸e̵r̸s̴
  9. BONUS: I̸n̵v̶e̵r̶s̶e̷ f̵un̸c̴t̵i̴o̷n̴s̸ ̵s̵h̵o̸u̸l̸d̶ ̶e̷a̴s̶e̶ work with ̷a̴l̷l t̵y̷p̵e̸ ̴s̴p̵e̴c̵i̸f̵i̴c̵a̵t̷i̸o̵n̴s (next post)
  10. BONUS: Type/value union is another fundamental operation for representing indeterminism

What in the name of satan is all of that? Possibly, I’ll explain everything in the next blog posts, but this time, let’s just review some examples.


I’ll use pseudocode in some semi-esoteric language for clarity. It’s very expressive, so if you want something more conventional, you can change to pseudo-C++ or pseudo-Haskell in every code example - see tabs above code blocks. But I suggest to glimpse through all three.

In this section, I’ll explain shortly how to read the ideas described in this post.

Firstly, this is how type intersection is done. This would be a fundamental operation for composing types.

myVariable: MyType1
            MyType2 & MyType3
MyIntersectionType = MyType1 & MyType2
MyStruct = has myField:  Integer
           has myField2: String
// Values of type MyStruct are limited to those which have
// both `myField` and `myField2` fields
intersect<MyType1, MyType2> myVariable;
using MyStruct = intersect<struct { int x; }, 
                           struct { int y; }>
// Values of type MyStruct are limited to those which have
// both `myField` and `myField2` fields (struct { int x, y; })
type MyIntersectionType = MyType1 & MyType2
type MyStruct = { x :: Integer }
              & { y :: Bool    }
-- Values of type MyStruct are limited to those which have
-- both `myField` and `myField2` fields (MyStruct { x :: Integer, y :: Bool })

In our magical language, type-level expressions could contain runtime values. This could be both constructed types and subtractive types that would filter out values of types they’re intersecting with. For example, here we use “myNaturalVariable” in inline type definition:

myNaturalVariable: Integer
myVariableWithCondition: {1, 2, 3, myNaturalVariable}
                         if myNaturalVariable > 3
auto positive = [](int x){ return x >= 0; };
using MyNaturalType = intersect<int, refine(positive)>;
MyNaturalType myNaturalVariable;

using MyTypeWithCondition = intersect<{1, 2, 3, myNaturalVariable}, 
                                      condition(myNaturalVariable > 3)>;
type MyNaturalType = Integer & refine (>=0)

myNaturalVariable :: MyNaturalType
myNaturalVariable = 4

type MyTypeWithCondition = [ 1, 2, 3, myNaturalVariable ]
                         & { myNaturalVariable > 3}

Unique to this theoretical language. Types should not only be on the same level as variables, but also they should act as functions, collections, and as true predicates. All these concepts can be unified with one syntax for a concept of “type filter”.

In the examples for C++ and Haskell, I use refine function/keyword, which creates a refinement type out of function - otherwise, if we write just functions, it won’t look as clear. Also, C++ doesn’t allow type annotation of any value, so I can’t apply “type filter” idea to it.

3: Int
print (Int 3)
"123": Boolean // error
4: >0          // partially applied "greater than zero" function
               // acts as a type
(=2) 2 = 2 : (=2) // hellish mashup
1: (x->1) // lambda as set/type

myList = [1, 2, 3, 4, 5] 
// with this syntax, there are some cool ways to say `map (1+) myList`:
print (x:myList -> x+1) // [2, 3, 4. 5, 6]
print {x:myList + 1}   // [2, 3, 4. 5, 6]
auto positive = [](int x){ return x > 0; };
refine(positive) x; // partially applied "greater than zero" function
                    // acts as a type

x :: Integer & refine (>0)
"123" :: Boolean -- error
4 :: refine (>0) -- partially applied greater than zero function
                 -- acts as a type

Dependent Types With Runtime Values

This is not possible anywhere now (is it?), but I’m sure after 30 more years of research, we’ll be able to do this in some experimental Haskell extension or language. Runtime values can be used in static types and erased after compilation, leaving dynamic checks only on entry points. Here is a simple example of what this could look like:

Dog = has isAwake: Boolean
          bark() : String     // type intersection takes place
                   if isAwake // String & (if not isAwake)
                 = "woof"

dog: Dog
dog.isAwake <- read Boolean
print dog.bark() // error: can't apply `dog.bark`, 
                 //        `dog.isAwake` could be false
if dog.isAwake // theoretical "if" intersects types with 
               // information from the condition
    print dog.bark() // woof
struct Dog {
    bool isAwake;
    auto bark() -> intersect<string, condition(isAwake)> {
        return "woof";

Dog dog;
std::cin >> dog.isAwake;
std::cout << dog.bark(); // error: can't apply `Dog::bark`, 
                         //        `dog.isAwake` could be false
if auto (dog.isAwake) { // theoretical "if auto" intersects types with 
                        // information from the condition
                        // (of course, I had to invent another use for auto)
    std::cout << dog.bark(); // woof
data Dog = Dog { isAwake :: Boolean }
bark :: { this :: Dog } -> String & if isAwake this
bark this = "woof"

main :: IO ()
main = do
    isDogAwake <- getLine
    let dog = Dog { isAwake = (read isDogAwake :: Boolean) }
    print $ bark dog -- error: can't apply `bark`, 
                     --        `dog.isAwake` could be false
    if' isAwake dog then -- theoretical "if'" intersects types 
                         -- with information from the condition
        print $ bark dog -- woof

My dog actually can bark while sleeping, but in the example above, you won’t be able to call bark function without guaranteeing that isAwake is false.

Here is one more example of the same concept:

Dog = has maxFood = 10
          food: >= 0
                <= maxFood
          isHungry = food != maxFood

          eat newFood : where newFood + food < maxFood
                        if isHungry
                      = food <- food + newFood
dog: Dog <- 2 (read Integer) // error: argument newFood doesn't satisfy `newFood + food < maxFood` and `isHungry`
read Integer : clamp 0 5 :
struct Dog {
    int maxFood = 10;
        > food;
    bool isHungry() {
        return food != maxFood;

    auto eat(int newFood) -> intersect<void,
            condition(newFood + food < maxFood),
        food += newFood;


Dog dog; = 2;

int newFood;
std::cin >> newFood;; // error: argument newFood doesn't satisfy 
                  //`newFood + food < maxFood` and `isHungry`, newFood, 5)); // no error
type Dog = { maxFood :: Int, food :: Int & refine (<=maxFood) }
isHungry dog = food dog != maxFood
eat :: { this :: Dog } 
    -> { newFood :: Int } 
    -> Dog & if isHungry & if food this + newFood < maxFood this
    = ...

main = do
    foodToEatInput <- getLine
    let foodToEat = read foodToEatInput :: Int
    let dog = Dog { food = 2, maxFood = 10 }
    print $ eat dog footToEat -- error: argument newFood doesn't satisfy:
                              -- - food this + newFodd < maxFood this  
                              -- - isHungry

    let foodToEatLimited = clamp (0, 5) newFood
    print $ eat dog footToEat -- no error


It can be implementation-dependent whether the value is actually stored in memory, or is it inferred at compile time like an evidence and discarded immediately. Perhaps things like implication and abstract value could be cleaner than a typed variable.

Dog = has
    food < maxFood => isHungry

dog: Dog <- read (0 <= _ <= 10) 1 // error: couldn't satisfy `isHungry` (`food <= maxFood`)
class Dog {
    implication(food < maxFood, isHungry);

Dog dog;
std::cin >>;; // error: couldn't satisfy `isHungry` (`food <= maxFood`)

type Dog = { maxFood :: Int, food :: Int & refine (<=maxFood) } isHungry dog = food < maxFood eat :: { isHungry dog } => { dog :: Dog } -> Dog

main = do foodInput <- getLine let dog = Dog { food = (read foodInput :: Int), maxFood = 10 } print $ eat dog 1 – error: couldn’t satisfy isHungry (food <= maxFood)

There is enough information for isHungry flag would be completely erased on runtime, even though no values are known at compile time: all checks are performed outside on input, conversions, and manual tests!

By the way, this actually resembles logic programming on Prolog and similar systems.

Complex Relations Expressed With Type System

Static typing in popular languages is very good for letting you know about typos, misplaced arguments, and other minor mess-ups. But it is usually too concrete to give a programmer the ability to express higher concepts and rule out possibilities of behavior-related bugs. While proposed ideas obviously can’t solve all of them, it’s certainly useful to let users describe more details of the system using the tools in the language.

Case Study: Game UI Bugs

Let’s suppose that in some game, the player is suggested to select one or more goods at the same time and click upgrade button to buy selected goods for his gold. There are many kinds of bugs for UI to protect from, such as

  • buying 0 goods
  • spending all gold in some other window and then buying something in this window because it wasn’t updated
  • somehow buying things twice at the same time
  • buying things for less gold than required

These errors need to be explicitly warned in UI - that means that every bug has to be mentally (and sometimes physically) procesed multiple times. It would be good to remove this burden from an UI implementor. He would be warned of each bug and he will be forced to handle each case that is described right in the type system.

GoodInShop = has item: InventoryItem
                      cost: Cost
Shop = has
    player: Player
    buy goods = ...
        where goods: [GoodInShop]
     >= fold (+) (x:goods -> x.cost)
              not goods.isEmpty
struct GoodInShop {
    InventoryItem item;
    Cost cost;

class Shop {
    using GoodsToBuy = intersect(
        const std::vector<GoodInShop>&, // wrong
        refine([](const std::vector<GoodInShop>& goods){ return !goods.empty(); }),
        refine([this](const std::vector<GoodInShop>& goods){ 
            return player->gold() >= 
                       std::ranges::accumulate(goods, 0 [](const auto& x, const auto&y){ 
                                                    return x.cost + y.cost;}
    void buy(GoodsToBuy goods);
data GoodInShop = GoodInShop { inventoryItem :: InventoryItem, cost :: Cost }
type BuyOrder = (Player, [GoodInShop])
                & refine ((!=[]) . snd) 
                & refine (\(player, goods) -> foldl (+) 0 x > gold player)
buy :: PlayerId -> GoodsToBuy -> Shop ()

How a game designer could try to use it at first in UI layer:

ShopWindowWidget.buyButton.onClick = do
    goodToBuy: this.goodsBox.children
    goodToBuy.Selected = true {goodToBuy} // error:
        std::vector<GoodInShop> goodsToBuy;
        for (auto& child: this->goodsBox) {
            if (auto goodToBuy = Cast<GoodInShop>(child)) {
                if (goodToBuy.Selected)
        this->shop->buy(goodsToBuy); // error:
    button <- makeButton "BuyButton" $ do
        goodsToBuy <- getSelectedGoods
        buy shop goodsToBuy // error: 

getSelectedGoods :: GUI [GoodInShop]
getSelectedGoods = do

Type system immediately will stop him, noting that goodsToBuy can be empty and that he didn’t handle the case when there is not enough gold. User can then probably handle these cases like that

ShopWindowWidget.buyButton.onClick = do
    goodToBuy: this.goodsBox.children
    goodToBuy.Selected = true

    if isEmpty goodToBuy
    else if < fold (+) (x:goods -> x.cost)
    else {goodToBuy}
        std::vector<GoodInShop> goodsToBuy;
        for (auto& child: this->goodsBox) {
            if auto (auto goodToBuy = Cast<GoodInShop>(child)) {
                if auto (goodToBuy.Selected)
        if auto (goodsToBuy.empty())
        else if auto (player->gold() >= std::ranges::accumulate(goods, Goods::cost))
    button <- makeButton "BuyButton" $ do
        goodsToBuy <- getSelectedGoods
        buy shop goodsToBuy

getSelectedGoods :: GUI [GoodInShop]
getSelectedGoods = do

Now, type system quickly ensures that the player will never have less gold than needed on calling buy, and it won’t allow passing an empty array or any other incorrect data. It would make sense to name give these types/rules simple names and reuse them across the project.

Asking The Type System

No one would want to rewrite parts of conditions like in the previous example. You would either alias each of intersection operands and test separately, or check for generic error. Maybe there could be a special tool that would return true if an argument can be applied by function, kind of like SFINAE in C++:

if fits glDrawElementsInstanced mode count _ indexBuffer _
    fail "incorrect buffer size specified"
if constexpr (fits<glDrawElementsInstanced, mode, count, _, indexBuffer, _>())
    return std::unexpected("incorrect buffer size specified");
if fits glDrawElementsInstanced mode count _ indexBuffer _ then
    fail "incorrect buffer size specified"

Perhaps we could wrap it into a language’s error management systems/patterns somehow (I suggest to read all examples

    print (read MyStructure)
catch error: TypeError
    print e.message
try constexpr { // haha
} catch (std::type_error e) {
parseUser :: String -> String -> TypeCheck User
parseUser name description = 
    parsedName <- parseName name
    parsedDesc <- parseDesc desc
    return $ User name desc
    checkType (parseUser "Jane Doe" "123")"

Synergizing Types

To provide easiest experience when mixing runtime and compile-time computations, we could not only erase the boundary between type-level entities and value-level entities, but also erase the boundary between types and collections.

In the example below, types/functions could have other operations bound to them, allowing them to be used in listing all values from the time, like in collection. Certain things, like Integers could have these operations defined so that their behaviour is obvious.

for i: (>0) // error: no end condition
    print i
for i: (<10) // error: no start condition
    print i
for 0 < i < 10
    print i // 12345678910
for (auto i: moreThan(0)) // error: no end condition (or `begin`)
    std::cout << i;
for (auto i: lessThan(10)) // error: no start condition (or `end`)
    std::cout << i;
for (auto i: values<intersect<lessThan(0), moreThan(10)>>())
    std::cout << i; // 12345678910
map print (>0) -- endless print
map print ((>0) & (<10)) -- 12345678910

So, “more-than” type would provide a way to get the beginning of the collection, “less-than” specifies an ending, and integer would tell the compiler to increment value to get the next value. All three combined allow you to go through each value.

Case Study: Calculated Values as Evidence

Let’s review something less “arithmetic” in the context of this idea.

Creature = has
    NearEnemy c: Creature = c.faction != this.faction
                           distance c.position this.position < this.attackRange
    attack target: this.NearEnemy =
        target.applyDamage this.getDamage

    attackClosestEnemy() = do
        nearEnemies = world.creatures
        attack (world.random.pick nearEnemies)
class Creature {
    auto NearEnemy<const Creature& c> = 
        intersect<condition(c.faction != faction),
                  condition(distance(c.position, position) < attackRange)>;
    void attack(const NearEnemy& target) {
    void attackClosestEnemy() {
        auto nearEnemies = values(intersect<world->creatures,
nearEnemy :: Creature -> Creature -> Boolean
nearEnemy c other = faction c != faction other 
                 && distance (position c) (position other) < attackRange c

attack :: Creature -> NearEnemy -> GameState ()
attack this enemy = applyDamage enemy (damage this)

attackClosestEnemy :: Creature -> GameState ()
attackClosestEnemy this = 
    creatures <- getCreatures
    let nearEnemies = creatures & nearEnemy
    randomCreature <- randomPick nearEnemies
    attack this randomCreature

All the work happens in nearEnemies - it goes through all creatures in the world and filters only those from different faction and in near attack range. attack then takes a value that is definitely a NearEnemy. I think this could be a great improvement in readability, coding speed, and safety.


Of course, by “simpler types” I mean that they shouldn’t be simple in terms of theory behind them. Supporting things above with at compile type and with type erasure could take years of research and implementation. But it will be simpler from user perspective: there should less rules and limitations of what a user can write. For example, by C++17 standard, you are not allowed to capture structured bindings into lambdas. This is a pointless limitation that was fixed in the next standard. Not allowing runtime values in types is similar too. Whatever you write, it should work as expected, like a blackboard.