There has been a lot of work on this in typed functional programming languages!

I recommend checking out projects like LiquidHaskell that add â€śrefinement typesâ€ť onto a type system. I also recommend checking out languages like Agda, Idris, or Coq where they use â€śdependent typesâ€ť to get very strong guarantees about stuff like this.

You can do aspects of it in any language with an ML-family type system. In Haskell you could represent numbers as types like this:

```
data Zero
data Succ a -- This is short for Successor, the one that follows.
-- You sometimes see these as Z and S to make them shorter.
type One = Succ Zero
type Two = Succ (Succ Zero)
type Three = Succ (Succ (Succ Zero))
data List n a where
Empty :: List Zero a
Cons :: a -> List n a -> List (Succ n) a
-- [] :: List Zero a
-- [1] :: List One Int
-- [1,2,3] :: List Three Int
cons :: a -> List n a -> List (Succ n) a
uncons :: List (Succ n) a -> (a, List n a)
-- cons 0 [1,2,3] :: List (Succ Three) Int
```

This is the normal kind of example youâ€™d see when getting into dependent types, but things get trickier when you start appending lists! I havenâ€™t personally seen attempts to do safe matrix operations like this, but it seems like it could work nicely since thereâ€™s not too much subtraction or multiplication of dimensions. (Thatâ€™s what Iâ€™d be most interested in personally.)

I know Stephanie Weirich has done a lot of work on exploring this kind of thing in Haskell. Searching for stuff on â€śtype-level natsâ€ť like this may lead you to some tutorials about the tradeoffs that come when you start encoding more information in types!

I have personally found that types like `(a, List a)`

can cover guarantees like â€śthere is one or more element in the listâ€ť without anything extra. I use that pattern in Haskell and Elm a decent bit. I have also personally struggled with systems like Coq (which was made in 1985, before Haskell in 1990) but I have heard Agda and Idris give more leeway to not prove *everything*.

I think the big risk here is that the cost of managing these type level guarantees can be relatively high in practice. I think youâ€™ll get a feeling for that if you try out a dependently typed language.