# Would it make sense for Julia to adopt refinement types?

**URL:** <https://discourse.julialang.org/t/would-it-make-sense-for-julia-to-adopt-refinement-types/113586>\
**Category:** Internals & Design\
**Created:** [April 28, 2024, 1:38pm UTC](https://discourse.julialang.org/t/would-it-make-sense-for-julia-to-adopt-refinement-types/113586 "2024-04-28T13:38:08Z")\
**Posts on this page:** 20\
**Page:** 1

<div class="post-metadata">

**Author:** ![xiaoxi](https://avatars.discourse-cdn.com/v4/letter/x/a9adbd/32.png) [@xiaoxi](https://discourse.julialang.org/u/xiaoxi)\
**Post date:** [April 28, 2024, 1:38pm UTC](https://discourse.julialang.org/t/would-it-make-sense-for-julia-to-adopt-refinement-types/113586/1 "2024-04-28T13:38:08Z")

</div>

> Refinement types enrich a language’s type system with logical predicates that circumscribe the set of values described by the type, thereby providing software developers a tunable knob with which to inform the type system about what invariants and correctness properties should be checked on their code.

> **[Refinement Types: A Tutorial](https://arxiv.org/abs/2010.07763)**
>
> Refinement types enrich a language's type system with logical predicates that circumscribe the set of values described by the type, thereby providing software developers a tunable knob with which to inform the type system about what invariants and...

Rust and some other programming languages are experimenting with them.

> **[GitHub - flux-rs/flux: Refinement Types for Rust](https://github.com/flux-rs/flux)**
>
> Refinement Types for Rust. Contribute to flux-rs/flux development by creating an account on GitHub.

> **[GitHub - fthomas/refined: Refinement types for Scala](https://github.com/fthomas/refined)**
>
> Refinement types for Scala. Contribute to fthomas/refined development by creating an account on GitHub.

Would it make sense for Julia to have them?

---

<div class="post-metadata">

**Author:** ![gdalle](https://sea2.discourse-cdn.com/julialang/user_avatar/discourse.julialang.org/gdalle/32/27854_2.png) [@gdalle](https://discourse.julialang.org/u/gdalle)\
**Post date:** [April 28, 2024, 1:45pm UTC](https://discourse.julialang.org/t/would-it-make-sense-for-julia-to-adopt-refinement-types/113586/2 "2024-04-28T13:45:36Z")

</div>

Sounds like what we call “interfaces” (e.g. `AbstractArray`), and although there is no official formalism, there are several attempts worth mentioning like Interfaces.jl or RequiredInterfaces.jl

---

<div class="post-metadata">

**Author:** ![xiaoxi](https://avatars.discourse-cdn.com/v4/letter/x/a9adbd/32.png) [@xiaoxi](https://discourse.julialang.org/u/xiaoxi)\
**Post date:** [April 28, 2024, 2:31pm UTC](https://discourse.julialang.org/t/would-it-make-sense-for-julia-to-adopt-refinement-types/113586/3 "2024-04-28T14:31:54Z")

</div>

I may be wrong, but it seems that refinement types restrict the range of possible values of a type, while Interfaces.jl or RequiredInterfaces.jl help to restrict types that do not have certain methods.

For example, refinement types help to restrict the range of acceptable values that the absolute function can return.

```rust
#[flux::sig(fn (n:i32) -> i32{v:0<=v && n<=v})]
pub fn abs(n: i32) -> i32 {
    if 0 <= n {
        n
    } else {
        0 - n
    }
}

```

[https://flux-rs.github.io/flux/blog/01-introducing-flux.html](https://flux-rs.github.io/flux/blog/01-introducing-flux.html)

---

<div class="post-metadata">

**Author:** ![Sukera](https://avatars.discourse-cdn.com/v4/letter/s/ce7236/32.png) [@Sukera](https://discourse.julialang.org/u/Sukera)\
**Post date:** [April 28, 2024, 3:42pm UTC](https://discourse.julialang.org/t/would-it-make-sense-for-julia-to-adopt-refinement-types/113586/4 "2024-04-28T15:42:54Z")

</div>

> [@xiaoxi](#):
>
> but it seems that refinement types restrict the range of possible values of a type, while [Interfaces.jl](https://juliahub.com/ui/Packages/General/Interfaces) or [RequiredInterfaces.jl](https://juliahub.com/ui/Packages/General/RequiredInterfaces) help to restrict types that do not have certain methods

That is correct, but since refinement types are much more complicated to both implement & use than more simple interfaces (which we’d still need either way), I think the point of @gdalle is that the current problems in the Julia ecosystem would not be addressed by just adding refinement types.

> [@xiaoxi](#):
>
> For example, refinement types help to restrict the range of acceptable values that the absolute function can return

Yes, that is correct. Note that the example given doesn’t translate to Julia, because of the underflow on `0 - typemin(Int32)`. In Julia, this is always defined as wraparound arithmetic, while IIRC this panics in Rust in debug mode.

EDIT:

In release mode, rustc doesn’t even want to compile this: [Rust Playground](https://play.rust-lang.org/?version=stable&mode=release&edition=2021&gist=2a61950303dbc79c18fb216179e08255)

---

<div class="post-metadata">

**Author:** ![xiaoxi](https://avatars.discourse-cdn.com/v4/letter/x/a9adbd/32.png) [@xiaoxi](https://discourse.julialang.org/u/xiaoxi)\
**Post date:** [April 29, 2024, 7:39am UTC](https://discourse.julialang.org/t/would-it-make-sense-for-julia-to-adopt-refinement-types/113586/5 "2024-04-29T07:39:09Z")

</div>

Understood. Refinement types wouldn’t solve any problems that the Julia ecosystem has, but they would open up Julia to new applications like Liquid Haskell did in the Haskell ecosystem.

> **[Liquid Haskell](https://en.wikipedia.org/wiki/Liquid_Haskell)**
>
> Liquid Haskell is a program verifier for the programming language Haskell which allows specifying correctness properties by using refinement types. Properties are verified using a satisfiability modulo theories (SMT) solver which is SMTLIB2-compliant, such as the Z3 Theorem Prover.
>  
> This formal methods-related article is a stub. You can help Wikipedia by expanding it. This free and open-source software article is a stub. You can help Wikipedia by expanding it.

---

<div class="post-metadata">

**Author:** ![tecosaur](https://sea2.discourse-cdn.com/julialang/user_avatar/discourse.julialang.org/tecosaur/32/23206_2.png) [@tecosaur](https://discourse.julialang.org/u/tecosaur)\
**Post date:** [April 29, 2024, 8:49am UTC](https://discourse.julialang.org/t/would-it-make-sense-for-julia-to-adopt-refinement-types/113586/6 "2024-04-29T08:49:10Z")

</div>

Personally I’m quite a fan of the idea of refinement types in Julia, and find the paper you linked rather compelling.

We often write code that requires positive, even, or non-empty values, and so a type system that allows for this level of detail to be specified both seems like a route for a higher standard of robustness that is possible to be specified using “plain” old interfaces.

The way I like to look at refinement types is that they’re compile-time contracts. My understanding is that the main complexity as a result is that suddenly you then need something like Z3 in the compiler, and describing that as a tough sell seems like an understatement.

For a quick intro and a motivating example, I’d recommend this short article introducing Haskell’s refined library: [Announcing the refinement types library – Functional programming debugs you](http://nikita-volkov.github.io/refined/)

---

<div class="post-metadata">

**Author:** ![Benny](https://avatars.discourse-cdn.com/v4/letter/b/49beb7/32.png) [@Benny](https://discourse.julialang.org/u/Benny)\
**Post date:** [April 29, 2024, 10:23am UTC](https://discourse.julialang.org/t/would-it-make-sense-for-julia-to-adopt-refinement-types/113586/7 "2024-04-29T10:23:37Z")

</div>

I’m understanding 10% of this at most, but I think I’m seeing at least 2 very different approaches going on. Rust’s seems to leave the original type alone, but the compiler errors when an asserted condition of its values can’t be proven. Haskell’s on the other hand wraps the type into a separate `Refined` type, and you must `unrefine` it to extract the value for normal computation. Apparently unwrapping is done at compile-time (no runtime cost), and the wrapping and verification can be done at compile-time with `refineTH`; there is also `refineTH_` to refine then unrefine immediately, which I’m interpreting as a compile-time assertion.

Either way, it sounds like static analysis and AOT compilation, so I’m not sure how it’ll fit well into Julia. The Rust code examples I (think I) understand rely on computation of values knowable at compile-time; does that mean we need runtime verification otherwise, especially in interactive sessions? I’m definitely too unfamiliar with the topic and languages to know how formal verification is used and how refinement types play into that.

---

<div class="post-metadata">

**Author:** ![mefob](https://avatars.discourse-cdn.com/v4/letter/m/ea5d25/32.png) [@mefob](https://discourse.julialang.org/u/mefob)\
**Post date:** [May 7, 2024, 4:19am UTC](https://discourse.julialang.org/t/would-it-make-sense-for-julia-to-adopt-refinement-types/113586/8 "2024-05-07T04:19:14Z")

</div>

I would love to see refinement types myself. Having tinkered with Ada/SPARK in the past, I am convinced this is great and straightforward way to avoid many bugs.

Once the annotations are in place, a lot can be done to improve program quality, from injecting dynamic tests, to a full formal verification of the entire program.

It is not clear if there is a single best approach, probably a mix of different approaches is best.

As a first step, we’d need a way to attach additional specifications to variables or return values of functions, such as

- range
- set membership
- arbitrary predicates

I don’t think there is currently a way to add attributes to variables, but the user-facing syntax could look like this:  
`@annotation 0 < x < 10`  
`@annotation myPredicate(x) == true`  
The annotations could also go into docstrings:

```julia
"""
N counts the 
@annotation n > 0
"""
n::Integer

```

Based on these annotations, libraries could generate tests, add dynamic checks, or try to statically prove the assertions.

Such checks would not have to be part of the core, different verification tools could use different approaches. As an example, one tool could verify ranges, while another tool could verify physical units.

Some libraries to study for inspiration:

> **[“learn.adacore.com"](https://learn.adacore.com/courses/intro-to-spark/index.html)**
>
> An interactive learning platform to teach the Ada and SPARK programming languages.

[https://docs.adacore.com/spark2014-docs/html/ug/en/source/type\_contracts.html#predicates](https://docs.adacore.com/spark2014-docs/html/ug/en/source/type_contracts.html#predicates)

> <https://github.com/creusot-rs/creusot/blob/master/ARCHITECTURE.md>

These annotations could also be used, very naturally, to implement design by contract:

> [@DesignByContract.jl: DbC interface for Julia (feedback)](https://discourse.julialang.org/t/designbycontract-jl-dbc-interface-for-julia-feedback/49079):
>
> I’ve been working on a new package for Julia which brings the “Design by Contract” functionality from Eiffel in the form of macros. I think this is something that could be used on future Julia application development, when considering the correctness checks on runtime as well as easing the testing process. However, developing a package that is basically adding checks embedded within Julia code seems a bit off since the language thrives on efficiency. I wanted to know the community’s thoughts on…

[https://www.cs.cmu.edu/~csd-phd-blog/2023/rust-verification-with-verus/](https://www.cs.cmu.edu/~csd-phd-blog/2023/rust-verification-with-verus/)

> **[GitHub - newca12/awesome-rust-formalized-reasoning: An exhaustive list of all...](https://github.com/newca12/awesome-rust-formalized-reasoning)**
>
> An exhaustive list of all Rust resources regarding automated or semi-automated formalization efforts in any area, constructive mathematics, formal algorithms, and program verification. - newca12/aw...

Variable annotations would also nicely enable design by contract

> [@DesignByContract.jl: DbC interface for Julia (feedback)](https://discourse.julialang.org/t/designbycontract-jl-dbc-interface-for-julia-feedback/49079):
>
> I’ve been working on a new package for Julia which brings the “Design by Contract” functionality from Eiffel in the form of macros. I think this is something that could be used on future Julia application development, when considering the correctness checks on runtime as well as easing the testing process. However, developing a package that is basically adding checks embedded within Julia code seems a bit off since the language thrives on efficiency. I wanted to know the community’s thoughts on…

Additionally, they would also be useful for physical units, e.g. through Unitful.jl.

---

<div class="post-metadata">

**Author:** ![xiaoxi](https://avatars.discourse-cdn.com/v4/letter/x/a9adbd/32.png) [@xiaoxi](https://discourse.julialang.org/u/xiaoxi)\
**Post date:** [July 4, 2024, 7:27pm UTC](https://discourse.julialang.org/t/would-it-make-sense-for-julia-to-adopt-refinement-types/113586/9 "2024-07-04T19:27:48Z")

</div>

The authors of Flux made a presentation last year.

[![](https://global.discourse-cdn.com/julialang/original/3X/e/8/e81e0ac7c8927d251aac695f2e75322961d96520.jpeg "[SOAP'23] Flux: Refinement types for Rust") ](https://www.youtube.com/watch?v=NIJtZ0yUDX0)

---

<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:** [July 15, 2024, 7:51am UTC](https://discourse.julialang.org/t/would-it-make-sense-for-julia-to-adopt-refinement-types/113586/10 "2024-07-15T07:51:48Z")

</div>

Stumbled on an example where it seems like refinement types would be useful to improve Julia’s type inference:

```julia
f(t::Tuple, n::Bool) = t[10 + n]

```

Julia would ideally be able to prove that the below abstract call is type stable, but it currently fails:

```julia-repl
julia> Core.Compiler.return_type(f, Tuple{Tuple{Bool,String,Vararg{Int}},Bool})
Union{Bool, Int64, String}

```

The call will always return `Int` (if it returns), because the index `10 + n` is always either `10` or `11`, thus the index is always greater than two.

I guess Julia isn’t able to prove this because, after `n` gets converted to `Int`, Julia has forgotten about the fact that `n` can only take two values: zero or one. Some kind of refinement types (perhaps purely for internal use in the compiler) could presumably help Julia remember that the result of `convert(::Type{Int}, ::Bool)` is always nonnegative, and thus that `10 + n` is always greater than two.

EDIT: issue on Github:

> <https://github.com/JuliaLang/julia/issues/55155>
>
> \`\`\`julia-repl
> julia\> f(t::Tuple, n::Bool) = t\[10 + n\]
> f (generic function with… 1 method)
> 
> julia\> Core.Compiler.return\_type(f, Tuple{Tuple{Bool,String,Vararg{Int}},Bool})
> Union{Bool, Int64, String}
> 
> julia\> versioninfo()
> Julia Version 1.12.0-DEV.unknown
> Commit 0fdd655 (2024-07-17 15:39 UTC)
> \`\`\`
> 
> Ideally, the inferred return type would be \`Int\`. Proof: the index \`10 + n\` is always either \`10\` or \`11\`, thus the index is always greater than two.
> 
> Context, hypothesized solution approach using refinement types: https://discourse.julialang.org/t/would-it-make-sense-for-julia-to-adopt-refinement-types/113586/10

---

<div class="post-metadata">

**Author:** ![kapple](https://sea2.discourse-cdn.com/julialang/user_avatar/discourse.julialang.org/kapple/32/218915_2.png) [@kapple](https://discourse.julialang.org/u/kapple)\
**Post date:** [July 17, 2024, 3:59pm UTC](https://discourse.julialang.org/t/would-it-make-sense-for-julia-to-adopt-refinement-types/113586/11 "2024-07-17T15:59:05Z")

</div>

As a sidenote, I understand formal verification is not possible in Julia and Supposition.jl seeks to assist in spite of that.

Instead of applying more restrictions to the types you implement, you can alternatively apply appropriate tests to check your algorithms output numbers they way you expect using Supposition.jl. Property-based fuzzy testing.

---

<div class="post-metadata">

**Author:** ![vchuravy](https://sea2.discourse-cdn.com/julialang/user_avatar/discourse.julialang.org/vchuravy/32/8_2.png) [@vchuravy](https://discourse.julialang.org/u/vchuravy)\
**Post date:** [July 17, 2024, 7:52pm UTC](https://discourse.julialang.org/t/would-it-make-sense-for-julia-to-adopt-refinement-types/113586/12 "2024-07-17T19:52:41Z")

</div>

The core issue here is that our lattice only has Const and PartialConst, but not “Set of Values” or “Range of Values” representation.

So we can represent `Union{Int, Float}`, but not `Union{Const(false), Const(true)}`.

---

<div class="post-metadata">

**Author:** ![tecosaur](https://sea2.discourse-cdn.com/julialang/user_avatar/discourse.julialang.org/tecosaur/32/23206_2.png) [@tecosaur](https://discourse.julialang.org/u/tecosaur)\
**Post date:** [July 18, 2024, 8:58am UTC](https://discourse.julialang.org/t/would-it-make-sense-for-julia-to-adopt-refinement-types/113586/13 "2024-07-18T08:58:53Z")

</div>

IIRC @Sukera had a brief look at Refinement Types in Julia, and may have run into exactly that limitation with the lattice.

---

<div class="post-metadata">

**Author:** ![Sukera](https://avatars.discourse-cdn.com/v4/letter/s/ce7236/32.png) [@Sukera](https://discourse.julialang.org/u/Sukera)\
**Post date:** [July 18, 2024, 9:27am UTC](https://discourse.julialang.org/t/would-it-make-sense-for-julia-to-adopt-refinement-types/113586/14 "2024-07-18T09:27:38Z")

</div>

> [@tecosaur](#):
>
> and may have run into exactly that limitation with the lattice.

Nah, I was experimenting with an entirely separate lattice. Regular inference was already taking care of `Const` and `ParticalConst`. The problem was that the abstract interpreter, at the time, did NOT like having to lug around that separate lattice while also doing its own inference, and the docs about how to extend that were (are?) sparse at best.

I still think it would be useful to stabilize that interface further, which would potentially open up a whole bunch of likely useful analysis & optimization. Maybe things are better in the future, there were some interesting talks in that direction (not refinement types in particular) at this years’ juliacon (specifically, [this](https://pretalx.com/juliacon2024/talk/D3H79J/) and [this](https://pretalx.com/juliacon2024/talk/D88XFU/) talk have given me some ideas for projects).

All that being said - I don’t think adopting refinement types at the core level & by default would be a boon. It’s just way too costly for the sideeffect-happy, non-trivial, non-functional code that is idiomatic in Julia. IMO it’d be more useful as a distinct check as part of a testsuite.

---

<div class="post-metadata">

**Author:** ![filchristou](https://sea2.discourse-cdn.com/julialang/user_avatar/discourse.julialang.org/filchristou/32/26760_2.png) [@filchristou](https://discourse.julialang.org/u/filchristou)\
**Post date:** [July 18, 2024, 9:46am UTC](https://discourse.julialang.org/t/would-it-make-sense-for-julia-to-adopt-refinement-types/113586/15 "2024-07-18T09:46:20Z")

</div>

isn’t `Val` meant to do more or less this ? bringing values to the type system ?

---

<div class="post-metadata">

**Author:** ![tecosaur](https://sea2.discourse-cdn.com/julialang/user_avatar/discourse.julialang.org/tecosaur/32/23206_2.png) [@tecosaur](https://discourse.julialang.org/u/tecosaur)\
**Post date:** [July 18, 2024, 11:24am UTC](https://discourse.julialang.org/t/would-it-make-sense-for-julia-to-adopt-refinement-types/113586/16 "2024-07-18T11:24:50Z")

</div>

> [@Sukera](#):
>
> too costly

In what sort of sense? It seems to me the main thing you’d be missing out on for casual script-y code is potential optimisations and no-throw-type guarantees.

---

<div class="post-metadata">

**Author:** ![Sukera](https://avatars.discourse-cdn.com/v4/letter/s/ce7236/32.png) [@Sukera](https://discourse.julialang.org/u/Sukera)\
**Post date:** [July 18, 2024, 2:58pm UTC](https://discourse.julialang.org/t/would-it-make-sense-for-julia-to-adopt-refinement-types/113586/17 "2024-07-18T14:58:22Z")

</div>

> [@tecosaur](#):
>
> In what sort of sense? It seems to me the main thing you’d be missing out on for casual script-y code is potential optimisations and no-throw-type guarantees.

TL;DR of the below: In pretty much every sense, computational & dev time.

* * *

It’s as you say above - to handle the general case, you need an SMT solver like z3 at potentially every dispatch. Not to mention that these sorts of things _really_ dislike modelling mutability, because that introduces a temporal component. Solvers don’t like temporal components (or rather, YOU shouldn’t like temporal components here), and now you suddenly need to [add invariants manually](https://www.hillelwayne.com/post/lpl/#on-leftpad) to help the solver along. Not a good fit for script-y code.

Btw, even the functional languages struggle with these temporal invariants. Just take a look at how much additional code you need to [prove _`leftpad`_](https://github.com/hwayne/lets-prove-leftpad)! And that’s just for an innocent little function like `leftpad`, just imagine how much more you’ll need for something that you actually care about, nevermind having the solver actually check that the model works out.

And then there’s the horror of actually [composing (temporal) specifications](https://www.hillelwayne.com/post/spec-composition/). This isn’t (to the best of my knowledge) automatable.

> [@filchristou](#):
>
> isn’t `Val` meant to do more or less this ? bringing values to the type system ?

Yes, sort of - but even then you can easily get `Any` back out and you still don’t have mutability. Also, lots of things that you’d _think_ you can lift like that you actually can’t; like `String` (it’s technically mutable but we all pretend otherwise), structs containing `Symbol`, and the like. Lifting things to type parameters [very quickly](https://github.com/Seelengrab/TypingTheJuliaInterview.jl) runs into inference just giving up and dealing with it “later”. So that doesn’t help with actually proving properties about your code either.

---

<div class="post-metadata">

**Author:** ![mefob](https://avatars.discourse-cdn.com/v4/letter/m/ea5d25/32.png) [@mefob](https://discourse.julialang.org/u/mefob)\
**Post date:** [February 23, 2025, 7:24pm UTC](https://discourse.julialang.org/t/would-it-make-sense-for-julia-to-adopt-refinement-types/113586/18 "2025-02-23T19:24:56Z")

</div>

Thanks for the links, the n-queens problem via types is cool!

I don’t think @xiaoxi was suggesting to replace the current type system with refinement types. That would be a bad idea for the reasons you outlined, and either way, the result would be a completely new language.

On the other hand, keeping Julia’s current type system for dispatch and then using refinement types as an additional checker to verify program properties seems like a very feasible approach. It would actually be much easier than many existing type checking algorithms (e.g. J or W), as there would be no polymorphism to deal with.

Some other advantages:

- Failure to verify type properties does not affect running the program
- Verification can run asynchronously without affecting scripting
- Proven technology: Ada/SPARK has been used in industry for decades, the Rust libraries have gained a lot of momentum
- Verification of useful properties is not always a hard problem. Units of measurements are linear with negligible memory without heterogeneous arrays
- Units of measurements would add a whole new dimension to verify numerical algorithms, as unit consistency puts very strict, and easily verifiable, constrains on the permissible operations. See e.g. the book by Hart, Multidimensional analysis.
- An external type verifier would not be constrained by Julia’s type system and could use whatever algorithm is best. We see this e.g. with Uniful.jl. In principle, verifying measurement units is a very simple problem. The problem is that expressing the measurement units type system via Julia’s type system itself is very challenging and often leads to type instabilities. So far, it hasn’t been possible to consistently verify units at the type level, which especially affects some of the core ODE libraries, and lead to the creation of [GitHub - SymbolicML/DynamicQuantities.jl: Efficient and type-stable physical quantities in Julia](https://github.com/SymbolicML/DynamicQuantities.jl), which replaces the type instabilities by a runtime overhead. Just like the n-queens problems, units of measurement are easy to solve with a constraint-based approach, but very hard to express through Julia’s type system.

---

<div class="post-metadata">

**Author:** ![mefob](https://avatars.discourse-cdn.com/v4/letter/m/ea5d25/32.png) [@mefob](https://discourse.julialang.org/u/mefob)\
**Post date:** [February 24, 2025, 9:22pm UTC](https://discourse.julialang.org/t/would-it-make-sense-for-julia-to-adopt-refinement-types/113586/19 "2025-02-24T21:22:05Z")

</div>

One additional comment, because I don’t want my last response to be seen as criticism of Unitful.jl or DynamicQuantities.jl, two awesome libraries that I could not live without.

The point that I wanted to make is that type-level programming is simply not the easiest approach for these kinds of problems.

The n-queens problem is the perfect example, because it is very similar to what a typechecker would do. In [Typing the Julia Interview](https://github.com/Seelengrab/TypingTheJuliaInterview.jl/blob/main/src/TypingTheJuliaInterview.jl), you’ll find 200 lines of code of the form:

```julia
struct AddQueens{n,x,cs}
    function AddQueens{n,x,cs}() where {n,x,cs}
        pred = PeanoLT{x,n}()
        AddQueensIf{pred,n,x,cs}()
    end
end

struct Solution{n}
    Solution{n}() where {n} = First{AddQueens{n,Z,Cons{Nil,Nil}}()}()
end

```

I barely understand what this does, and I am certainly not able to write such code on my own, probably a safe assumption for 99% of the Julia community. Obviously the insanity of this approach is what makes it such a great hack.

Trying to express complicated structures through type-level programming is a fun exercise, but not a good engineering practice, as long as there are alternatives. Just like C++ template metaprogramming.

On the other hand, a version of the n-queens based on constraint programming, [CLP(FD)](https://www.metalevel.at/prolog/clpz), is very simple. Even if you’ve never seen [Picat](https://rosettacode.org/wiki/N-queens_problem#Picat), the code is immediately clear once you know that `#!=` means to post a constraint that both sides are not equal.  
This is the entire code, while the type-level version can barely solve N6, the Picat version can do N1000 easily.

```picat
queens_naive(N, Q) => 
  Q = new_list(N),
  Q :: 1..N,
  foreach(I in 1..N, J in 1..N, I < J) 
    Q[I] #!= Q[J],
    Q[I] + I #!= Q[J] + J,
    Q[I] - I #!= Q[J] - J
  end,
  solve([ff], Q).

```

I chose Picat, a slightly modernized Prolog version, because it has loops, Prolog would have used a recursive call instead. Of course, an SMT solver could also be used and there are CLP libraries for most programming languages, including Julia. CLP just happens to be perfectly integrated into many logic programming languages.

For this reason, I strongly believe that we need to abandon the idea of creating more and more complex type systems, then making more and more heroic efforts to express our program logic in such type systems, only to discover that we’ve pushed the compiler to far and need to follow up with even more heroic efforts on the compiler side to get our programs to compile in a reasonable time, if at all. Julia is neither Haskell, nor Rust.

Instead, the language should provide a basic type system that makes sure the right machine code gets generated with the minimum amount of dynamism. All checks beyond this should be left to user-space libraries.

This would also provide additional features that are unthinkable otherwise, such as e.g. different levels of warnings depending on the type consistency.  
In the case of measurement units, a system could have the following warning levels, depending on whether it was used for quick scripting or for important engineering calculations:

1. Units are not consistent, e.g. 1u"m" + 1u"kg". This is clearly an error.
2. Units are consistent, but not uniquely determined. The equivalent of a type instability, e.g. a function that returns u"m" or u"kg" depending on the context. This is most likely an error.
3. Constants don’t (yet) have units, e.g. 1u"m" + 1. An error, but might need to be ignored during gradual typing.
4. Units are consistent, but not fixed, e.g. the unit-polymorphic function f(a,b) = a+b. Might be ok for a generic function.
5. Units are consistent and fixed, but not all variables have units specified. E.g. x=f(1u"m", 2u"m"). x inherits the unit through f, which is probably ok.
6. Units are consistent and fixed, and all variables/functions have types attached to them, e.g. in the example above x is specified to have a type u"m". I’d want this for a high reliability application.

The nice thing of such an approach is that the programmer can start with an untyped program, and then add types throughout the program, and get a warning the moment the types are not consistent. There is no all or nothing requirement, where the program does not even compile as long as not all variables are properly typed.

Providing this level of error handling through the type system is probably impossible, but for an external library based on constraints, it would only be a very minor addition.

Julia has most of the machinery already in place. What is lacking is a good way to attach types and typing predicates to variables and functions, similar to @doc. Maybe this mechanism could be enough to capture extra type information.

---

<div class="post-metadata">

**Author:** ![Tamas\_Papp](https://sea2.discourse-cdn.com/julialang/user_avatar/discourse.julialang.org/tamas_papp/32/25949_2.png) [@Tamas\_Papp](https://discourse.julialang.org/u/Tamas_Papp)\
**Post date:** [February 25, 2025, 7:51am UTC](https://discourse.julialang.org/t/would-it-make-sense-for-julia-to-adopt-refinement-types/113586/20 "2025-02-25T07:51:38Z")

</div>

> [@mefob](#):
>
> I barely understand what this does, and I am certainly not able to write such code on my own, probably a safe assumption for 99% of the Julia community.

Just to clarify, TypingTheJuliaInterview.jl is something between a practical joke and a demo of pushing the type system too far. It is clearly not meant as idomatic Julia code, and its README explains this clearly. Generally, it is recommended not to do computations in type space.

> [@mefob](#):
>
> Instead, the language should provide a basic type system that makes sure the right machine code gets generated with the minimum amount of dynamism.

I am under the impression that this is what Julia does now.

[Next page](https://discourse.julialang.org/t/would-it-make-sense-for-julia-to-adopt-refinement-types/113586.md?page=2)