# Type domain (static) integers

**URL:** <https://discourse.julialang.org/t/type-domain-static-integers/118568>\
**Category:** Internals & Design\
**Tags:** discussion, integer\
**Created:** [August 24, 2024, 4:52pm UTC](https://discourse.julialang.org/t/type-domain-static-integers/118568 "2024-08-24T16:52:11Z")\
**Posts on this page:** 9\
**Page:** 2

<div class="post-metadata">

**Author:** ![nsajko](https://sea2.discourse-cdn.com/julialang/user_avatar/discourse.julialang.org/nsajko/32/221187_2.png) [@nsajko](https://discourse.julialang.org/u/nsajko)\
**Post date:** [August 27, 2024, 2:20pm UTC](https://discourse.julialang.org/t/type-domain-static-integers/118568/21 "2024-08-27T14:20:35Z")

</div>

> [@caleb-allen](#):
>
> Why is your design better?

It’s not strictly better, but some of the benefits are:

- More type safety.
- The increment and decrement operations are very simple, which should benefit functions that need to recurse over a type domain integer by incrementing it or decrementing it. Decrementing (`natural_predecessor`) is just `getfield`.
- It’s possible to express sets of values such as “the negative integers” or “the positive integers” etc. in the type system. With correct subtyping relations, of course.

> [@caleb-allen](#):
>
> Can you make this available?

It’s a registered package: TypeDomainNaturalNumbers.jl. ~~The released versions don’t have the introduced types subtype `Integer` yet, though.~~

---

<div class="post-metadata">

**Author:** ![nsajko](https://sea2.discourse-cdn.com/julialang/user_avatar/discourse.julialang.org/nsajko/32/221187_2.png) [@nsajko](https://discourse.julialang.org/u/nsajko)\
**Post date:** [August 28, 2024, 7:23pm UTC](https://discourse.julialang.org/t/type-domain-static-integers/118568/22 "2024-08-28T19:23:37Z")

</div>

> [@nsajko](#):
>
> It’s possible to express sets of values such as “the negative integers” or “the positive integers” etc. in the type system. With correct subtyping relations, of course.

A specific example where that’s useful: defining rationals:

```julia-repl
julia> using TypeDomainNaturalNumbers

julia> struct TypeDomainRational{
           Num <: TypeDomainInteger,
           Den <: NonnegativeInteger,
       } <: Real
           num::Num
           den::Den
       end

julia> const TypeDomainRationalFinite = TypeDomainRational{Num, Den} where {
           Num <: TypeDomainInteger,
           Den <: PositiveInteger,
       };

julia> TypeDomainRationalFinite <: TypeDomainRational <: Real
true

```

So it’s not possible (as ensured by the type system) to create a rational with a negative denominator. Or the type of a rational with a negative denominator. And “finite rationals” (not infinity, not NaN) are also expressible in the type system.

---

<div class="post-metadata">

**Author:** ![adienes](https://sea2.discourse-cdn.com/julialang/user_avatar/discourse.julialang.org/adienes/32/37459_2.png) [@adienes](https://discourse.julialang.org/u/adienes)\
**Post date:** [August 28, 2024, 7:50pm UTC](https://discourse.julialang.org/t/type-domain-static-integers/118568/23 "2024-08-28T19:50:12Z")

</div>

but one could just as well do this with a check (of values) in the constructor for `Rational` already. This example shows that a `TypeDomainInteger` might be useful to construct a `TypeDomainRational`, sure. but what’s the value of a `TypeDomainRational` over a normal `Rational` + a few `isfinite` calls?

---

<div class="post-metadata">

**Author:** ![CameronBieganek](https://sea2.discourse-cdn.com/julialang/user_avatar/discourse.julialang.org/cameronbieganek/32/6915_2.png) [@CameronBieganek](https://discourse.julialang.org/u/CameronBieganek)\
**Post date:** [August 28, 2024, 7:56pm UTC](https://discourse.julialang.org/t/type-domain-static-integers/118568/24 "2024-08-28T19:56:28Z")

</div>

The value of a `TypeDomainRational` is in the ability to create a `TypeDomainComplexRational`. 😉

---

<div class="post-metadata">

**Author:** ![CameronBieganek](https://sea2.discourse-cdn.com/julialang/user_avatar/discourse.julialang.org/cameronbieganek/32/6915_2.png) [@CameronBieganek](https://discourse.julialang.org/u/CameronBieganek)\
**Post date:** [August 28, 2024, 7:59pm UTC](https://discourse.julialang.org/t/type-domain-static-integers/118568/25 "2024-08-28T19:59:21Z")

</div>

> [@nsajko](#):
>
> So it’s not possible (as ensured by the type system) to create a rational with a negative denominator. Or the type of a rational with a negative denominator. And “finite rationals” (not infinity, not NaN) are also expressible in the type system.

If you want everything to be checked by the type system than you might be better off using a dependently typed language like Lean:

> **[Lean Programming Language](https://lean-lang.org/)**
>
> Lean is an open-source programming language and proof assistant that enables correct, maintainable, and formally verified code.

---

<div class="post-metadata">

**Author:** ![nsajko](https://sea2.discourse-cdn.com/julialang/user_avatar/discourse.julialang.org/nsajko/32/221187_2.png) [@nsajko](https://discourse.julialang.org/u/nsajko)\
**Post date:** [August 28, 2024, 8:00pm UTC](https://discourse.julialang.org/t/type-domain-static-integers/118568/26 "2024-08-28T20:00:27Z")

</div>

> [@adienes](#):
>
> what’s the value of a `TypeDomainRational` over a normal `Rational` + a few `isfinite` calls?

How about you read the thread here, and/or the linked discussion? This has now been discussed extensively. TBH at this point you’re just being flippant, at least that’s the way I see it.

---

<div class="post-metadata">

**Author:** ![adienes](https://sea2.discourse-cdn.com/julialang/user_avatar/discourse.julialang.org/adienes/32/37459_2.png) [@adienes](https://discourse.julialang.org/u/adienes)\
**Post date:** [August 28, 2024, 8:04pm UTC](https://discourse.julialang.org/t/type-domain-static-integers/118568/27 "2024-08-28T20:04:57Z")

</div>

can you point me to where in the extensive discussion an answer was given to that question, or my original question?

> Do you have any benchmarks for a common set of use cases showing relevant performance improvements over plain value-domain integers?

I mean, you don’t “owe” me an answer or anything. If you don’t want to provide examples of where — _concretely_ ---- this tool is useful that’s fine. I was just trying to engage with the idea you raised and understand why one would want to use it. I think it’s also worth noting that you did specifically ask to “know more about the reasons people are opposed to getting this into `Base`” so I’m not just being contrarian for pettiness’ sake.

---

<div class="post-metadata">

**Author:** ![sadish-d](https://sea2.discourse-cdn.com/julialang/user_avatar/discourse.julialang.org/sadish-d/32/48058_2.png) [@sadish-d](https://discourse.julialang.org/u/sadish-d)\
**Post date:** [September 2, 2024, 4:19am UTC](https://discourse.julialang.org/t/type-domain-static-integers/118568/28 "2024-09-02T04:19:21Z")

</div>

I don’t have much to add but was reading through a bit of `Static.jl` and saw this, in case people find it relevant.

@nsajko said “having [type domain integers] outside of Base means it’s not available for improving Base, not without type piracy”.

`Static.jl` has this:

```julia
const IntType = Union{StaticInt, Int}
IntType(x::Integer) = Int(x)

```

`Union{StaticInt, Int}` is an instance of `Type{Union{StaticInt, Int}}`, which does not “belong to” `Static.jl` even if `StaticInt` does. `Integer` doesn’t belong to `Static.jl`. I could be wrong, but I think `IntType(x::Integer) = Int(x)` constitutes type piracy. Previous discussion here: [Is dispatch on another type's parameter (::NotMyType{MyType}) piracy?](https://discourse.julialang.org/t/is-dispatch-on-another-types-parameter-notmytype-mytype-piracy/110797)

---

<div class="post-metadata">

**Author:** ![jar1](https://avatars.discourse-cdn.com/v4/letter/j/c0e974/32.png) [@jar1](https://discourse.julialang.org/u/jar1)\
**Post date:** [September 2, 2024, 4:41am UTC](https://discourse.julialang.org/t/type-domain-static-integers/118568/29 "2024-09-02T04:41:37Z")

</div>

I’ll just point out an alternative way of doing compile-time computation. [`comptime`](https://kristoff.it/blog/what-is-zig-comptime/) is a keyword in Zig which takes an expression and evaluates it at compile time.

You can’t dispatch on it like a type, but the big advantage is it’s just the same as the normal language: no macro scoping issues, no need to learn about type-level programming.

One library implementation exists in Julia; it would be great to have guaranteed compile-time evaluation built into the language though.

> **[GitHub - AlgebraicJulia/CompTime.jl: Library for compile-time computing in julia](https://github.com/AlgebraicJulia/CompTime.jl)**
>
> Library for compile-time computing in julia

[Previous page](https://discourse.julialang.org/t/type-domain-static-integers/118568.md?page=1)