If I have a function that should only accept odd integers, what’s the best way to implement this? Should I create a new OddInt type and only allow that, or just check whether the integer is odd inside the function and throw an error if it’s not? How would I even create an OddInt type in Julia?

function oddball(n::OddInt)
println("I won't even bother if n isn't odd")
end

OR

function oddball(n::Int64)
if isodd(n)
println("good job")
else
throw("the int must be odd!")
end
end

The easiest and perhaps cleanest approach is to use a function barrier (an outer function and then another function that handles the real work).

function oddball(n::Int)
if isodd(n)
return thisoddball(n)
end
throw(DomainError("$n is not odd"))
end
function thisoddball(n::Int)
# do stuff
return result
end

You would create an OddInt with an inner constructor that performs validation:

struct OddInt
value :: Int
function OddInt(x :: Int)
if isodd(x)
return new(x)
else
throw(DomainError("$x is not odd"))
end
end
end
function thisoddball(n :: OddInt)
return n
end

whether that is any better than the function barrier probably depends on context.

An OddInt type feels like overkill unless you actually need to treat these OddInts as first-class citizens in your code. Do you have functions that always produce OddInts? Or lots of functions that always take OddInts? If so, then having a dedicated type might be helpful. Otherwise, a simple runtime check should be quite effective. You can be more explicit about the kind of error you throw by using an ArgumentError, which provides more helpful information to future users of your code:

if !isodd(n)
throw(ArgumentError("should be odd!"))
end

or, more tersely:

isodd(n) || throw(ArgumentError("should be odd!"))

It should be noted that LLVM is increadibly clever, so checking that an integer is odd might be a no-op. Example:

julia> function f(x)
y = 2x+1
(y & 1) == 0 ? error("y is not odd!") : y
end
f (generic function with 1 method)
julia> @code_llvm f(0)
; @ REPL[17]:2 within `f'
define i64 @julia_f_13872(i64) {
top:
; ┌ @ int.jl:54 within `*'
%1 = shl i64 %0, 1
; └
; ┌ @ int.jl:53 within `+'
%2 = or i64 %1, 1
; └
; @ REPL[17]:3 within `f'
ret i64 %2
}

The LLVM code contains no trace of the second line of f.

This is precisly the sort of thing you could do if we finally had implemented inductive types in Julia

What you want is an inductive type so that the type system can make formal proofs about odd and even integers… I’ve been wanting this for a long time now.

In type theory, a system has inductive types if it has facilities for creating a new type along with constants and functions that create terms of that type.

“creating a new type” : struct

“constants” : const

“functions that create terms of that type” : f()::MyType = ...

What’s missing? Please don’t read this as antagonistic; I’m genuinely curious.

What’s different is that you want the type system to be able to prove whether an input is even or odd… so, the need to extend the type system to handle inductive types.

This is about proofs in the type system. Can Julia type system currently prove whether an element of Peano arithmetic is even or odd? Don’t think so, hence the thread.