Type domain (static) integers

Internals & Design
,
21

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.

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

1 Like
22

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

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.

23

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?

1 Like
24

The value of a TypeDomainRational is in the ability to create a TypeDomainComplexRational. :wink:

2 Likes
25

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

https://lean-lang.org/

26

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.

27

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.

1 Like
28

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:

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?

29

I’ll just point out an alternative way of doing compile-time computation. 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.

2 Likes