Define natural numbers in functional languages like Ada subtypes

Question

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

Answer 1

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.

Answer 2

Typed Racket, a typed dialect of Racket, has a rich set of numeric subtypes and it knows about a fair number of closure properties (eg, the sum of two nonnegative numbers is nonnegative, the sum of two exact integers is an exact integer, etc). Here's a simple example:

#lang typed/racket
(: f : (Nonnegative-Integer Nonnegative-Integer -> Positive-Integer))
(define (f x y)
  (+ x y 1))

Type checking is done statically, but of course the typechecker is not able to prove every true fact about numeric subtypes. For example, the following function in fact only returns values of type Nonnegative-Integer, but the type rules for subtraction only allow TR to conclude the result type of Integer.

> (lambda: ([x : Nonnegative-Integer] [y : Nonnegative-Integer])
    (- x (- x y)))
- : (Nonnegative-Integer Nonnegative-Integer -> Integer)
#<procedure>

The Typed Racket approach to numbers is described in Typing the Numeric Tower by St-Amour et al (appeared at PADL 2012). There's usually a link to the paper here, but the link seems to be broken at the moment. Google has a cached rendering of the PDF as HTML, if you search for the title.