Search code examples
functional-programmingsubtype

Define natural numbers in functional languages like Ada subtypes

In Ada to define natural numbers you can write this:

subtype Natural  is Integer range 0 .. Integer'Last;

This is type-safe and it is checked at compile-time. It is simple (one-line of code) and efficient (it does not use recursion to define natural numbers as many functional languages do). Is there any functional language that can provide similar functionality?

Thanks

Solution

  • This is type-safe and it is checked at compile-time.

    As you already pointed out in the comments to your question, it is not checked at compile time. Neither is equivalent functionality in Modula-2 or any other production-ready, general-purpose programming language.

    The ability to check constraints like this at compile time is something that requires dependent types, refinement types or similar constructs. You can find those kinds of features in theorem provers like Coq or Agda or in experimental/academic languages like ATS or Liquid Haskell.

    Now of those languages I mentioned Coq and Agda define their Nat types recursively, so that's not what you want, and ATS is an imperative language. So that leaves Liquid Haskell (plus languages that I didn't mention, of course). Liquid Haskell is Haskell with extra type annotations, so it's definitely a functional language. In Liquid Haskell you can define a MyNat (a type named Nat is already defined in the standard library) type like this:

    {-@ type MyNat = {n:Integer | n >= 0} @-}

    And then use it like this:

    {-@ fac :: MyNat -> MyNat @-}
fac :: Integer -> Integer
fac 0 = 1
fac n = n * fac (n-1)

    If you then try to call fac with a negative number as the argument, you'll get a compilation error. You will also get a compilation error if you call it with user input as the argument unless you specifically check that the input was non-negative. You would also get a compilation error if you removed the fac 0 = 1 line because now n on the next line could be 0, making n-1 negative when you call fac (n-1), so the compiler would reject that.

    It should be noted that even with state-of-the-art type inference techniques non-trivial programs in languages like this will end up having quite complicated type signatures and you'll spend a lot of time and effort chasing type errors through an increasingly complex jungle of type signatures having only incomprehensible type errors to guide you. So there's a price for the safety that features like these offer you. It should also be pointed out that, in a Turing complete language, you will occasionally have to write runtime checks for cases that you know can't happen as the compiler can't prove everything even when you think it should.