It should be possible to define a custom number type that has a finite amount of possible values. For example, here is a type of number that includes all integers that are less than or equal to 100

type MyNumber ( x : Int ) where x <= 100

You can define these like this:

-- defined at compile time; invalid value gives compile error
MyNumber 68
-- From an integer
MyNumber.fromInt 6 == Just <| MyNumber 6
MyNumber.fromInt 700 == Nothing -- to high

This could be useful for fixed length lists. Here is an example where the index can be from 0 to 9 (curly brackets are used to distinguish from normal lists:

type MyIndex ( i : Int ) where i <= 9 && i >= 0
type MyList = FixedList MyIndex Int
MyList { 7, 9, 11, 0, 1, 9, 1, 2, 8, 5 } -- ok
MyList { 1, 2, 9, 7 } -- compile error; too small
MyList.fromList [ 0 ] == Nothing

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.