Proposal: Fixed length lists and restricted number types

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! :slight_smile: 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.

8 Likes

Rust has the typenum crate (1) and the closely related generic-array crate (2). They use the typesystem to emulate constant generics.

The nalgebra crate (3) then uses these arrays and give strong compile time guarantees (e.g. that dimensions match in matrix multiplication).

I think a typenum like thing could be defined in userland elm. Maybe?

1: https://docs.rs/typenum/1.12.0/typenum/
2: https://docs.rs/generic-array/0.14.1/generic_array/
3: https://docs.rs/nalgebra/0.21.0/nalgebra/

man that Succs

that code seems interesting

I think you’ll find @Lucas_Payr’s maser thesis work very interesting:


1 Like

This topic was automatically closed 10 days after the last reply. New replies are no longer allowed.