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.
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.)